Search code examples
coqcoqide

Cannot find a physical path bound to logical path matching suffix <> and prefix Coquelicot

I've recently installed Coq version 8.12.2 with opam. I have installed all the packages of Coq using the following command :

opam repo add coq-released https://coq.inria.fr/opam/released

But when I try to compile packages in Coqide, it doesn't recognize 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.

I receive these errors :
Cannot find a physical path bound to logical path matching suffix <> and prefix Coquelicot

And

Unable to locate library
Rbar_compl. (While searching for a .vos file.)
Solution

  • Here is a session under Linux (Fedora) that makes it all work, assuming that you already did all the work to have opam installed on your machine.

    First in your linux machine, I advise that you create a new empty directory and change to this directory. Then you perform the following commands. The name MILC can be changed to your liking, this name is part of the link that @Lolo found.

    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

    In the coqide window, you can load all the files by typing the following command.

    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.

    Then you can see one of the theorems inside this development by typing

    Check LInt_p_Dirac.