The Coq mailing list

[Virgile Prevosto <virgile.prevosto AT m4x.org>]

Hello Andrej,

Le mer 12 déc 2007 23:04:14 CET,
Andrej Bauer 
<Andrej.Bauer AT fmf.uni-lj.si>
 a écrit :

> The ./configure script is happy (see below) but the compilation gets
> stuck on:
> 
>  OCAMLOPT4 tactics/hipattern.ml4
>  Error while loading "parsing/q_constr.cmo": file not found in path.
>  Preprocessor error
>  make[1]: *** [tactics/hipattern.cmx] Error 2
>  make[1]: Leaving directory `/home/andrej/compile/coq-8.1pl2'

This looks a lot like my last installation of Coq. Your configure
script might not be as happy as it seems, especially if your system 
shell is not bash: there is one test written in bash-specific syntax
([[ ... ]] instead of [ ... ]). Normally, this is fixed in the svn
version of coq. The godi package should have provided a patch too, but
my hard disk decided against it. This should be corrected by Monday. If
you can't wait that long, I don't recall exactly where the bashism is
located in the configure script, but your config.log should. 

Hope this helps,
-- 
E tutto per oggi, a la prossima volta.
Virgile