From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 22DF2BC6B for ; Wed, 12 Dec 2007 18:20:59 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAJemX0fBAkMt/2dsb2JhbAA X-IronPort-AV: E=Sophos;i="4.24,157,1196636400"; d="scan'208";a="5147728" Received: from vega.fmf.uni-lj.si (HELO postar.fmf.uni-lj.si) ([193.2.67.45]) by mail2-smtp-roc.national.inria.fr with ESMTP; 12 Dec 2007 18:20:59 +0100 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 08323238F9D for ; Wed, 12 Dec 2007 18:20:58 +0100 (CET) X-Virus-Scanned: amavisd-new at spam.fmf.uni-lj.si Received: from postar.fmf.uni-lj.si ([192.168.5.5]) by localhost (spam.fmf.uni-lj.si [192.168.5.1]) (amavisd-new, port 10024) with ESMTP id ej3fGYn7GvRe for ; Wed, 12 Dec 2007 18:20:57 +0100 (CET) Received: from [10.10.4.98] (katapult.fmf.uni-lj.si [193.2.67.50]) (Authenticated sender: bauer) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 9998C238F94 for ; Wed, 12 Dec 2007 18:20:57 +0100 (CET) Message-ID: <47601894.1080105@fmf.uni-lj.si> Date: Wed, 12 Dec 2007 18:21:24 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Thunderbird 1.5.0.14pre (X11/20071023) MIME-Version: 1.0 To: caml-list@yquem.inria.fr Subject: Coq 8.1 and Ocaml 3.10 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; andrej:01 andrej:01 coq:01 ocaml:01 coq:01 ocaml:01 camlp:01 compilation:01 ocamlopt:01 constr:01 cmo:01 cmx:01 constr:01 usr:01 --prefix:01 The Coq homepage seems to indicate that Coq 8.1pl2 can be compiled with Ocaml 3.10 and camlp5. I have those (installed through Godi), the configuration script for Coq is happy, see below, yet the compilation is getting 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' There is a parsing/q_constr.ml4 file which does not seem to be compiled. This happens with Godi version of Coq as well as one that I compiled "by hand". I am blaming myself and Ocaml 3.10 which is why I am posting on this list, as opposed to coq-club. Any help is appreciated. Andrej P.S. This is the result of ./configure prefix /usr/local: -------------------- $ ./configure --prefix /usr/local You have Objective-Caml 3.10.0. Good! You have native-code compilation. Good! LablGtk2 found, native threads: native CoqIde will be available. Should I compile the complete theory of real analysis [Y/N, default is Y] ? y Coq top directory : /home/andrej/compile/coq-8.1pl2 Architecture : i686 OS dependent libraries : -cclib -lunix Objective-Caml/Camlp4 version : 3.10.0 Objective-Caml/Camlp4 binaries in : /usr/local/godi/bin Objective-Caml library in : /usr/local/godi/lib/ocaml/std-lib Camlp4 library in : +camlp5 Lablgtk2 library in : +lablgtk2 FSets theory : All Reals theory : All CoqIde : opt 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 emacs mode will be copied in /usr/local/share/emacs/site-lisp /home/andrej/compile/coq-8.1pl2/theories /home/andrej/compile/coq-8.1pl2/contrib 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'. --------------------