这个问题与我问的另一个问题相关，但我意识到该问题中的一个附带问题值得有自己的问题。
使用 JavaScript，我想查看用户从网页复制的内容。当用户粘贴时，读取剪贴板内容相当容易：
document.addEventListener("paste", e => {
let text = e.clipboardData.getData("text");
alert("pasting text: " + text);
});
这会正确地创建带有刚刚粘贴的内容的警报。然而，当用户进行复制时，获取剪贴板数据会更加困难。
document.addEventListener("copy", e => {
let text = e.clipboardData.getData("text");
alert("copying text: " + text);
});
这会警告“正在复制数据：”，但后面没有任何文本。那是因为该getData方法正在返回""（空字符串）。我的理解是，当您执行粘贴以外的任何操作时，网站读取您的剪贴板会被认为是一个太大的安全问题。
document.addEventListener("copy", () => {
navigator.clipboard.readText().then(text => alert("copied text: " + text));
});
这是可行的，但在发出警报之前，它会创建一个弹出窗口，请求网站读取剪贴板的权限。我不想有这个弹出窗口。
document.addEventListener("copy", () => {
let text = window.getSelection().toString();
alert("copying text: " + text);
});
这似乎是我想要的。允许这样做似乎很奇怪，但方法 1 却不允许。
我有一些问题：
我对 Haskell 还很陌生，我认为我在某个地方存在根本性的误解。当我在 GHCi 中（使用命令ghci）时，我可以输入import System.Random，它就可以工作。然后我可以生成随机数。
接下来，我创建一个名为的文件test.hs，其中只包含一行：import System.Random. 然后我调用该命令ghc test.hs并收到以下错误消息：
test.hs:1:1: error:\n Could not find module \xe2\x80\x98System.Random\xe2\x80\x99\n There are files missing in the \xe2\x80\x98random-1.1\xe2\x80\x99 package,\n try running \'ghc-pkg check\'.\n Use -v to see a list of the files searched for.\n |\n1 | import System.Random\n | ^^^^^^^^^^^^^^^^^^^^\n但是，如果我返回 GHCi，我可以输入:load test.hs. 这有效，并允许我生成随机数。
当我运行时ghc-pkg check，我只收到有关丢失黑线鳕接口文件的警告：https ://pastebin.com/6a9f0nYZ 。据我了解，这与当前问题无关。
另外，当我运行时ghc-pkg list，random-1.1位于列表中，因此 …
假设我在 Coq 中写出以下引理和证明：
Lemma foo : forall A, A -> A.
Proof.
- simpl.
- auto.
Qed.
在simpl这里没有做任何事情，这是一个不好的使用要点（-）。当我尝试用 编译它时coqc，我收到以下投诉：
Error: [Focus] Wrong bullet -: Current bullet - is not finished.
我很清楚为什么会发生这个错误。当我打开 的第二个要点时auto，它抱怨我没有完成第一个要点。但是，对我来说没有意义的是这段代码编译得很好：
From Coquelicot Require Import Complex.
Lemma foo : forall A, A -> A.
Proof.
- simpl.
- auto.
Qed.
似乎导入 from 的行为Coquelicot使得项目符号点被完全忽略。几个问题：
我目前使用的是用 OCaml 4.10.2 和 Coquelicot 3.2.0 编译的 Coq 8.13.2。