Browse thread
gcc compilation of ocaml and native code coq in window95
- Gang CHEN
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ 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