问题描述
我最近安装了带有 opam 的 Coq 8.12.2 版。我已经使用以下命令安装了 Coq 的所有软件包：
opam repo add coq-released https://coq.inria.fr/opam/released
但是当我尝试在 Coqide 中编译包时，它无法识别 coquelicot。
From Coq Require Import Lia Reals Lra List.
From Coquelicot Require Import Coquelicot.
From Coq Require Import PropExtensionality FunctionalExtensionality.
Require Import Rbar_compl.
Require Import sum_Rbar_nonneg.
Require Import measurable_fun.
Require Import subset_compl.
Require Import R_compl.
Require Import sigma_algebra_R_Rbar.
Require Import sigma_algebra.
Require Import simple_fun.
Require Import LInt_p.
我收到这些错误：Cannot find a physical path bound to logical path matching suffix <> and prefix Coquelicot
和
Unable to locate library
Rbar_compl. (While searching for a .vos file.)
解决方法
你做了吗
opam install coq-coquelicot
？ 如果是这样
opam list coq-coquelicot
应该告诉你你有哪个版本。
这应该足以编译第一行。
对于文件 Rbar_compl.v 来自的第二行？我不认为它是一个 coquelicot 文件。
似乎您需要的文件是 here。 您首先需要编译然后才能执行文件。如果您不知道如何编译它们，请随时寻求帮助。
,这里是 Linux (Fedora) 下的一个会话，假设您已经完成了在您的机器上安装 opam 的所有工作。
首先在你的 linux 机器上，我建议你创建一个新的空目录并切换到这个目录。然后执行以下命令。 MILC这个名字可以根据你的喜好更改，这个名字是@Lolo找到的链接的一部分。
opam install coq-coquelicot
opam install coqide
eval $(opam env)
wget https://lipn.univ-paris13.fr/MILC/CoqLIntp/LInt_p.tgz
tar xfz LInt_p.tgz
echo -R . MILC > _CoqProject
echo -R . MILC > Make
ls *.v >> Make
coq_makefile -f Make -o Makefile.coq
make -f Makefile.coq
coqide -R . MILC
在 coqide 窗口中，您可以通过键入以下命令来加载所有文件。
From Coq Require Import Lia Reals Lra List.
From Coquelicot Require Import Coquelicot.
From Coq Require Import PropExtensionality FunctionalExtensionality.
From MILC Require Import Rbar_compl sum_Rbar_nonneg measurable_fun.
From MILC Require Import subset_compl R_compl sigma_algebra_R_Rbar.
From MILC Require Import sigma_algebra simple_fun LInt_p.
然后你可以通过输入看到这个发展中的定理之一
Check LInt_p_Dirac.
这条线应该可以工作：
+----+----+----+----+----+----+----+----+----+----+
|# | S| | | | | | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | | | | |l | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | | | | | | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| |l | S| | | | | | s| |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | | | |L | | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | | | | | | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | |l | | |L |S | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | | | | | | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | | | | s| | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | s|L | | | | | | | |
|abcd| | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
a's turn.
a,press <Enter> to roll.
+----+----+----+----+----+----+----+----+----+----+
|# | S| | | | | | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | | | | |l | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | | | | | | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| |l | S| | | | | | s| |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | | | |L | | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | | | | | | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | |l | | |L |S | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | | | | | | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | | | | | s| | | | |
| | | | | | | | | | |
+----+----+----+----+----+----+----+----+----+----+
| | s|L | | | | | | | |
| bcd| | | | a| | | | | |
+----+----+----+----+----+----+----+----+----+----+
a rolls a 4!
b's turn
b,press <Enter> to roll.
但这些行是可疑的。
From Coquelicot Require Import Coquelicot.
你确定有一个叫这个名字的图书馆吗？它看起来更像是库中定理的名称。不过，它们似乎没有在 Coquelicot 中定义...
您是从哪里得知应该写这些台词的？