Ssreflect Users Discussion List

[(François Garillot)]

Ralph Matthes wrote today: 

> Le lundi 16 novembre 2009 à 11:40 +0100, François Garillot a écrit :

>> > Again, I was lost. But I observed that /usr/local/lib/coq contains
>> > subdirectories from quite different dates which, to my mind, shows that
>> > the Coq build and install routines are buggy. Did you ever come across
>> > that problem?
>> 
>> Frequently. It means that coqide.cmi is not valid according to the
>> current version of the OCaml compiler. You may have several unclean
>> Ocaml or Coq installations on this machine.
>
> Thank you for your confirmation. Is this worth a bug report to the Coq
> developers?

I am not sure. The way I interpret the error you get at this stage is
that there are, on your systems, two different compilations of Coq
(possibly made with different versions of Ocaml), that compete for the
/usr/local/lib/coq hierarchy. Either the recent re-compilation you made
couldn't install its files there (because of a non-writable previous
occupant), or the binary you are calling from your PATH doesn't
correspond to said recent re-compilation.

Of course, I might be wrong in that assertion: this is just the only way
I know how to interpret the error you reported. I'm sorry I can't be
more helpful than that.

Notice that, since you are running Ubuntu, you can find a package
(albeit without manual) for ssreflect that will allow you to install the
whole compilation chain coherently through apt/aptitude. It's native in
karmic, and can be found for previous Ubuntu versions in the
maintainer's ppa:

https://launchpad.net/~glondu/+archive/ppa

(the link explains how to set up your sources.list)

> I am sorry, but the INSTALL file did not tell me to set these variables.
> Those settings are under the proviso "If your installation of Coq is not
> standard". Are the following settings the intended ones?
>
> echo $PATH $COQTOP $COQLIB $COQBIN
> yields
> /usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games 
> /usr/local/lib/coq /usr/local/lib/coq /usr/local/bin/

Yes, they are. I apologize if I've been unclear.

Perhaps you should try compiling your Coq files locally, by adding the
option -local to the configure script of the Coq distribution. You would
then have compiled files contained in this fixed location, to which you
could point the 'quatuor' of PATH/COQBIN/COQTOP/COQLIB there, in order
to call this specific version of (ssr)coq, with these libraries,
independently of whatever else is on your system.

> The previous error Unbound value Coqide.start remains.

This error was previously encountered by users who had a binary
installation of coq that did not include the ide, or a compiled source
version of coq for which the ide could not be compiled (because, e.g. of
missing libraries such as lablgtk2). Are you sure you achieved a proper
recompilation of Coq that *include* the IDE ? what was the output of the
configure script ? 

> The Coq developers warned my that Ubuntu identifies /bin/sh with the
> dash shell. Can this play a role here?

I don't think so.

-- 
François Garillot