找不到与后缀&lt；和前缀Coquelicot匹配的绑定到逻辑路径的物理路径 [英] Cannot find a physical path bound to logical path matching suffix <> and prefix Coquelicot

问题描述

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

Opam Repo Add Coq-Releasehttps://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的所有工作，则在linux(Fedora)下有一个会话可以使一切正常工作。

首先，在您的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.

这篇关于找不到与后缀&lt；和前缀Coquelicot匹配的绑定到逻辑路径的物理路径的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！