aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
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
* \ Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \
| | * 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
| |/ |/|
* | Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵Gravatar Maxime Dénès2018-02-19
|\ \ | | | | | | | | | camlp4
| * | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | | | | | | | | longer use camlp4.
| | * Implement name mangling optionGravatar Jasper Hugunin2018-02-17
| |/ |/|
* | Merge PR #1073: new quick2vo target: like vio2vo, but smarterGravatar Maxime Dénès2018-02-15
|\ \
| * | new quick2vo target: like vio2vo, but smarterGravatar Ralf Jung2018-02-15
| |/
* | Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProjectGravatar Maxime Dénès2018-02-15
|\ \
| * | coq_makefile: Support "" as the prefix in _CoqProjectGravatar Joachim Breitner2018-02-15
| | | | | | | | | | | | | | | | | | | | | | | | This fixes #6350 (and even comes with a test case). Refering to other directories as `-R … ""` is maybe not best practice, but some people out there do it, so as long as it does not cause too much trouble, we can continue to support it.
* | | Merge PR #6704: Fix coq_makefile not passing -R options to coqdoc, breaking ↵Gravatar Maxime Dénès2018-02-13
|\ \ \ | |/ / |/| | | | | links (#6697)
* | | [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].
| * Possible fix for issue #6697Gravatar Yannick Forster2018-02-07
|/
* Merge PR #6466: Replace md5sum/md5 calls by an OCaml programGravatar Maxime Dénès2018-01-16
|\
| * Avoid shell backticks and improve md5sum.ml error messagesGravatar Jacques-Pascal Deplaix2018-01-15
| |
* | Added newline at the end of usage of coqdep.Gravatar Bernhard Schommer2018-01-11
| |
* | Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scriptsGravatar Maxime Dénès2018-01-08
|\ \
| * | Add TIMING_SORT_BY and --sort-by to timing scriptsGravatar Jason Gross2017-12-27
| | | | | | | | | | | | | | | This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292
* | | [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
|/ / | | | | | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
* | Merge PR #6040: Making coq_makefile usage consistent with what it claims + ↵Gravatar Maxime Dénès2017-12-27
|\ \ | | | | | | | | | possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments)
| | * Check the whole string given by md5sum.mlGravatar Jacques-Pascal Deplaix2017-12-24
| | |
| | * Replace md5sum/md5 calls by an OCaml programGravatar Jacques-Pascal Deplaix2017-12-23
| |/ |/|
| * Registering a printing handler in coq_makefile.Gravatar Hugo Herbelin2017-12-23
| | | | | | | | | | This allows to fix the non-printing of error messages produced when parsing arguments.
| * Forbidding -o and -f in input file of coq_makefile.Gravatar Hugo Herbelin2017-12-23
| | | | | | | | This was apparently either silently doing nothing or failing.
| * Removing failure of coq_makefile on no arguments.Gravatar Hugo Herbelin2017-12-23
| | | | | | | | | | | | | | | | Nevertheless making option -o of coq_makefile recommended as discussed in PR#6040. This is one way to resolve the inconsistency with the usage which says that all arguments are optional.
* | Merge PR #6217: Do dependencies in 1 command per file class.Gravatar Maxime Dénès2017-12-18
|\ \
| * | Do dependencies in 1 command per file class.Gravatar Gaëtan Gilbert2017-12-15
| | |
* | | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ \
* \ \ \ Merge PR #6388: Fix issue #6387Gravatar Maxime Dénès2017-12-14
|\ \ \ \
* \ \ \ \ Merge PR #1108: [stm] Reorganize flagsGravatar Maxime Dénès2017-12-13
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6175: Restoring filtering of native files passed to `rm` during ↵Gravatar Maxime Dénès2017-12-13
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | `make clean`.
| | | * | | | Fix issue #6387Gravatar Martin Vassor2017-12-11
| |_|/ / / / |/| | | | |
| * | | | | Restoring filtering of native files passed to `rm` during `make clean`.Gravatar Maxime Dénès2017-12-11
| | |_|_|/ | |/| | | | | | | | | | | | | Was lost during the coq_makefile 1 -> 2 translation.
| | * | | [flags] [stm] Reorganize flags.Gravatar Emilio Jesus Gallego Arias2017-12-11
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | We move the main async flags to the STM in preparation for more state encapsulation. There is still more work to do, in particular we should make some of the defaults a parameter instead of a flag.
| | * | [build] Remove coqmktop in favor of ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-12-10
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
* | | Merge PR #6142: Single quotes break on WindowsGravatar Maxime Dénès2017-12-07
|\ \ \
* | | | coq_makefile: pass filenames to coqchkGravatar Ralf Jung2017-11-29
| |_|/ |/| |
* | | Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate.Gravatar Maxime Dénès2017-11-27
|\ \ \
| * | | Fix coq-makefile ocamldoc call when configured with -annotate.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | Fixes #6120.
* | | | Update TimeFileMaker.py to correctly sort timing diffsGravatar Jason Gross2017-11-22
|/ / / | | | | | | | | | Previously, it was reverse-ordering timing diffs.
* | / Rename coq-inferior.el -> inferior-coq.el to match provided feature.Gravatar Gaëtan Gilbert2017-11-19
| |/ |/| | | | | Fixes #4988.
| * Single quotes break on WindowsGravatar Carl Patenaude Poulin2017-11-11
|/ | | | | | | As it is, running a `Makefile.coq` on Windows produces the following error: `cut: ': No such file or directory` Changing to double quotes fixes this.
* Fix FIXME: use OCaml 4.02 generative functors when available.Gravatar Gaëtan Gilbert2017-11-01
| | | | 4.02.3 has been the minimal OCaml version for a while now.
* Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or ↵Gravatar Maxime Dénès2017-10-12
|\ | | | | | | directory` on every execution
| * Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every ↵Gravatar Maxime Dénès2017-10-11
| | | | | | | | execution
* | Merge PR #1143: fix coq_makefile on cygwinGravatar Maxime Dénès2017-10-11
|\ \
| * | Fix BZ#5780: coq_makefile broken under CygwinGravatar Ralf Jung2017-10-10
| |/
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 06:48:44 +0000