aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_common.ml
Commit message (Collapse)AuthorAge
* [coqdep] Minor cleanups.Gravatar Emilio Jesus Gallego Arias2018-05-08
| | | | | | | - Remove inclusion of the `tactics` directory, this is coming from a time loadable modules were found there, now all are under `plugins`. - Remove 2 dependencies so we can bootstrap coqdep earlier. - Use `Format` instead of `Printf` for printing.
* Fix #7413: coqdep warning on repeated filesGravatar Gaëtan Gilbert2018-05-04
| | | | | | | | The same warning exists in ocamllibdep so I copied the change there. Detecting when 2 paths are the same is approximate, eg ././a.ml and a.ml are considered different. Implementing realpath probably isn't worth doing for this warning.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* 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
* Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Gaëtan Gilbert2017-05-28
| | | | | | | | Deprecations which can't be fixed in 4.02.3 are locally wrapped with [@@@ocaml.warning "-3"]. The only ones encountered are - capitalize to capitalize_ascii and variants. Changing to ascii would break coqdoc -latin1 and maybe other things though. - external "noalloc" to external [@@noalloc]
* coqdep: remove optimization making makefiles harder to writeGravatar Enrico Tassi2017-05-23
|
* coqdep: set FOR_PACK variable for files that need to be packedGravatar Enrico Tassi2017-05-23
| | | | | | | | | This enables one to have just one rule to compile .ml -> .cmx. By using $(FOR_PACK) in such rule one passes to ocamlopt -for-pack ModName only when necessary. Before this coq_makefile had to generate 2 different rules, depending if the module was mentioned in an .mlpack.
* Dead code in coqdep.Gravatar Hugo Herbelin2017-05-15
| | | | Was introduced in 5268efdef, reverted then readded in 1be9c4d.
* Fix #4837: ./configure -local makes coqdep issue many warningsGravatar Maxime Dénès2016-11-04
| | | | | | We simply remove the warnings about paths mixing Win32 and Unix separators, since that situation does not seem problematic (c.f. discussion on the bug tracker).
* 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
* ocamllibdep + coqdep : simpler deps concerning .mllib and .mlpackGravatar Pierre Letouzey2016-06-15
| | | | | | | Since we already have a rule %.cmxs:%.cmxa and the .cmxa depends already on all the .cmx inside it, no need to state explicitely that the .cmxs depends on these inner .cmx. Same thing concerning .cmxs built out of a single .cmx.
* Makefile: restore the use of coqdep_boot for creating .v.d filesGravatar Pierre Letouzey2016-06-01
| | | | | | | Coqdep_boot has almost no dependencies, and hence can be compiled very early during the build, without relying on .ml.d files. Some code of system.ml is now in a separate file minisys.ml, which is also included in system.ml for compatibility.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Fixing bug #4373: coqdep does not know about .vio files.Gravatar Pierre-Marie Pédrot2016-01-24
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Remove unused functions.Gravatar Guillaume Melquiond2016-01-01
| |
* | Remove some occurrences of Unix.opendir.Gravatar Guillaume Melquiond2015-12-14
| |
* | 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.
| * Fixing #4406 coqdep: No recursive search of ml (-I).Gravatar Pierre Courtieu2015-11-06
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-22
|\|
| * report the full module path when reporting errors in coqdepGravatar Gregory Malecha2015-08-13
| |
* | 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.
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-02
|\|
| * Removing dead code in coqdep.Gravatar Pierre-Marie Pédrot2015-06-30
| | | | | | | | | | | | Since commit 2f521670fbd, the Require "file" syntax was not used anymore by coqtop but the code handling it was still there in coqdep. We finish the work by erasing the remnant code.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Remove spurious ".v" from warning message.Gravatar Guillaume Melquiond2015-04-20
| |
* | 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
|
* Fixing typo in previous commit.Gravatar Hugo Herbelin2015-01-12
|
* Fixing wrong duplication message when finding both a .ml and a .ml4 in coqdep.Gravatar Hugo Herbelin2015-01-11
|
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
|
* coqdep: granting #2506 (./dir is the same as dir)Gravatar Hugo Herbelin2014-12-04
|
* 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.
* Support for Timeout n and From ..Gravatar Gregory Malecha2014-08-25
| | | | | - The state machine gets kind of complex maybe it should become a parser at some point?
* 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.
* Declared ML Module are not uncapitalized/capitalized/uncapitalized/...Gravatar Pierre Boutillier2014-01-13
| | | | The exact filename has to be written. This is coherent with the RefMan.
* .vi files: .vo files without proofsGravatar Enrico Tassi2014-01-04
| | | | | | | | | | | | | | | | | | | | | | | File format: The .vo file format changed: - after the magic number there are 3 segments. A segment is made of 3 components: bynary int, an ocaml value, a digest. The binary int is the position of the digest, so that one can skip the value without unmarshalling it - the first segment is the library, as before - the second segment is the STM task list - the third segment is the opaque table, as before A .vo file has a complete opaque table (all proof terms are there). A .vi file follows the same format of a .vo file, but some entries in the opaque table are missing. A proof task is stocked instead. Utilities: coqc: option -quick generates a .vi insted of a .vo coq_makefile: target quick to generate all .vi coqdep: generate deps for .vi files too votour: can browse .vi files too, the first question is which segment should be read coqchk: rejects .vi files
* Warning removalGravatar Pierre Boutillier2013-12-20
|
* Coqdep always uses / as dir_sepGravatar Pierre Boutillier2013-12-20
|
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵Gravatar xclerc2013-09-19
| | | | | | with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7