2

The same Linux command succeeds in one environment while it fails in another:

$ coqtop -lv test.v -I Lib

The failure I am getting is under Debian stretch and Coq v8.5

$ uname -a
Linux front 4.8.0-1-amd64 #1 SMP Debian 4.8.7-1 (2016-11-13) x86_64 GNU/Linux

$ coqtop -v
The Coq Proof Assistant, version 8.5 (June 2016)
compiled on Jun 9 2016 12:4:46 with OCaml 4.02.3

and the error message I am getting is:

Welcome to Coq 8.5 (June 2016)
Require Import libtest.
Error during initialization:
File "/home/user/dev/coq/test.v", line 1, characters 15-22:
Error: Unable to locate library libtest.

The environment under which the same command relating to the same source succeeds is:

$ uname -a 
Linux back 3.16.0-4-amd64 #1 SMP Debian 3.16.36-1+deb8u2 (2016-10-19)x86_64 GNU/...

$ coqtop
The Coq Proof Assistant, version 8.4pl4 (July 2014)
compiled on Jul 27 2014 13:34:24 with OCaml 4.01.0

The successful outcome is as follows:

Welcome to Coq 8.4pl4 (July 2014)
Require Import libtest.

Coq <

So I am trying to figure out what is going on, hoping to get an answer from this post but to no avail.

For the sake of this question, I have reduced the source code to the simplest:

test.v

Require Import libtest.

Lib/libtest.v

<empty file>

In case this matters I have recompiled the (empty) library file libtest.v in each environment.

$ cd Lib
$ coqc libtest.v
$ cd ..

Any help is gratefully appreciated.

Sven Williamson
  • 1,094
  • 1
  • 10
  • 19

2 Answers2

5

Indeed, the behaviour of -I changed between 8.4 and 8.5. In the changelog of Coq, we can find an interesting line. As hinted in the changelog and as advised by the other answer, you can use -R instead.

Community
  • 1
  • 1
eponier
  • 3,062
  • 9
  • 20
  • Thank you very much ! `coqtop -lv test.v -I Lib` can indeed be replaced by `coqtop -lv test.v -R Lib ''` or `coqtop -lv test.v -Q Lib ''`. – Sven Williamson Dec 05 '16 at 17:01
4

The following works for me (I'm using Coq 8.5pl3). Let's compile our library, putting it in the Lib namespace:

$ pwd
<...>/libtest-question
$ cd Lib
$ coqc -R . "Lib" libtest.v
$ cd ..

Then let's modify our test.v:

$ cat test.v
Require Import Lib.libtest.

and load it with

$ coqtop -R Lib Lib -l test.v

The -Q switch would work too, see the Reference manual's §14.3.3 for more detail.

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
  • Thank you very much Anton ! I somewhat arbitrarily chose to validate the other answer as it is simpler. However, your answer is showing us how to introduce namespaces which is very useful. – Sven Williamson Dec 05 '16 at 17:06
  • Thank you! eponier's answer also shows when it all started :). – Anton Trunov Dec 05 '16 at 17:10