1

我最近用 opam 安装了 Coq 版本 8.12.2。我已经使用以下命令安装了 Coq 的所有软件包：

opam repo 添加 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.)
4

4 回答 4

1

你做了一个

opam install coq-coquelicot

? 如果是这样

opam list coq-coquelicot

应该告诉你你有哪个版本。

这应该足以编译第一行。对于文件Rbar_compl.v 来自的第二行？我不认为它是一个coquelicot文件。

于 2021-04-20T18:07:55.900 回答
1

看来你需要的文件在这里。您首先需要编译然后才能执行该文件。如果您不知道如何编译它们，请随时寻求帮助。

于 2021-04-21T16:14:14.923 回答
1

这是一个在 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.
于 2021-04-21T16:53:29.453 回答
0

这条线应该工作：

From Coquelicot Require Import Coquelicot.

但这些线是可疑的。

Require Import Rbar_compl. 
Require Import sum_Rbar_nonneg.

你确定有一个同名的图书馆吗？它看起来更像是库中定理的名称。不过，它们似乎没有在 Coquelicot 中定义……

你从哪里得知你应该写那些行？

于 2021-04-21T16:05:09.327 回答