aboutsummaryrefslogtreecommitdiffhomepage
path: root/myocamlbuild.ml
Commit message (Collapse)AuthorAge
* Revert "remove -rectypes except for term.ml"Gravatar mdenes2013-01-22
| | | | | | | | | | Preparing landing of the native compiler, which requires -rectypes flag. This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16135 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: get rid of threads, use gtk asynchronous i/o insteadGravatar letouzey2012-12-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Threads were only there to handle blocking dialogs with the different coqtops. But programming with threads have drawbacks : complex mutex infrastructure, possible deadlocks, etc. In particular gtk functions are not meant to be called from a thread which isn't the gtk main loop, (unless some gtk mutex have been taken). This seem to pose problem specifically in win32 (and macosx ?), hence the use of the GtkThread.(a)sync hack for scheduling code for execution in the gtk main loop. Instead, we now use the Glib.Io module to install a callback that will be runned when some answer of coqtop is available on the channel. This implies using now a continuation-passing style: for instance, instead of two sequential requests to coqtop, we'll now have the 2nd request inside the callback handling the answer to the 1st request. Remarks: - Also use asynchronous i/o for external commands (editor, coqc, make...). Launching an external editor or browser won't freeze coqide anymore. - Reworked handling of coqtop process, especially when closing them. A responsive coqtop should now hara-kiri immediatly when its input channel is closed. Otherwise we try later a soft kill, then some hard kills if necessary. If nothing work we warns the user. When quitting coqide, all this might induce a small delay (2s at worse). - Be careful now to avoid "long" computations (or blocking i/o) in a coqide function. Experimentally, it seems that loading/saving a .v file is quick enough. If necessary, we could use asynchronous i/o also for writing the .v, but for loading I've no clue. - In the Coqide module, we ensure that the current continuation k will indeed be run at the end thanks to an abstract return type (void = opaque copy of unit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Turn mltop.ml4 into a regular ocaml fileGravatar letouzey2012-10-06
| | | | | | | | | | | | | | | | | | The IFDEF's in mltop.ml4 were there to support platforms with a native ocaml compiler but no dynlink.cmxa, a situation that should be pretty rare in the Coq community nowadays (playing with coqtop on ARM, anyone ?). So we now refuse to build a native coqtop unless dynlink.cmxa exists (cf ./configure), and we explain how to create a dummy one if necessary (cf dev/dynlink.ml). This way, we can clean-up mltop.ml, and remove ugly special rules in Makefile and myocamlbuild NB: I checked that this shouldn't have any impact on Coq's debian packages on exotic architectures (arm, mips, ...), since apparently on these architectures no ocamlopt at all are shipped, and coq packages are already byte-only git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15879 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild simplificationsGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15878 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove -rectypes except for term.mlGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
* myocamlbuild : fixes for new printing directory + sourceview for coqideGravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15754 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
| | | | | | | | For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "when cross-compiling with mingw32, let's fix the Filename.dir_sep"Gravatar letouzey2012-08-23
| | | | | | | This was merely cosmetic after all, since recent Windows versions do tolerate paths with /. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15750 85f007b7-540e-0410-9357-904b9bb8a0f7
* Port from 8.4 branch some build fixes concerning win32 :Gravatar letouzey2012-08-23
| | | | | | | | | | | | | | r15722: - CAMLBIN was cygwin-specific, leading to issues with coqmktop - A missing Filename.quote on the temp file used in coqmktop - Try to shorten the cmdline passed to Sys.command in coqmktop: way too many includes were passed to coqmktop -boot r15724: Coqmktop: the +compiler-libs for ocaml4 is back r15725: Coqmktop: better detection of ocaml 4 and above r15739: ocamlbuild : a missing include for camlp4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15744 85f007b7-540e-0410-9357-904b9bb8a0f7
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7
* when cross-compiling with mingw32, let's fix the Filename.dir_sepGravatar letouzey2012-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15327 85f007b7-540e-0410-9357-904b9bb8a0f7
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
| | | | | | | | | | | | | | | - 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
* myocamlbuild: -DWIN32 instead of -DWin32Gravatar letouzey2011-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14849 85f007b7-540e-0410-9357-904b9bb8a0f7
* adapt myocamlbuild after changes in coqdep_boot (.beautify)Gravatar letouzey2011-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14839 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild: remove -dllpath from coqrunbyteflagsGravatar glondu2011-10-07
| | | | | | See bug #2614. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14519 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild: Fix ocamlbuild compilation for changes to configure from r14500.Gravatar glondu2011-10-07
| | | | | | | | | | | The changes to myocamlbuild.ml didn't compile. See bug #2614. Signed-off-by: Tom Prince <tom.prince@ualberta.net> Signed-off-by: Stephane Glondu <steph@glondu.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14518 85f007b7-540e-0410-9357-904b9bb8a0f7
* In Coq_config: get rid of coqsrc and make coqlib optionalGravatar glondu2011-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I assume that once Coq is installed in non-local mode and run from its installed path, sources are no longer available. The coqsrc variable doesn't make any sense, then, and its intended value can always be inferred from Sys.executable_name. Moving it to Envars.coqroot. Make coqlib optional. Currently, it is set to None only in -local mode or with ocamlbuild. When set to None, -local layout is assumed (binaries in ./bin, library in .). The behaviour should not be changed when an explicit coqlib has been given to ./configure. This commit should make it possible to run a Coq compiled with -local from anywhere (no hard-coded absolute path embedded in the executables, intermediary step to bug #2565). It WILL BREAK settings re-using source trees after installation in non-local mode (are there actual use cases for that?). Hard-coded absolute paths still remain: - in the build system, so the need to re-run ./configure after moving the source tree is still expected for now; - in coqrunbyteflags, I think we are limited by ocaml itself; - docdir. All absolute paths should be removed, ultimately. As a side-effect, simplify computing of Envars.coqbin. I don't see any good reason to keep it as a function. Disclaimers: - initialization of Sys.executable_name is not consistent across all architectures; relying so much on it might trigger bugs. I'm pretty sure something will explode if one adds arbitrary symlinks on top of that; - ocamlbuild stuff not tested. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ocamlbuild : build of fake_ideGravatar letouzey2011-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14457 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: try to properly send interrupts to coqtop on Win32Gravatar letouzey2011-04-28
| | | | | | | | | | | | | | | We use GenerateConsoleCtrlEvent(CTRL_C_EVENT,...) after having attached coqide to the console of the coqtop we want to interrupt. Two caveats: - This code isn't compatible with Windows < XP SP1. - It relies on the fact that coqide is now a true GUI app, without console by default. If for some reason the console of coqide is restored (for instance via mkwinapp -unset), strange behavior of the interrupt button is to be expected, at the very least all instances of coqtop will get Ctrl-C instead of a precise one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14077 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: a special kill function for win32Gravatar letouzey2011-04-21
| | | | | | | | | | | | This is implemented as a C external launching the TerminateProcess of the Win32 API. This should be considered as quite experimental (cf. the way we handle pid in the comment of ide_win32_stubs.c). I don't know how to emulate an interrupt (Ctrl-C), for now the two button "Restart" and "Interrupt" have the same semantics on win32 (kill the subprocess and start at top). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14044 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ocamlbuild: in win32, coqide is now a console-free app by defaultGravatar letouzey2011-04-21
| | | | | | | | | | | | | | This is an adaptation of commit 13748 in 8.3 branch Making coqide console-free can be done via a link flag given to mingw. In case of problem with this setting, I also include a script mkwinapp.ml borrowed from project OCaml-Win32 (and slightly modified to allow restoring the console as well as removing it). Use: "mkwinapp coqide.exe" to make it console-free. "mkwinapp -unset coqide.exe" to go back to usual console app. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14039 85f007b7-540e-0410-9357-904b9bb8a0f7
* Win32: let's directly make coqtop.exe and coqide.exe incorporate coq.icoGravatar letouzey2011-04-21
| | | | | | This is an adaptation of commit 13747 for 8.3 branch git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14038 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild: support again camlp5 in addition to camlp4Gravatar letouzey2011-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13984 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: more reorganisation and cleanupGravatar letouzey2011-03-25
| | | | | | | | | | | | | | | | | | | - Avoid using Util which depends on Compat and hence Camlp4 - Instead, a small Minilib module specific to coqide, which duplicate 5 functions from Util (50 lines) - some dead code removal - the coqlib variable is asked to coqtop - remove obsolete Util.check_for_interrupt This way, coqide only depends on 3 files outside ide/ : Coq_config, Flags, Ide_intf. Makefile and ocamlbuild are adapted accordingly. TODO: how should we signal coqide error, warnings, etc ? For the moment, some Printf.eprintf, some failwith. To uniformize later... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix ocamlbuild-based build systemGravatar glondu2011-01-11
| | | | | | | | | Caveat: in native code, if the executable is a symlink, Sys.executable_name points to the target of the symlink... this breaks coqide's way of locating coqtop. Workaround: make bin/coqide.opt a hardlink (or a copy) instead of a symlink. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13790 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ocamlbuild: adapt to last changes for camlp4 (use of tools/compat5*.cmo)Gravatar letouzey2010-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13280 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ocamlbuild: try to speed-up error detection in *.ml*, by byte-compiling firstGravatar letouzey2010-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13064 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ocamlbuild: various fixGravatar letouzey2010-05-19
| | | | | | | | | - transition to camlp4, with no compatibility for ocamlbuild+camlp5 (error message) - fix compilation of decl_mode : a forgotten include, and Decl_expr which is a pure .mli shouldn't be mentionned in the .mllib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive wayGravatar letouzey2010-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13017 85f007b7-540e-0410-9357-904b9bb8a0f7
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13016 85f007b7-540e-0410-9357-904b9bb8a0f7
* Myocamlbuild: slight simplification of code for .ml4Gravatar letouzey2010-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12870 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some more adaptations for Debian-->mingw32Gravatar letouzey2010-02-26
| | | | | | | | | | | | | | | * 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 scriptGravatar letouzey2010-02-25
| | | | | | | 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 binariesGravatar letouzey2010-02-24
| | | | | | | | | | | | 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-->win32Gravatar letouzey2010-02-18
| | | | | | | | | | | 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
* Mycamlbuild: change name of autogenerated file : NMake -> Nmake_genGravatar letouzey2010-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵Gravatar letouzey2009-12-09
| | | | | | | | | | | | in */*/vo.itarget On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure if you want a partial build, make a specific rule such as theories-light Beware: these vo.itarget should not contain comments. Even if this is legal for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the build of coq via ocamlbuildGravatar letouzey2009-12-08
| | | | | | | | - no more plugins/interface - a few missing files in theories.itarget - a few things required Unix now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12572 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use camlp4 to accept some specific non-exhaustive patterns in groebnerGravatar letouzey2009-07-20
| | | | | | | | The camlp4 extension "refutpat" provides a syntax let* for pattern that are non-exhaustive on purpose (e.g. let* x::l = foo in ...). A Failure is raised if the pattern doesn't match the expression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12245 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild: right symlink for csdpcertGravatar letouzey2009-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12074 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ocamlbuild: option for (not) building coqide, better log messagesGravatar letouzey2009-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12048 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ocamlbuild: improvements suggested by N. PouillardGravatar letouzey2009-04-03
| | | | | | | | | | | | | * Import of Coq_config via myocamlbuild_config.ml, instead of my get_env * As a consequence, we enrich this Coq_config with stuff that was only in config/Makefile * replace the big ugly find by some dependencies against source files * by the way: build csdpcert, with the right aliases. I've tried to escape things properly for windows in ./configure, but this isn't fully tested yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the fix script for ocamlopt -shared in MacOS 10.5 (remarks by Hugo)Gravatar letouzey2009-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12041 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)Gravatar letouzey2009-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ocamlbuild: 1st reasonably complete version (rules for binaries + plugins + vo)Gravatar letouzey2009-03-26
| | | | | | | | | | | | | | | | | | | | Dealing with .vo files was harder than anticipated (issues with coqdep_boot and the location of the .v files). Current solution cannot compete for a beauty prize, but well. Several other issues remain (see top and bottom of myocamlbuild.ml) - For the moment the coqlib / coqsrc in Coq_config is to be hacked by hand to add _build/ in it. - Parallelism is a "no go" for the moment. Ocamlbuild accepts a -j option, but it has almost no effect experimentally. (but at least it doesn't take more time than make -j1, i.e. about 14 min here, instead of about 7 for make -j2) - After a first full build, ocamlbuild is awfully slow to detect that nothing has to be redone (1 min 25 here) To be continued... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12021 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild: coqide, coqchk, a bit of .voGravatar letouzey2009-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12019 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild improvements + minor makefile fixGravatar letouzey2009-03-24
| | | | | | | | | | | * a small shell script ./build to drive ocamlbuild * rules for all the binaries (apart from coqide and coqchk) * use of ocamlbuild's Echo instead of using shell + sed + awk for generated files * Makefile: remove unused STAGE1_CMO and add bin/coqdep_boot to the list of things to "clean" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12012 85f007b7-540e-0410-9357-904b9bb8a0f7
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* generalize the use of .mllib to build all cma, not only in plugins/ * the .mllib in plugins/ now mention Bruno's new _mod.ml files * lots of .cmo enumerations in Makefile.common are removed, since they are now in .mllib * the list of .cmo/.cmi can be retreive via a shell script line, see for instance rule install-library * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not _files_ * a -I option to coqdep_boot allows to control piority of includes (some files with the same names in kernel and checker ...) This is quite a lot of changes, you know who to blame / report to if something breaks. ... and last but not least I've started playing with ocamlbuild. The myocamlbuild.ml is far from complete now, but it already allows to build coqtop.{opt,byte} here. See comments at the top of myocamlbuild.ml, and don't hesitate to contribute, either for completing or simplifying it ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 15:36:52 +0000