Ssreflect Users Discussion List

[Ralph Matthes <>]

Le lundi 16 novembre 2009 à 16:01 +0100, François Garillot a écrit :
> 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.

Still, I think if I install the SVN trunk version at some times and the
current official version at other times, and this all through make world
and make install, any inconsistent installation should be avoided by the
makefiles and not by the user.

> 
> 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 only see a choice between 9.04 and 9.10. But 8.04 is the current
long-term support version.

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

Thank you. It is just not easy to guess from the INSTALL file whether
directory names have to end by a slash or not. For COQBIN, it does not
work without, but for COQTOP/COQLIB, I only guessed that it would be
meant without. And COQTOP is not the root of the source directory,
although this is what the configure script says.

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

I won't be able to do this today.

> 
> > 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 ? 

I use CoqIDE for all my Coq development. The coqide executable comes
from the same minutes as all the other installation.

The configure script showed the following output:

You have GNU Make 3.81. Good!
You have Objective-Caml 3.10.0. Good!
You have native-code compilation. Good!
LablGtk2 found, native threads: native CoqIde will be available.
Where should I install the Coq binaries [/usr/local/bin]? 
Where should I install the Coq library [/usr/local/lib/coq]? 
Where should I install the Coq man pages [/usr/local/man]? 
Where should I install the Coq documentation
[/usr/local/share/doc/coq]? 
Where should I install the Coq Emacs mode
[/usr/local/share/emacs/site-lisp]? 
Where should I install Coqdoc TeX/LaTeX files
[/usr/local/share/texmf/tex/latex/misc]? 

  Coq top
directory                 : /home/matthes/Software/coq/coq8.2/coq-8.2pl1
  Architecture                      : Linux
  Coq VM bytecode link flags        : -dllib -lcoqrun -dllpath
'/usr/local/lib/coq'
  Coq tools bytecode link flags     : 
  OS dependent libraries            : -cclib -lunix
  Objective-Caml/Camlp4 version     : 3.10.0
  Objective-Caml/Camlp4 binaries in : /usr/bin
  Objective-Caml library in         : /usr/lib/ocaml/3.10.0
  Camlp4 library in                 : +camlp5
  Lablgtk2 library in               : +lablgtk2
  FSets theory                      : All
  Reals theory                      : All
  Documentation                     : All
  CoqIde                            : opt
  Web browser                       : firefox -remote "OpenURL(%
s,new-tab)" || firefox %s &
  Coq web site                      :
http://www.lix.polytechnique.fr/coq/

  Paths for true installation:
    binaries      will be copied in /usr/local/bin
    library       will be copied in /usr/local/lib/coq
    man pages     will be copied in /usr/local/man
    documentation will be copied in /usr/local/share/doc/coq
    emacs mode    will be copied in /usr/local/share/emacs/site-lisp

If anything in the above is wrong, please restart './configure'

*Warning* To compile the system for a new architecture
          don't forget to do a 'make archclean' before './configure'.

------------

Thank you for your efforts,         Ralph