coq/build, branch master The formal proof system Officially discontinue the experimental coq build via ocamlbuild 2016-06-08T12:32:56+00:00 Pierre Letouzey 2016-06-01T23:22:41+00:00 1d6d0060330197896748739a625d0b1c7f083da2 It has been accidentaly broken since early 2014 (and especially in 8.5), no easy repair, I won't devote any more hours to this stuff. Moreover no one seems to care apart from Emilio, but he's ok to work on this in a separate repository or branch. I left a dev/doc/ocamlbuild.txt file with a few words about this experiment. 
 It has been accidentaly broken since early 2014 (and especially
 in 8.5), no easy repair, I won't devote any more hours to this stuff.
 Moreover no one seems to care apart from Emilio, but he's ok to work
 on this in a separate repository or branch.
 I left a dev/doc/ocamlbuild.txt file with a few words about this
 experiment.
Minor fix in the ./build wrapper for ocamlbuild 2012-10-06T10:08:55+00:00 letouzey 2012-10-06T10:08:55+00:00 48b3abb2373a1bd4655f2de44f42245be4d773ac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15877 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15877 85f007b7-540e-0410-9357-904b9bb8a0f7
lib directory is cut in 2 cma. 2012-04-12T20:49:01+00:00 pboutill 2012-04-12T20:49:01+00:00 59c9403ceb09a35ed219b522e9f5abdb50615d76 - Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7 
 - Clib that does not depend on camlpX and is made to be shared by all coq
   tools/scripts/...
 - Lib that is Coqtop specific

As a side effect for the build system :
 - Coq_config is in Clib and does not appears in makefiles
 - only the BEST version of coqc and coqmktop is made
 - ocamlbuild build system fails latter but is still broken

(ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
Ocamlbuild needs OCAML_LD_LIBRARY_PATH (bug #2502) 2011-02-25T14:19:40+00:00 glondu 2011-02-25T14:19:40+00:00 51f2b9f79b92e6feee8915f311fdb75c273fabf4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13857 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13857 85f007b7-540e-0410-9357-904b9bb8a0f7
Some more adaptations for Debian-->mingw32 2010-02-26T18:13:48+00:00 letouzey 2010-02-26T18:13:48+00:00 f5c13ce06bd0f7e7d3a6e18467f5b4b88e253974 * Remove option -mwindows which isnt working : the GUI binary refuses to launch in a real windows. * simplification of ./build. New way of use : ./configure -prefix "" -arch win32 && ./build win32 This way we avoid any tricks with coq_config.ml. It is also best to avoid ./configure -local otherwise Envars.coqbin () will be wrong later. * Avoid creation of an ad-hoc coq_config in myocamlbuild.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12819 85f007b7-540e-0410-9357-904b9bb8a0f7 
 * Remove option -mwindows which isnt working : the GUI binary refuses to
   launch in a real windows.

 * simplification of ./build. New way of use :
    ./configure -prefix "" -arch win32 && ./build win32
   This way we avoid any tricks with coq_config.ml.
   It is also best to avoid ./configure -local otherwise Envars.coqbin ()
   will be wrong later.

 * Avoid creation of an ad-hoc coq_config in myocamlbuild.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12819 85f007b7-540e-0410-9357-904b9bb8a0f7
mingw32 cross-compilation: coqide.exe as a GUI program, nicer ./build script 2010-02-25T19:09:03+00:00 letouzey 2010-02-25T19:09:03+00:00 94315f7e1fb2647785d82262a669a70e0e202503 we pass -mwindows to the mingw32 linker, this allows coqide.exe to be considered as a GUI windows program instead of as a console one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12814 85f007b7-540e-0410-9357-904b9bb8a0f7 
 we pass -mwindows to the mingw32 linker, this allows coqide.exe to be
 considered as a GUI windows program instead of as a console one.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12814 85f007b7-540e-0410-9357-904b9bb8a0f7
Win32 cross-compilation from debian: build of coqide.exe and other binaries 2010-02-24T19:30:09+00:00 letouzey 2010-02-24T19:30:09+00:00 043532049cf272fd870294265707febc68d1e6a5 Details will follow. In a word, we use a gtk+ win32 bundle from gtk.org to build some (unofficial) mingw32-liblablgtk2 debian packages. Then ./configure -local && ./build win32 is enough to get all native win32 binaries and plugin cmxs from a confortable linux box. Next step: an auto-installer :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12804 85f007b7-540e-0410-9357-904b9bb8a0f7 
 Details will follow. In a word, we use a gtk+ win32 bundle from gtk.org
 to build some (unofficial) mingw32-liblablgtk2 debian packages. Then
  ./configure -local && ./build win32
 is enough to get all native win32 binaries and plugin cmxs from
 a confortable linux box.

 Next step: an auto-installer :-)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12804 85f007b7-540e-0410-9357-904b9bb8a0f7
Experimental build of coqtop.exe + plugins via cross-compilation linux-->win32 2010-02-18T18:14:50+00:00 letouzey 2010-02-18T18:14:50+00:00 c0511de2634363029307aa35a1f41539bae905d0 Ideally, just install the cross-compiler (mingw32-ocaml on debian) and launch ./configure -local && ./build win32 For the moment, this needs some twicking of mingw32-ocaml, plus a mingw32-camlp5 which is not yet distributed. If you want to play with that, contact me... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12792 85f007b7-540e-0410-9357-904b9bb8a0f7 
 Ideally, just install the cross-compiler (mingw32-ocaml on debian)
 and launch ./configure -local && ./build win32

 For the moment, this needs some twicking of mingw32-ocaml, plus
 a mingw32-camlp5 which is not yet distributed. If you want to play with
 that, contact me...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12792 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove bashisms 2010-01-28T22:10:08+00:00 glondu 2010-01-28T22:10:08+00:00 115860adb8e0054b005fe08efc45d999b2f0f3c1 As pointed out by Nima Hoda, bash is not installed everywhere... and we really don't NEED bash anyway. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12701 85f007b7-540e-0410-9357-904b9bb8a0f7 
As pointed out by Nima Hoda, bash is not installed everywhere... and
we really don't NEED bash anyway.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12701 85f007b7-540e-0410-9357-904b9bb8a0f7
Backport of Eric Le Lay's patch (bug report #2078) from v8.2 branch 2009-04-08T15:50:39+00:00 herbelin 2009-04-08T15:50:39+00:00 0cf541452e6bb56ddddfae6bd9c1e08fbd47a687 (r12063) for smooth compilation/installation under Solaris (/bin/sh -> /bin/bash, -or -> -o in find, echo -n -> printf, ! in test rather than in if). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12065 85f007b7-540e-0410-9357-904b9bb8a0f7 
(r12063) for smooth compilation/installation under Solaris (/bin/sh ->
/bin/bash, -or -> -o in find, echo -n -> printf, ! in test rather than
in if).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12065 85f007b7-540e-0410-9357-904b9bb8a0f7