From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA17878; Mon, 21 Jun 2004 17:53:16 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 RAA17805 for ; Mon, 21 Jun 2004 17:53:15 +0200 (MET DST) Received: from main.gmane.org (main.gmane.org [80.91.224.249]) by concorde.inria.fr (8.12.10/8.12.10) with ESMTP id i5LFrESH032486 for ; Mon, 21 Jun 2004 17:53:14 +0200 Received: from list by main.gmane.org with local (Exim 3.35 #1 (Debian)) id 1BcR6d-0007Uj-00 for ; Mon, 21 Jun 2004 17:53:13 +0200 Received: from pcmath208.unice.fr ([134.59.10.208]) by main.gmane.org with esmtp (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 21 Jun 2004 17:53:11 +0200 Received: from maggesi by pcmath208.unice.fr with local (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Mon, 21 Jun 2004 17:53:11 +0200 X-Injected-Via-Gmane: http://gmane.org/ To: caml-list@inria.fr From: Marco Maggesi Subject: [Caml-list] Re: installing caml-light Date: Mon, 21 Jun 2004 15:53:09 +0000 (UTC) Message-ID: References: <200406190852.03332.michel.quercia@prepas.org> X-Complaints-To: usenet@sea.gmane.org X-Gmane-NNTP-Posting-Host: pcmath208.unice.fr User-Agent: slrn/0.9.8.0 (Linux) X-Miltered: at concorde with ID 40D7046A.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; maggesi:01 maggesi:01 unice:01 2004:99 quercia:01 quercia:01 prepas:01 runtime:01 memcpy:01 memcpy:01 triggers:01 libunix:01 errno:01 extern:01 errno:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On 2004-06-19, Michel Quercia wrote: > > There is a micmac in the src/runtime/config.h file. Comment out (or fix) the > definition of bcopy : > > --------------------------------------------------------------------------------- > #ifdef HAS_MEMMOVE > #define bcopy(src,dst,len) memmove((dst), (src), (len)) > #else > #ifdef HAS_BCOPY > /* Nothing to do */ > #else > #ifdef HAS_MEMCPY > #define bcopy(src,dst,len) memcpy((dst), (src), (len)) > #else > #define bcopy(src,dst,len) memmov((dst), (src), (len)) > #define USING_MEMMOV > #endif > #endif > #endif > --------------------------------------------------------------------------------- > > On Linux bcopy is already defined and the redefinition above triggers this > (strange) error when HAS_MEMMOVE is set. > > You will encounter another problem later when compiling libunix related to > errno which is a macro and no longer an external variable. The fix for this > is to remove all declarations "extern int errno" in libunix/*.c files and add > "#include " when not already present. Thanks to everyone who replied to my message. I was able to compile caml-light and use HOL-light following the above suggestions. Regarding HOL-light: I found an OCaml version of HOL-light http://www.math.pitt.edu/~thales/flyspeck/hol_light.tar.gz from the page of the Flyspeck Project: http://www.math.pitt.edu/~thales/flyspeck/index.html -- Marco ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners