aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
Commit message (Collapse)AuthorAge
* Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for ↵Gravatar Maxime Dénès2018-03-09
|\ | | | | | | fiat-crypto/OSX
| * Closes #6830: coqdep reads options and files from _CoqProject.Gravatar Gaëtan Gilbert2018-03-06
| | | | | | | | Note that we don't look inside -arg for eg -coqlib.
| * Add source (project file / command line) to project fields.Gravatar Gaëtan Gilbert2018-03-01
| |
| * Fix #6830: coqdep VDFILE uses too many arguments for fiat-crypto/OSXGravatar Gaëtan Gilbert2018-02-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We fix as suggested by @JasonGross by reading file names from the _CoqProject when coq_makefile was invoked with one. I made coqdep only look at the .v files from _CoqProject because it's easier this way. Since we're going through the _CoqProject parser we could have coqdep understand more of it but let's leave that to another PR (and maybe someone else). Some projects pass vfiles on the command line, we keep the list of these files to pass them to coqdep via command line even when there is a _CoqProject. Multiple project files is probably broken.
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [error] Replace msg_error by a proper exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | The current error mechanism in the core part of Coq is 100% exception based; there was some confusion in the past as to whether raising and exception could be replace with `Feedback.msg_error`. As of today, this is not the case [due to some issues in the layer that generates error feedbacks in the STM] so all cases of `msg_error` must raise an exception of print at a different level [for now].
* Added newline at the end of usage of coqdep.Gravatar Bernhard Schommer2018-01-11
|
* 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
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
* coqdep: remove optimization making makefiles harder to writeGravatar Enrico Tassi2017-05-23
|
* Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
|
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | Suggested by @ppedrot
* 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.
* Merge remote-tracking branch 'github/pr/229' into trunkGravatar Maxime Dénès2016-07-04
|\ | | | | | | Was PR#229: Bytecode compilation in a new 'make byte' rule apart from 'make world'
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | | | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
| * 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
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
| * Minor edits in output of coqdep --help.Gravatar Maxime Dénès2016-01-15
| |
| * Fix #4408.Gravatar Pierre Courtieu2016-01-15
| | | | | | | | | | Removed documentation for broken -D -w (but the option are still there). Fixed documentation of others.
| * Partially fixing #4408: coqdep --help is up to date.Gravatar Pierre Courtieu2016-01-15
| |
* | Remove deprecated command-line options such as "-as".Gravatar Guillaume Melquiond2016-01-06
| |
* | 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.
* | 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.
* | 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.
* | Restricting the need for coqdep_boot to mllib.d files (since ocamlGravatar Hugo Herbelin2015-02-16
| | | | | | | | | | 3.12.1, ocamldep was able to deal with .ml4, so that building .mllib.d is the only feature that coqdep_boot was still required for).
| * 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.
| * Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
| | | | | | | | This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
| * Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
| |
| * 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.
* Applying Virgile Prevosto's patch for better error report in coqdep (#3029).Gravatar Hugo Herbelin2014-10-08
|
* 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.
* make coqdep canonicalize paths from the command lineGravatar Gregory Malecha2014-05-26
| | | | | | | | - logical paths given to -R and -I should be split on periods. - it also seems like giving an empty string should result in the empty path rather than the singleton path with an empty string as an identifier.
* Fixing the undocumented -dumpgraphbox option of coqdep.Gravatar Pierre-Marie Pédrot2014-05-12
|
* Newline on -slash warning in coqdep.Gravatar Pierre-Marie Pédrot2014-03-28
|
* Using full paths in coqdep -dumpgraph.Gravatar Pierre-Marie Pédrot2014-01-19
|
* Fixing coqdep graph printing. The transitive reduction algorithm was bugged.Gravatar Pierre-Marie Pédrot2014-01-19
|
* Implementing transitive reduction in the dependency graph printingGravatar Pierre-Marie Pédrot2014-01-16
| | | | mechanism of coqdep.
* 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.