aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
Commit message (Collapse)AuthorAge
* [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)
| * 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
| |/
* / [configure] Support for flambda flags.Gravatar Emilio Jesus Gallego Arias2017-10-10
|/ | | | | | | | | We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
* TimeFileMaker.py: Allow trailing spacesGravatar Jason Gross2017-10-06
| | | | | This allows the timing aggregation scripts to handle logs from Travis, which, for some reason, seems to insert trailing spaces.
* Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵Gravatar Maxime Dénès2017-10-05
|\ | | | | | | to escape non-UTF-8 file names)
* \ Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵Gravatar Maxime Dénès2017-10-05
|\ \ | | | | | | | | | coq_makefile are in sync (supersed #1039)…
| * | fix compilation on OCaml < 4.04Gravatar Enrico Tassi2017-10-03
| | |
* | | Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵Gravatar Maxime Dénès2017-10-03
|\ \ \ | | | | | | | | | | | | proof for coqwc
* \ \ \ Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580).Gravatar Maxime Dénès2017-10-03
|\ \ \ \
| | * | | look for Obligation num or Next Obligation to start proofGravatar Paul Steckler2017-09-26
| |/ / / |/| | |
* | | | Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\ \ \ \
* \ \ \ \ Merge PR #1070: Remove remaining occurrences of -just-parsing.Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \
| | | * | | Properly handle "coq_makefile -Q . Foo" (bug #5580).Gravatar Guillaume Melquiond2017-09-21
| | | | | |
| * | | | | Remove remaining occurrences of -just-parsing.Gravatar Guillaume Melquiond2017-09-21
| | |/ / / | |/| | |
* / | | | coq_makefile: dont show errors from failed (ignored) rmdirGravatar Ralf Jung2017-09-20
|/ / / /
| | * | coq_makefile: make sure compile flags for Coq and coq_makefile are in syncGravatar Emilio Jesus Gallego Arias2017-09-19
| | | | | | | | | | | | | | | | | | | | | | | | E.g. -safe-string is set by configure.ml and made available to both make (via config/Makefile) and coq_makefile (via config/coq_config.ml -> lib/envars.ml -> CoqMakefile.in).
| * | | Add XML protocol support for Wait.Gravatar Maxime Dénès2017-09-19
|/ / /
* | | Merge PR #990: Prevent warning about DSTROOT being undefined.Gravatar Maxime Dénès2017-09-15
|\ \ \ | |/ / |/| |
| | * Supporting library names in utf8 in coqdep.Gravatar Hugo Herbelin2017-09-13
| |/ |/|
* | Merge PR #997: coqdoc: Support comments in verbatim outputGravatar Maxime Dénès2017-09-07
|\ \
* \ \ Merge PR #958: coq_makefile: build/use .cma for packed plugins tooGravatar Maxime Dénès2017-08-31
|\ \ \
| * | | coq_makefile: fix .merlin generation (FLG -thread)Gravatar Enrico Tassi2017-08-29
| | | |
| * | | coq_makefile: improve documentationGravatar Enrico Tassi2017-08-29
| | | |
| * | | coq_makefile: print error message when coqlib is not set properlyGravatar Enrico Tassi2017-08-29
| | | |
| * | | coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxsGravatar Enrico Tassi2017-08-29
| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 23:08:35 +0000