| Age | Commit message (Collapse) | Author |
|---|
|
|
|
compute.
|
|
|
|
We document the most useful timing targets and variables, how to invoke
them, and what the output looks like.
|
|
|
|
|
|
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.
|
|
Global declarations used to carry universe instances with them, but it
turns out this information is not used anywhere. Instead, instances were
already properly encoded as the first argument of polymorphic definitions.
|
|
|
|
This closes [bug #5596](https://coq.inria.fr/bugs/show_bug.cgi?id=5596).
|
|
This is usable for no-color terminal.
For instance, a typical application in mind is the Coq-generate names
marker which can be rendered with a color if the interface supports it
and a prefix "~" if the interface does not support colors.
|
|
|
|
constant".
|
|
|
|
the monad.
|
|
|
|
|
|
|
|
|
|
Delaying also some computation needed for printing to the time of
really printing it.
|
|
|
|
Fixes Coq bug 5635 (https://coq.inria.fr/bugs/show_bug.cgi?id=5635).
|
|
|
|
We now pass `-ignore-coq-version` to CompCert's configure (cf
AbsInt/CompCert#188) , thanks to @xavierleroy .
|
|
Extraction TestCompile foo
is equivalent to:
Extraction "/tmp/testextraction1234.ml" foo
ocamlfind ocamlc -I /tmp -c /tmp/testextraction1234.mli /tmp/testextraction1234.ml
This command isn't meant for the end user, but rather as an helper
for test-suite scripts. It only works with extraction to OCaml,
and the generated code should be standalone.
|
|
|
|
|
|
|
|
|
|
|
|
This should help preventing weird compilation failures due to leftover
object files after deleting or moving some source files
By the way:
- use plain $(filter-out ...) instead of a 'diff' macro (thanks Jason
for the suggestion)
- rename FIND_VCS_CLAUSE into FIND_SKIP_DIRS since it contains more
than version control stuff nowadays
|
|
Not a useful overlay. Fiat-crypto has since been updated to pass
-compat 8.6.
|
|
|
|
|
|
This code was a sketch of what to do when we properly implement module-level
handling of instanciation of definitions by inductive types. It was completely
dead code, called after an error, and somewhat incorrect. Instead of letting
it bitrot, we remove it.
|
|
These functions were messing with the deferred universe constraints in an
error-prone way, and were only used for printing as of today. We inline
the one used by the printer instead.
|
|
This was useless, because immediate constraints are assumed to already be in
the current environment, while deferred constraints are useless for the
conversion check of the definition types, as they only appear in the opaque
body.
This also clarifies a bit what is going on in the typing of module constraints
w.r.t. global universes.
|
|
|
|
|
|
|
|
|
|
We document an example `Makefile` which does not include the generated
`CoqMakefile`, but instead invokes arbitrary targets in it.
|
|
It does not seem to be referred to by any file, and does not seem to be
built by any implicit rules.
|
|
|
|
|
|
|
|
|
|
In case COQLIB has backslashes, as it does on Windows, or spaces
|
|
|
|
This, I hope, will fix [bug #5620](https://coq.inria.fr/bugs/show_bug.cgi?id=5620)
|
