aboutsummaryrefslogtreecommitdiff
path: root/tools
AgeCommit message (Collapse)Author
2017-10-03fix compilation on OCaml < 4.04Enrico Tassi
2017-10-03Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵Maxime Dénès
proof for coqwc
2017-10-03Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580).Maxime Dénès
2017-09-26look for Obligation num or Next Obligation to start proofPaul Steckler
2017-09-22Merge PR #1055: Remove STM vernacularsMaxime Dénès
2017-09-22Merge PR #1070: Remove remaining occurrences of -just-parsing.Maxime Dénès
2017-09-21Properly handle "coq_makefile -Q . Foo" (bug #5580).Guillaume Melquiond
2017-09-21Remove remaining occurrences of -just-parsing.Guillaume Melquiond
2017-09-20coq_makefile: dont show errors from failed (ignored) rmdirRalf Jung
2017-09-19coq_makefile: make sure compile flags for Coq and coq_makefile are in syncEmilio Jesus Gallego Arias
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).
2017-09-19Add XML protocol support for Wait.Maxime Dénès
2017-09-15Merge PR #990: Prevent warning about DSTROOT being undefined.Maxime Dénès
2017-09-13Supporting library names in utf8 in coqdep.Hugo Herbelin
2017-09-07Merge PR #997: coqdoc: Support comments in verbatim outputMaxime Dénès
2017-08-31Merge PR #958: coq_makefile: build/use .cma for packed plugins tooMaxime Dénès
2017-08-29coq_makefile: fix .merlin generation (FLG -thread)Enrico Tassi
2017-08-29coq_makefile: improve documentationEnrico Tassi
2017-08-29coq_makefile: print error message when coqlib is not set properlyEnrico Tassi
2017-08-29coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxsEnrico Tassi
2017-08-29Merge PR #773: [flags] Remove XML output flag.Maxime Dénès
2017-08-29coq_makefile: do not overwrite CAMLFLAGSEnrico Tassi
2017-08-29coq_makefile: use dedicated variable for extra packagesEnrico Tassi
CAMLPKGS is now used to hold extra findlib -packages The previous solution was to use CAMLFLAGS but since 4.05 an invocation of `ocamlopt -pack useless.cmxa foo.cmx -o packedfoo.cmx` fails saying that `useless.cmxa` is not a compilation unit description. CAMLPKGS is used in all `ocamlopt` invocations but for the one performing the packing.
2017-08-29coq_makefile: build/use .cma for packed pluginsEnrico Tassi
The build chain is always ml -> cmo -> cma ml -> cmx -> cmxa -> cmxs If we are packing, then it becomes ml -> cmo \ ml -> cmo --> cmo -> cma ml -> cmo / ml -> cmxo \ ml -> cmxo --> cmxo -> cmxa -> cmxs ml -> cmxo / The interest of always having a .cma or .cmxa is that such file can carry linking flags, that in findlib terms means which -package was use to build the plugin.
2017-08-29coqdoc: Support comments in verbatim outputTej Chajed
Fixes BZ#5700
2017-08-22Prevent warning about DSTROOT being undefined.Guillaume Melquiond
2017-08-21Fix coqdoc URLs under Windows.Théo Zimmermann
URLs on Windows are the same as on Unix, they use / not \.
2017-08-16Merge PR #964: More portable location for the time command.Maxime Dénès
2017-08-16Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵Maxime Dénès
wrongly tagged as keywords
2017-08-12fix coq_makefileMatej Košík
Make sure that when plugin writer does not use -bypass-API, API is opened by default.
2017-08-12More portable location for the time command.Théo Zimmermann
On NixOS in particular, /usr/bin/time doesn't exist.
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
2017-08-01Merge PR #921: [make] remove compat5 file.Maxime Dénès
2017-08-01Merge PR #917: Moving --print-version to -print-version for consistency.Maxime Dénès
2017-07-27[toplevel] Remove long ago deprecated and NOOP options.Emilio Jesus Gallego Arias
Minor clean up, no sense in having these as they do nothing.
2017-07-27[make] remove compat5 file.Emilio Jesus Gallego Arias
It is empty and not used anymore.
2017-07-25Adding -print-version in addition to -print-version for consistency.Hugo Herbelin
2017-07-20fake_ide: do as coqide to find out coqtop pathEnrico Tassi
2017-07-20coq-makefile: strip windows drive letter when DESTDIR is not emptyEnrico Tassi
In unix one can concatenate a prefix with an absolute path in order to obtain a valid path. This is not the case on Windows.
2017-07-20coq-makefile: treat coq_makefile as any other coq binaryEnrico Tassi
In particular, find it under $(COQBIN)
2017-07-20coq-makefile: quote using ' to preserve \ (windows paths)Enrico Tassi
2017-07-20In fake_ide, call coqtop.exe instead of coqtop on Win32.Maxime Dénès
2017-07-20Avoid using unsupported signals under Windows in fake_ide.Maxime Dénès
2017-07-20Merge branch 'v8.7'Maxime Dénès
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-15Fixing #5648 (too early decision of tagging ident as keyword in html coqdoc).Hugo Herbelin
Fix proposed by the reporter, Vincent Laporte. Note that for LaTeX output, the selection of a keyword was already done after checking if the ident is recognized as a Coq ident by coqtop. Incidentally, being now explicit on an wildcard-catching of exceptions.
2017-07-11Add timing scriptsJason Gross
This commit adds timing scripts from https://github.com/JasonGross/coq-scripts/tree/master/timing into the tools folder, and integrates them into coq_makefile and Coq's makefile. The main added makefile targets are: - the `TIMING` variable - when non-empty, this creates for each built `.v` file a `.v.timing` variable (or `.v.before-timing` or `.v.after-timing` for `TIMING=before` and `TIMING=after`, respectively) - `pretty-timed TGTS=...` - runs `make $(TGTS)` and prints a table of sorted timings at the end, saving it to `time-of-build-pretty.log` - `make-pretty-timed-before TGTS=...`, `make-pretty-timed-after TGTS=...` - runs `make $(TGTS)`, and saves the timing data to the file `time-of-build-before.log` or `time-of-build-after.log`, respectively - `print-pretty-timed-diff` - prints a table with the difference between the logs recorded by `make-pretty-timed-before` and `make-pretty-timed-after`, saving the table to `time-of-build-both.log` - `print-pretty-single-time-diff BEFORE=... AFTER=...` - this prints a table with the differences between two `.v.timing` files, and saves the output to `time-of-build-pretty.log` - `*.v.timing.diff` - this saves the result of `print-pretty-single-time-diff` for each target to the `.v.timing.diff` file - `all.timing.diff` (`world.timing.diff` and `coq.timing.diff` in Coq's own Makefile) - makes all `*.v.timing.diff` targets N.B. We need to make `make pretty-timed` fail if `make` fails. To do this, we need to get around the fact that pipes swallow exit codes. There are a few solutions in https://stackoverflow.com/questions/23079651/equivalent-of-pipefail-in-gnu-make; we choose the temporary file rather than requiring the shell of the makefile to be bash.
2017-07-08Fix TIMED=1 on Mac OSXJason Gross
This closes [bug #5596](https://coq.inria.fr/bugs/show_bug.cgi?id=5596).
2017-07-07Merge PR #844: Better support for make TIMED=1 on WindowsMaxime Dénès
2017-07-05Merge PR #840: Quote $(OCAMLFIND) in CoqMakefile.in for WindowsMaxime Dénès
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 16:53:52 +0000