From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 3313CBB81 for ; Fri, 2 Dec 2005 01:34:15 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id jB20YEka019270 for ; Fri, 2 Dec 2005 01:34:14 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id BAA16002 for ; Fri, 2 Dec 2005 01:34:14 +0100 (MET) Received: from iron.cat.pdx.edu (iron.cat.pdx.edu [131.252.208.92]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id jB20YCV2019267 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Fri, 2 Dec 2005 01:34:13 +0100 Received: from rastaban.cs.pdx.edu (root@rastaban.cs.pdx.edu [131.252.209.214]) by iron.cat.pdx.edu (8.13.1/8.13.1) with ESMTP id jB20Xktf000495 (version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=NO) for ; Thu, 1 Dec 2005 16:33:51 -0800 (PST) Received: from rastaban.cs.pdx.edu (suzannew@localhost [127.0.0.1]) by rastaban.cs.pdx.edu (8.12.10/8.12.6) with ESMTP id jB20XgbX008377 for ; Thu, 1 Dec 2005 16:33:42 -0800 (PST) Received: (from suzannew@localhost) by rastaban.cs.pdx.edu (8.12.10/8.12.6/Submit) id jB20Xgeb008376 for caml-list@inria.fr; Thu, 1 Dec 2005 16:33:42 -0800 (PST) Date: Thu, 1 Dec 2005 16:33:42 -0800 (PST) From: Suzanne Wood Message-Id: <200512020033.jB20Xgeb008376@rastaban.cs.pdx.edu> To: caml-list@inria.fr Subject: ocaml-3.08.3 for blast model checker X-Virus-Scanned: by amavisd-new X-Miltered: at concorde with ID 438F9686.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 438F9684.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; ocaml-:01 3.08.3:01 model:01 checker:01 ocaml-:01 3.09.0,:01 3.08.3:01 model:01 checker:01 implements:01 ocaml:01 ocaml:01 gcc:01 gcc:01 otherlibs:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 Having had no problem installing ocaml-3.09.0, it looks like I need to install ocaml-3.08.3 for use with the UC Berkeley Blast software model checker, per the following advisory: "Release note: We have to distribute one part of Blast precompiled (the foci library, which implements the craig interpolation), because the code is copyrighted by Cadence labs, Berkeley. Unfortunately, this precompiled piece is not compatible with OCaml 3.08.04. A working example configuration for compiling Blast 2.0 is OCaml 3.08.3 and gcc (GCC) 3.4.4 20050721 (Red Hat 3.4.4-2). --Dirk 2005-10-18" But, in trying to compile ocaml-3.08.3, "make world" dies with: make[1]: Leaving directory ` /ocaml-3.08.3/otherlibs/str' make[1]: Entering directory ` /ocaml-3.08.3/otherlibs/num' gcc -O -I../../byterun -fno-defer-pop -Wall -D_FILE_OFFSET_BITS=64 -D_REENTRANT -fPIC -DBNG_ARCH_ia32 -DBNG_ASM_LEVEL=2 -c -o bng.o bng.c In file included from bng.c:21: bng_ia32.c: In function ‘bng_ia32_mult_sub_digit’: bng_ia32.c:153: error: can't find a register in class ‘GENERAL_REGS’ while reloading ‘asm’ make[1]: *** [bng.o] Error 1 make[1]: Leaving directory ` /ocaml-3.08.3/otherlibs/num' make: *** [otherlibraries] Error 2 Thank you for any suggestion about how to proceed.