The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 28/12/2011 10:27, Beta Ziliani a écrit :
> I'm having problems with the ML top level: I cannot do anything useful
> (not even go back to Coq).
> [...]
> # go();;
> Error: Unbound value go
> 
> It seems like it's not loading any Coq source but I don't see what I'm
> doing wrong. [...]

You have to issue "#directory" directives first:

  #directory "/usr/lib/coq/interp";;
  #directory "/usr/lib/coq/kernel";;
  #directory "/usr/lib/coq/lib";;
  #directory "/usr/lib/coq/library";;
  etc.

one for each directory containing the .cmi file of a module you want to
access (adapt /usr/lib/coq/ accordingly). With zsh, you can generate a
"directories" file with the following command:

for u in $COQROOT/**/*.cmi; do echo '#directory "'"${u%/*}"'";;'; done |
sort -u > directories

Then, you can run '#use "directories";;' before running commands from
e.g. dev/include.

It seems that #directory are implicit for each "-I" given when linking
coqtop.byte, which may explain why you don't have to run them when the
source tree is still there.


Cheers,

-- 
Stéphane