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.9 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 6CDE7BC6B for ; Wed, 12 Dec 2007 18:33:02 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAABuqX0dC+Vysi2dsb2JhbACPbQEBAQgEBCQF X-IronPort-AV: E=Sophos;i="4.24,157,1196636400"; d="scan'208";a="20249932" Received: from ug-out-1314.google.com ([66.249.92.172]) by mail4-smtp-sop.national.inria.fr with ESMTP; 12 Dec 2007 18:33:02 +0100 Received: by ug-out-1314.google.com with SMTP id k40so637367ugc.18 for ; Wed, 12 Dec 2007 09:33:01 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:user-agent:mime-version:to:cc:subject:references:in-reply-to:content-type:content-transfer-encoding:sender; bh=l68Yp3yN5me7UD4xYJ2OT0rxJ545M84VwOtUaGSEniU=; b=MyI2nvLXuMrz+L0Rruh21chzPZxXlTpiy3qAEr0F/JMmJ8mlm917BNF8QBEuaIHIjmluL6EaIeGSLx3VZdCMhJHQQugojKsnoad4Z2asfloadQpnOYBZRqeKUWlGgoVzVLsw/xw7EIPlDI729znbCd6RtpyHc3J+9pcmPqvFYJ8= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:user-agent:mime-version:to:cc:subject:references:in-reply-to:content-type:content-transfer-encoding:sender; b=NqqVjVZohCNY9vscn8zNGNfBYkbffH6sHjeXSzZ+LctYT/w3Vip6CRmTpMJVn+35ACuZuoRN2f1DNKbNGBIwyxJ5+mhukc4XhXd3OwyKhXgfQVgEx9bGAy8Bq0c+uvJgRnjoLxUG8kez/DJmGlBopwB6C3fqbE4KlXZbnGDmhvc= Received: by 10.67.115.4 with SMTP id s4mr2450416ugm.41.1197480778079; Wed, 12 Dec 2007 09:32:58 -0800 (PST) Received: from ?192.168.0.3? ( [87.88.165.197]) by mx.google.com with ESMTPS id p34sm4227878ugc.2007.12.12.09.32.54 (version=SSLv3 cipher=RC4-MD5); Wed, 12 Dec 2007 09:32:56 -0800 (PST) Message-ID: <47601B45.5090503@lix.polytechnique.fr> Date: Wed, 12 Dec 2007 18:32:53 +0100 From: Arnaud Spiwack User-Agent: Thunderbird 2.0.0.9 (Windows/20071031) MIME-Version: 1.0 To: Andrej.Bauer@andrej.com Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Coq 8.1 and Ocaml 3.10 References: <47601894.1080105@fmf.uni-lj.si> In-Reply-To: <47601894.1080105@fmf.uni-lj.si> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Sender: Arnaud Spiwack X-Spam: no; 0.00; lix:01 coq:01 ocaml:01 bug:01 camlp:01 bug:01 ocaml:01 coq:01 makefile:01 constr:01 cmo:01 dependencies:01 andrej:01 camlp:01 compilation:01 Hi, This bug seems to have nothing to do with camlp4/5. I've seen this bug twice before, with two different version of OCaml (3.09.3 and 3.09.2 namely), but always Coq 8.1pl2. It's rare, and I have no clue why they occur. One solution is to move to the trunk version of Coq (whose Makefile has been reengineered, and is far less surprising). If you insist on keeping 8.1pl2, then here is a way to work around it : First do a : make world when it stops, do : make parsing/q_constr.cmo to build the missing file, then do : make worldnodep Which should build everything but not clean the installation (as make world do before building the dependencies). Arnaud Spiwack Andrej Bauer a écrit : > 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'. > -------------------- > > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > >