aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_common.mli
Commit message (Collapse)AuthorAge
* 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
* Dead code in coqdep.Gravatar Hugo Herbelin2017-05-15
| | | | Was introduced in 5268efdef, reverted then readded in 1be9c4d.
* 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
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Merge remote-tracking branch 'origin/v8.5' into upstream-trunkGravatar Hugo Herbelin2015-11-07
|\| | | | | | | | | - Had to add a Sigma.to_evar_map - Had to rework coqdep_common.ml{,i} and coqdep.ml
| * 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.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-27
|\|
| * 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.
| * Fixing bug #4265: "coqdep does not handle From ... Require" for good.Gravatar Pierre-Marie Pédrot2015-07-24
| |
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-06
|\|
| * Fixing bug #4265: coqdep does not handle From ... Require.Gravatar Pierre-Marie Pédrot2015-07-03
| | | | | | | | | | | | The search algorithm is not satisfactory though, as it crawls through all known files to find the proper one. We should rather use some trie-based data structure, but I'll leave this for a future commit.
* | Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-16
| | | | | | | | | | | | | | | | In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error), - uniformly expecting paths in Unix format and warning otherwise.
| * Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
| | | | | | | | | | | | (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
| * Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
|/ | | | | | | In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error).
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* coqdep: Warning about ml file clashes, keeping the file correspondingGravatar Hugo Herbelin2014-12-04
| | | | | | | | to the first -I option. Fortunately, with -I option, only one file can be found by occurrence of the option, so on the contrary of -Q/-R options for v files, the order is not file-system dependent.
* 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.
* Adding a -dumpgraph option to Coqdep that output the graph dependency of theGravatar Pierre-Marie Pédrot2014-01-06
| | | | | | considered files. Original patch by Guillaume Allais.
* 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
* avoid dependency nightmare by creating coqdep_{lexer,common}.mliGravatar letouzey2011-09-18
Sequel to commit 14476 : in fact, even with "tools" in .PHONY, we still may have coqdep stuff being recompiled in a "make" that follows a successful "make". This seems to related to the hacks I've introduced to prevent ocamlopt from erasing and recreating .cmi when there's no .mli around (cf. comment around line 823 in Makefile.build). Scenario: - First we build coqdep_boot directly out of coqdep_lexer.ml and co. When ocamlopt is around, this creates some .cmx and .cmi, but no .cmo. - Later we build coqdep, which need coqdep_lexer.cmx and co. Now "make" checks whether these .cmx are up-to-date. But our hacks made these .cmx depend on the corresponding .cmi. Then "make" checks whether these .cmi are up-to-date. But our hacks made these .cmi depend on the corresponding .cmo. These .cmo doesn't exist yet, we run ocamlc, which recreates the .cmi with same content but a different timestamp. For some strange reason, even with refreshed .cmi, the .cmx are not remade by this run, but will be on the next run. Conclusion: what a mess. Implicit rules about .cmx / .cmo / .cmi should be improved, but I see currently no simple solution. In the meantime, an simple ad-hoc fix is to create these two .mli ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14479 85f007b7-540e-0410-9357-904b9bb8a0f7