[Coq-Club] Weird import problem?

[Xuanrui Qi]

Hello all,

I appear to have run into a weird Import problem in Coq. I have
installed the "coq-equations" package using opam, but when I try to
Require Import the package:

Coq < Require Import Equations.

Require Import Equations.
^^^^^^^^^

Error: Unable to locate library Equations.

However, if I issue the "Print LoadPath." command, I can see that
Equations is in the load path!

Coq < Print LoadPath.
Logical Path / Physical path:
<> /home/xuanrui
<> /home/xuanrui/.opam/4.07.0/lib/coq/user-contrib
Equations /home/xuanrui/.opam/4.07.0/lib/coq/user-contrib/Equations

I also have ssreflect installed the same way, and I have no problems
importing ssreflect. I wonder what could be going wrong with Coq, or
perhaps it is a problem in the packaging of Equations?

Thanks a lot for your assistance.

-Ray

[Li-yao Xia]

Hi Xuanrui,

Try

Require Import Equations.Equations.

Looking at the "Print LoadPath" output, "Equations" is the path to the
Equations library, but that is not a path to an actual file, which
"Require" expects.

The logical path "Equations.Equations" refers to the module
.../user-contrib/Equations/Equations.vo which can thus be loaded.

Li-yao

Post by Xuanrui Qi
Hello all,
I appear to have run into a weird Import problem in Coq. I have
installed the "coq-equations" package using opam, but when I try to
Coq < Require Import Equations.

Post by Xuanrui Qi
Require Import Equations.
^^^^^^^^^

Error: Unable to locate library Equations.
However, if I issue the "Print LoadPath." command, I can see that
Equations is in the load path!
Coq < Print LoadPath.
<> /home/xuanrui
<> /home/xuanrui/.opam/4.07.0/lib/coq/user-contrib
Equations /home/xuanrui/.opam/4.07.0/lib/coq/user-contrib/Equations
I also have ssreflect installed the same way, and I have no problems
importing ssreflect. I wonder what could be going wrong with Coq, or
perhaps it is a problem in the packaging of Equations?
Thanks a lot for your assistance.
-Ray

[Xuanrui Qi]

Hello,

Thanks to Li-yao. This is right - the documentation needs to be
updated, I think!

Best,
Ray

Post by Li-yao Xia
Hi Xuanrui,
Try
Require Import Equations.Equations.
Looking at the "Print LoadPath" output, "Equations" is the path to the
Equations library, but that is not a path to an actual file, which
"Require" expects.
The logical path "Equations.Equations" refers to the module
.../user-contrib/Equations/Equations.vo which can thus be loaded.
Li-yao

Post by Xuanrui Qi
Hello all,
I appear to have run into a weird Import problem in Coq. I have
installed the "coq-equations" package using opam, but when I try to
Coq < Require Import Equations.

Post by Xuanrui Qi
Require Import Equations.
^^^^^^^^^

Error: Unable to locate library Equations.
However, if I issue the "Print LoadPath." command, I can see that
Equations is in the load path!
Coq < Print LoadPath.
<> /home/xuanrui
<> /home/xuanrui/.opam/4.07.0/lib/coq/user-contrib
Equations /home/xuanrui/.opam/4.07.0/lib/coq/user-contrib/Equations
I also have ssreflect installed the same way, and I have no
problems
importing ssreflect. I wonder what could be going wrong with Coq, or
perhaps it is a problem in the packaging of Equations?
Thanks a lot for your assistance.
-Ray

[Anton Trunov]

Hi Ray,

Yet another option is to use

From Equations Require Import Equations.

This is what the manual uses at the beginning of chapter 1, see
http://github.com/mattam82/Coq-Equations/raw/master/doc/equations.pdf

Best wishes,
Anton

Post by Xuanrui Qi
Hello,
Thanks to Li-yao. This is right - the documentation needs to be
updated, I think!
Best,
Ray

Post by Li-yao Xia
Hi Xuanrui,
Try
Require Import Equations.Equations.
Looking at the "Print LoadPath" output, "Equations" is the path to the
Equations library, but that is not a path to an actual file, which
"Require" expects.
The logical path "Equations.Equations" refers to the module
.../user-contrib/Equations/Equations.vo which can thus be loaded.
Li-yao

Post by Xuanrui Qi
Hello all,
I appear to have run into a weird Import problem in Coq. I have
installed the "coq-equations" package using opam, but when I try to
Coq < Require Import Equations.

Post by Xuanrui Qi
Require Import Equations.
^^^^^^^^^

Error: Unable to locate library Equations.
However, if I issue the "Print LoadPath." command, I can see that
Equations is in the load path!
Coq < Print LoadPath.
<> /home/xuanrui
<> /home/xuanrui/.opam/4.07.0/lib/coq/user-contrib
Equations /home/xuanrui/.opam/4.07.0/lib/coq/user-contrib/Equations
I also have ssreflect installed the same way, and I have no
problems
importing ssreflect. I wonder what could be going wrong with Coq, or
perhaps it is a problem in the packaging of Equations?
Thanks a lot for your assistance.
-Ray