aboutsummaryrefslogtreecommitdiff
path: root/scripts/coqmktop.ml
AgeCommit message (Collapse)Author
2013-04-18coqc and coqmktop migrated in tools/, get rid of scripts/ subdirletouzey
No need to place these binaries apart, and anyway they aren't (shell) scripts since ages. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16432 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Coqmktop: dynlink is now mandatory due to Maxime's native-compilerletouzey
Some cleanup btw, for instance Dynlink.init is deprecated since at least ocaml 3.11 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16419 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 11)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16287 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22Revert "remove -rectypes except for term.ml"mdenes
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
2013-01-12Coqmktop and camlp4 : sequel to commit 16113letouzey
Actually I don't see any reason to link q_utils and q_coqast in coqtop.byte specifically when using camlp4 (and not camlp5). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16121 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-22Avoiding collision between Camlp4 Loc.Exc_located and Coq's Loc.Exc_located.herbelin
Also fixing coqmktop for use with Camlp4. Don't know if this is the fix intended by coqmktop experts or not, though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16113 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-08Ensure that a function declared with a label is used with itletouzey
This correspond to ocaml4 warning 6 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16053 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Coqmktop: use the atomic Filename.open_temp_fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16016 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-23Coqmktop: missing -I (fix #2851)letouzey
The modules used in coqmktop's temporary main file should have their .cmi in the search path, hence a small set of -I is required: lib, toplevel. We do not place their the full list to avoid issues with the win32 command-line length Btw, coqmktop -boot now also builds its list of -I instead of receiving them via its command-line, it's simpler this way... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15926 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06Coqmktop: a misplaced Filename.quote prevented temp file cleanupletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15880 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06remove -rectypes except for term.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Port from 8.4 branch some build fixes concerning win32 :letouzey
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
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06Win32: some quote fixesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15688 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12Coq should compile with Ocaml4 and/or lablgtk installed with ocamlfindpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15603 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-12lib directory is cut in 2 cma.pboutill
- 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
2012-03-02Noise for nothingpboutill
Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-14Bug 2637: patches to make slightly easier to write programs that use coq ↵pboutill
code, without the toplevel. by Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14651 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-20Fix typo in coqmktop helpglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14288 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-12remove old traces of SearchIsos (never ported to 7.x nor 8.x)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13986 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-07Coqide is not built with coqmktop any morepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13777 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-18Now prints an error instead of an anomaly when dynlink failsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13430 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
See http://caml.inria.fr/mantis/view.php?id=4940 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13413 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-19Removing unexpected printing of debug output (see bug report #2271).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12874 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
* 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
2009-03-20replaced dir_load by load_file because dir_load does not raise an exception ↵barras
when loading fails git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12000 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-31Reorder coqmktop options and document -echoglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11875 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-10- Fixed the recompilation of config/revision.ml once every two conmpilations.herbelin
- Fixed an error message in configure - Support for filenames with spaces in coqmktop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11772 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-06Installation des librairies: on utilise maintenant LINKCMO au lieu denotin
l'appel à find. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11753 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-19Execute #rectypes directive in embedded OCaml toplevel...glondu
...to avoid the need to have cflags.cmi around. This directive will likely be available in the next version of OCaml. See OCaml bug #4460. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11605 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-29Remove calls to Dynlink.add_{interfaces,available_units} altogetherglondu
According to OCaml's Changes, all modules loaded so far (and statically linked) are available to dynamically loaded modules (since 3.07). Therefore, these calls seem irrelevant now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11522 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-28Native "Declare ML Module" when possibleglondu
Dynlink.add_{interfaces,available_units} are deprecated and not implemented natively. Currently, native "Declare ML Module" doesn't work because of this. Dynlink-related should be switched to the API introduced in OCaml 3.07. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11518 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-05Parametrize link flags for VM-dependent bytecodeglondu
* Remove unneeded -custom flags. * Replace needed ones by a configure parameter. Setting it to "-dllib -lcoqrun" enables the creation/usage of pure bytecode executable provided the so/dll with the VM is found by ocamlrun. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11363 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-08forgotten debug printf in coqmktop (anyway, can be obtained by -echo)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11215 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-19Intégration de micromega ("omicron" pour fourier et sa variante sur Z,herbelin
"micromega" et "sos" pour les problèmes non linéaires sous-traités à csdp); mise en place d'un cache pour pouvoir rejouer les preuves sans avoir besoin de csdp (pour l'instant c'est du bricolage, faudra affiner cela). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10947 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-09Des choses bizarres avec pa_op.cmo (extension syntaxique pour parser)herbelin
se passent avec camlp5 qui ne se passaient pas avec l'ancien camlp4: pa_op.cmo exige camlp5o.cma mais alors, il y a un message de redéfinition de ipatt que je ne sais pas éviter avec coqtop.byte. Puisque pa_op.cmo n'est finalement pas utile, on le retire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10646 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-06Oups. Clflags.recursive_types isnt normally accessible on a standard ocaml ↵letouzey
installation. Backtrack for the moment. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10292 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-05For debugging with coqtop.byte with ocaml 3.10, the toplevel should be made ↵letouzey
with -rectypes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10288 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey
the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-29Plus d'option -v8 dans coqmktopherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9813 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-17Correction bug #1282herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9495 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-14Modification de l'appel aux exécutables Camlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9135 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Suite ajout option -ocamlib à configurenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9115 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:32:23 +0000