Version française
Home     About     Download     Resources     Contact us    
Browse thread
gcc compilation of ocaml and native code coq in window95
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Gang CHEN <Chen.Gang@e...>
Subject: gcc compilation of ocaml and native code coq in window95
I find that compilation of ocaml in window95 by using gcc is possible. I
have realized such compilation with  cygnus tool kit.  In configuration,
arch is set to linux. 

This ocaml has all unix library functions. For example, you can use
Unix.fork, etc. Both native code ocamlc and ocamlopt are compiled. 
Using this ocaml, I have compiled camlp4 and coq6.2, including native
code camlp4 and coq. 

The compilation needs several modifications to the original distribution
of ocaml. The main points are:

1. set EXE=.exe in the configuration
2. remove the use of _Win32 variables in .c files. (I am not sure all
consequences of this modification, but if you do not do this, there will
be some errors. I would like some experts to give comments on this. )
3. copy linux gcc include files to the /usr/include directory. (there
are no un.h in cygnus gcc library).
4. In emit.ml and i386.s, make global variables  prefixed by _. (in the
assemble code, linux_elf does not prefix variables by _, but win32 does
it). 

One aspect that I am not quite satisfactory is the implementation of
Sys.command. It calls command in the Cygnus bash shell. But Cygnus does
not always well execute dos commands. This will give some trouble when
using -pp preprocessing in ocamlc. It might be possible to implement
Sys.command so that it calls Dos shell command, as done in the official
ocaml implemantation. But, then, I am not be able to compile the native
code ocaml. 

Graphic library has not been compiled.

Compilations of camlp4 and coq also need some modifications to the
original distributions. 

I find that ocaml source distribution is well organized and commented so
it is relatively easy to find where we need to modify.

This compilation shows that Cygnus is powerful. But it is not stable
yet. It makes my computer dead many times, especially in the compilation
of camlp4.  Execution of some Dos program does not generate identical
output as executed in Dos.  So when you redirect this output, as needed
in the preprocessing of ocaml, there will be problem. 

Your suggestions and questions are wellcome.

Gang Chen
DMI-ENS
email: gang@dmi.ens.fr