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

Question

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.)

Answer 1

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.

Answer 2

Did you do a

opam install coq-coquelicot

? If so

opam list coq-coquelicot

should tell you which version you have.

This should be sufficient to compile the first line. For the second line where the file Rbar_compl.v comes from? I don't think it is a coquelicot file.

Answer 3

This line should work:

From Coquelicot Require Import Coquelicot. 

But these lines are suspect.

Require Import Rbar_compl. 
Require Import sum_Rbar_nonneg. 

Are you sure there is a library with that name? It looks more like the names of theorems inside a library. They don't seem to be defined in Coquelicot, though...

From where did you learn that you should write those lines?

Answer 4

seems the files you need are here. You first need to compile then before being able to execute the file. Don't hesitate to ask for help if you don't know how to compile them.