[Caml-list] installing caml-light

[Caml-list] installing caml-light

[Marco Maggesi]

Hi everybody,

I am trying to install Caml-light with no success (from
cl75unix.tar.gz).  I made two attempts on two different machines:

  1. On a Linux Gentoo box (you can find the complete trace of the
     compilation at http://math.unice.fr/~maggesi/cl75gentoo.log)

     Problem: The Caml-light core compiles correctly but I am not able
     to compile the contributions, in particular "unix".  The precise
     error is

       make[1]: Entering directory `/home/maggesi/cl/cl75/contrib/libunix'
       gcc -I../../src/runtime -O    -c -o accept.o accept.c
       In file included from /usr/include/sys/un.h:38,
                        from socketaddr.h:4,
                        from accept.c:8:
       /usr/include/string.h:278: error: syntax error before '(' token
       /usr/include/string.h:278: error: syntax error before "const"
       make[1]: *** [accept.o] Error 1


  2. On a Fedora (with Intel Xeon).

     The bootstrap do not reach the fixpoint:

       camlcomp compiler/camlcomp differ: byte 69072, line 288



The only reason I have to compile Caml-light is that I would like to
give a try to HOL-light, the prover of John Harrison.  How hard is to
translate a Caml-light program into an OCaml program?

Thanks for any help,

  -- M

-------------------
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

Re: [Caml-list] installing caml-light

[David MENTRE]

Hello Marco,

Marco Maggesi <maggesi@math.unice.fr> writes:

> How hard is to translate a Caml-light program into an OCaml program?

I would say not that hard. Replace "__" by "." for module call. But I've
never done this exercise myself so I might have overlooked more tricky
points.

Yours,
d.
-- 
 David Mentré <dmentre@linux-france.org>

-------------------
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

Re: [Caml-list] installing caml-light

[William Lovas]

Hi Marco,

On Fri, Jun 18, 2004 at 04:44:00PM +0000, Marco Maggesi wrote:
> The only reason I have to compile Caml-light is that I would like to
> give a try to HOL-light, the prover of John Harrison.  How hard is to
> translate a Caml-light program into an OCaml program?

You might be interested in the last question answered at

    http://caml.inria.fr/ocaml/bigpicture.html

entitled, "How hard is it to convert code from Caml Light to Objective
Caml?"  It even has a pointer to an automatic translator!

Hope this helps.

cheers,
William

-------------------
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

Re: [Caml-list] installing caml-light

[Michel Quercia]

Le vendredi 18 Juin 2004 18:44, Marco Maggesi a écrit :
> Hi everybody,
>
> I am trying to install Caml-light with no success (from
> cl75unix.tar.gz).  I made two attempts on two different machines:
>
>   1. On a Linux Gentoo box (you can find the complete trace of the
>      compilation at http://math.unice.fr/~maggesi/cl75gentoo.log)
>
>      Problem: The Caml-light core compiles correctly but I am not able
>      to compile the contributions, in particular "unix".  The precise
>      error is
>
>        make[1]: Entering directory `/home/maggesi/cl/cl75/contrib/libunix'
>        gcc -I../../src/runtime -O    -c -o accept.o accept.c
>        In file included from /usr/include/sys/un.h:38,
>                         from socketaddr.h:4,
>                         from accept.c:8:
>        /usr/include/string.h:278: error: syntax error before '(' token
>        /usr/include/string.h:278: error: syntax error before "const"
>        make[1]: *** [accept.o] Error 1

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 <errno.h>" when not already present.

-- 
Michel Quercia
23 rue de Montchapet, 21000 Dijon
http://michel.quercia.free.fr (maths)
http://pauillac.inria.fr/~quercia (informatique)
mailto:michel.quercia@prepas.org

-------------------
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

[Caml-list] Re: installing caml-light

[Marco Maggesi]

On 2004-06-19, Michel Quercia <michel.quercia@prepas.org> 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 <errno.h>" 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