aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-07-11Add an entry to CHANGES about timing in coq_makefileJason Gross
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-08Also install gnu-time on travis on Mac OSXJason Gross
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 #863: Fixing environment in warning "Projection value has no head ↵Maxime Dénès
constant".
2017-07-07Merge PR #842: Update the Tutorial.Maxime Dénès
2017-07-07Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ↵Maxime Dénès
the monad.
2017-07-07Merge PR #835: Remove doc/refman/RefMan-ind.texMaxime Dénès
2017-07-07Set version to 8.7.0~alpha.Maxime Dénès
2017-07-07Merge PR #844: Better support for make TIMED=1 on WindowsMaxime Dénès
2017-07-07Merge PR #800: Enable fiat-cryptoMaxime Dénès
2017-07-07Fixing environment in warning "Projection value has no head constant".Hugo Herbelin
Delaying also some computation needed for printing to the time of really printing it.
2017-07-05Merge PR #837: Add inversion_sigma to CHANGES and to docMaxime Dénès
2017-07-05Merge PR #850: Improve grammar in RefMan-Gal and RefMan-synMaxime Dénès
2017-07-05Merge PR #840: Quote $(OCAMLFIND) in CoqMakefile.in for WindowsMaxime Dénès
2017-07-05Merge PR #839: Update .gitignore with doc/tutorial/Tutorial.v.outMaxime Dénès
2017-07-05Merge PR #832: Document an example `Makefile` for `coq_makefile`Maxime Dénès
2017-07-04Revert fiat-crypto overlayJason Gross
Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6.
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-07-01Update RefMan-syn.texwilliam-lawvere
2017-07-01Merge remote-tracking branch 'upstream/trunk' into trunkWilliam Lawvere
2017-07-01RefMan-gal: improve grammarWilliam Lawvere
2017-07-01RefMan-syn: grammar editWilliam Lawvere
2017-06-30Document an example `Makefile` for `coq_makefile`Jason Gross
We document an example `Makefile` which does not include the generated `CoqMakefile`, but instead invokes arbitrary targets in it.
2017-06-30Remove doc/refman/RefMan-ind.texJason Gross
It does not seem to be referred to by any file, and does not seem to be built by any implicit rules.
2017-06-30Add doc for inversion_sigma to RefMan-tacJason Gross
2017-06-30Update CHANGES with inversion_sigma entryJason Gross
2017-06-30Update .gitignore with doc/tutorial/Tutorial.v.outJason Gross
2017-06-30Fix more potential quoting issues: COQBIN , COQLIBJason Gross
2017-06-30Also quote $(COQLIB)/grammarJason Gross
In case COQLIB has backslashes, as it does on Windows, or spaces
2017-06-30Create a variable for CAMLDOC in CoqMakefile.inJason Gross
2017-06-30Quote $(OCAMLFIND) in CoqMakefile.in for WindowsJason Gross
This, I hope, will fix [bug #5620](https://coq.inria.fr/bugs/show_bug.cgi?id=5620)
2017-06-30Better support for make TIMED=1 on WindowsJason Gross
This fixes [bug #5619](https://coq.inria.fr/bugs/show_bug.cgi?id=5619)
2017-06-30Merge PR#846: Fix OS X Travis by pinning OCaml version.Maxime Dénès
2017-06-30Merge PR#843: closing bug #5618 introduce by PR 828Maxime Dénès
2017-06-30Mention again how to report bug and get version number.Théo Zimmermann
As suggested by @psteckler.
2017-06-30Fix OS X Travis by pinning OCaml version.Théo Zimmermann
2017-06-29Better phrasing.Théo Zimmermann
2017-06-29More substance on discouraged practices.Théo Zimmermann
2017-06-29closing bug #5618 introduce by PR 828Julien Forest
2017-06-29Some more corrections to the tutorial.Théo Zimmermann
2017-06-29Mask the reliance on coqtop.Théo Zimmermann
2017-06-28Update the Tutorial.Théo Zimmermann
2017-06-27Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails ↵Maxime Dénès
with make -j4
2017-06-27Merge PR#731: Mini-cleaning around OCaml file namesMaxime Dénès
This is only a partial merge, we stick with using the standard OCaml (un)capitalize functions.
2017-06-27A cleaning phase about ocaml file names.Hugo Herbelin
Ocaml file names are restricted since 2008 to A..Z followed by a..z0..9'_. We take this constraint into account in tools manipulating Ocaml file names.
2017-06-27Merge PR#814: Fix #5380: Default colors for CoqIDE are actually applied.Maxime Dénès
2017-06-26Merge PR#826: Put plugin exports in the right compatibility fileMaxime Dénès
2017-06-26Merge PR#825: Ignore all PDF files.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 10:29:52 +0000