Ssreflect Users Discussion List

[(François Garillot)]

Ralph Matthes wrote 2 days ago: 

> However, already executing
> coq_makefile -f Make -o Makefile 
> leads to the following
> Warning: install target will copy files at the first level of the coq
> contributions installation directory; option -R is recommended
> I ignored this warning since I do not understand what option -R could do
> for me.

This is non-consequential.

> Now, in the subdirectory src, the command
> coqmktop -ide -opt ssreflect.cmx -o ../bin/ssrcoqide
> generates the following output:
>
> File "/tmp/coqmaine4f218.ml", line 1, characters 0-1:
> Error: /usr/local/lib/coq/ide/coqide.cmi
> is not a compiled interface
>
> 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.

> I deleted all of the contents of /usr/local/lib/coq and did make world
> and make install again for Coq. I deleted the ssreflect source directory
> and unpacked the tgz file again. Compilation worked again, but
> coqmktop -ide -opt ssreflect.cmx -o ../bin/ssrcoqide
> generates the following different error message:
>
> File "/tmp/coqmain4a0e28.ml", line 2, characters 17-29:
> Error: Unbound value Coqide.start
>
> I have a standard installation of Coq where the shell variables COQTOP,
> COQBIN and COQLIB are not set.

You should be able to continue setting the COQBIN, COQTOP and COQLIB
variables, in the way indicated in the INSTALL file of the ssreflect
tarball.

-- 
François Garillot