aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_boot.ml
Commit message (Collapse)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Makefile: no bytecode compilation in make world, see make byte insteadGravatar Pierre Letouzey2017-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On a machine for which ocamlopt is available, the make world will now perform bytecode compilation only in grammar/ (up to the syntax extension grammar.cma), and then exclusively use ocamlopt. In particular, make world do not build bin/coqtop.byte. A separate rule 'make byte' does it, as well as bytecode plugins and things like dev/printers.cma. 'make install' deals only with the part built by 'make', while a new rule 'make install-byte' installs the part built by 'make byte'. IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any parallel mix of native and byte rules. These are known to crash sometimes, see below. Instead, do rather 'make -j && make -j byte'. Indeed, apart from marginal compilation speed-up for users not interested in byte versions, the main reason for this commit is to discourage any simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli, and in case of parallel build this may happen at the very moment another ocaml(c|opt) is accessing this .cmi. Until now, this issue has been handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in Makefile.build). But these hacks weren't obvious to extend to ocamlopt -pack vs. ocamlopt -pack. coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML Module influences the .v.d dependency file. Possible values are: -dyndep opt : regular situation now, depends only on .cmxs -dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a) -dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs -dyndep none : interesting for coqtop with statically linked plugins -dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d instead of extensions .cm*, so that the choice is made in the rest of the makefile (see a future commit about coq_makefile) NB: two extra mli added to avoid building unecessary .cmo during 'make world', without having to use the ocamldep -native option. NB: we should state somewhere that coqmktop -top won't work unless 'make byte' was done first
* Revert "Merge remote-tracking branch 'github/pr/229' into trunk"Gravatar Maxime Dénès2016-07-05
| | | | | | | | | This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing changes made to da99355b4d6de31aec5a660f7afe100190a8e683. Hugo asked for more discussion on this topic, and it was not in the roadmap. I merged it prematurely because I thought there was a consensus. Also, I missed that it was changing coq_makefile. Sorry about that.
* Makefile: no bytecode compilation in make world, see make byte insteadGravatar Pierre Letouzey2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On a machine for which ocamlopt is available, the make world will now perform bytecode compilation only in grammar/ (up to the syntax extension grammar.cma), and then exclusively use ocamlopt. In particular, make world do not build bin/coqtop.byte. A separate rule 'make byte' does it, as well as bytecode plugins and things like dev/printers.cma. 'make install' deals only with the part built by 'make', while a new rule 'make install-byte' installs the part built by 'make byte'. IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any parallel mix of native and byte rules. These are known to crash sometimes, see below. Instead, do rather 'make -j && make -j byte'. Indeed, apart from marginal compilation speed-up for users not interested in byte versions, the main reason for this commit is to discourage any simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli, and in case of parallel build this may happen at the very moment another ocaml(c|opt) is accessing this .cmi. Until now, this issue has been handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in Makefile.build). But these hacks weren't obvious to extend to ocamlopt -pack vs. ocamlopt -pack. coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML Module influences the .v.d dependency file. Possible values are: -dyndep opt : regular situation now, depends only on .cmxs -dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a) -dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs -dyndep none : interesting for coqtop with statically linked plugins -dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d instead of extensions .cm*, so that the choice is made in the rest of the makefile (see next commit about coq_makedile) NB: two extra mli added to avoid building unecessary .cmo during 'make world', without having to use the ocamldep -native option. NB: we should state somewhere that coqmktop -top won't work unless 'make byte' was done first
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Fixed #4407.Gravatar Pierre Courtieu2015-11-06
| | | | | | | Like coqc: detect if the current directory was set by options, if not: add it with empty logical path. TODO: check if coq_makefile is still correct wrt to this modification, I think yes, actually it should end being more correct.
* Remove usage of Printexc.catch in the tools, as it is deprecated since 2001.Gravatar Guillaume Melquiond2015-07-30
| | | | | | | | "This function is deprecated: the runtime system is now able to print uncaught exceptions as precisely as Printexc.catch does. Moreover, calling Printexc.catch makes it harder to track the location of the exception using the debugger or the stack backtrace facility. So, do not use Printexc.catch in new code."
* Using maps and sets instead of lists in coqdep.Gravatar Pierre-Marie Pédrot2015-07-24
| | | | | | The quadratic behaviour of list searching probably appears with small enough samples. With the advent of usable libraries in Coq, and thus many possible dependencies, better be safe than sorry.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Coqdep: update include strategiesGravatar Pierre Boutillier2014-06-30
| | | | | | | | | | | | | | | -I is (only) the ml one -I -as is fixed -Q is understood -R is not a recursive ml include anymore $COQENV, user_contrib, ... are not recursively included coqlib/theories and coqlib/plugins are still recursively included (for now). (This may deserves an option) Closes Bug 2910: If there is a "Require a." in a b.v and a a.vo in path but no a.v, coqdep does not complains about a missing a.v.
* Fixing coqdep_boot warning relative to unknown ML files that were in tactics.Gravatar Pierre-Marie Pédrot2014-05-17
|
* Coqdep always uses / as dir_sepGravatar Pierre Boutillier2013-12-20
|
* Coqdep: add an -exclude-dir option (wish mentionned in #3025)Gravatar letouzey2013-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16431 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - 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
* Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)Gravatar letouzey2010-03-04
| | | | | | | | | | | | | | | | - This way, the Makefile.build gets shorter and simplier, with a few nasty hacks removed. - In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep". Instead, we now use ocamldep -modules, and process its output via coqdep_boot. This ways, *.cm* of .ml4 are correctly located, even when some .ml files aren't generated yet. - There is no risk of editing the .ml of a .ml4 by mistake, since it is by default in a binary format (cf pr_o.cmo and variable READABLE_ML4). M-x next-error still open the right .ml4 at the right location. - mltop.byteml is now mltop.ml, while mltop.optml keeps its name - .ml of .ml4 are added to .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12833 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdep_boot: one line with bad indentationGravatar letouzey2009-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12018 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
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵Gravatar letouzey2009-03-20
| | | | | | user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
* missing -c option of ocamlc in coq_makefile; coqdep_boot main loop was ↵Gravatar barras2009-03-16
| | | | | | included in coqdep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11985 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqdep_boot: a specialized and dependency-free coqdep for killing one of the ↵Gravatar letouzey2009-03-16
build stages git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11984 85f007b7-540e-0410-9357-904b9bb8a0f7