| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
| |
It is empty and not used anymore.
|
| |
|
|
|
| |
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.
|
| |
|
|
| |
In particular, find it under $(COQBIN)
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
This closes [bug #5596](https://coq.inria.fr/bugs/show_bug.cgi?id=5596).
|
| |\ |
|
| | | |
|
| | |
| |
| | |
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)
|
| |/
|
|
| |
This fixes [bug #5619](https://coq.inria.fr/bugs/show_bug.cgi?id=5619)
|
| |
|
|
|
| |
Save the COQC variable for the actual path to coqc, as per
https://github.com/coq/coq/pull/742#pullrequestreview-44072778
|
| |
|
| |
It should not emit ` (user: 0.00 mem: 2852 ko)` multiple times
|
| | |
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| |/ / |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
make install does not install these *.cm(o|a) files either.
You could always do manually :
- make bytefiles : to build the bytecode *.cm(o|a) files
- make install-byte : to install these files
- make byte : to compile the whole development with the bytecode version
of Coq (this builds the *.cm(o|a) files, but also the .vo via coqc -byte).
Technically, the behavior of make is controlled by the OPT variable,
which could be -byte or -opt. For instance, 'make byte' corresponds to a
'make OPT:=-byte'
Note that coqdep is used with the new option "-dyndep var" : when seeing
a Declare ML Module "foo", "coqdep -dyndep var" does not decide whether to
depend on foo.cma or foo.cmxs, but rather use some Makefile variables such
as foo$(DYNLIB), whose content is later set according to $(OPT)
|
| |
|
|
|
|
|
|
| |
It used to generate only .cmo (the packed one).
While this works if the plugin has no external dependencies,
it does not if it does.
The bug affected only bytecode builds
|
| |
|
|
|
| |
This fixes bedrock and eliminates warnings.
Thanks Jason Gross for debugging this!
|
| |
|
|
|
|
|
|
| |
This makes the following work correctly:
make only TGTS="foo bar" -j2
note that
make foo bar -j2
is not doing what you think
|
| | |
|
| | |
|
| | |
|
| |
|
Emilio Jesus Gallego Arias
Enrico Tassi
Jason Gross
Maxime Dénès
Jason Gross
Matej Košík
Pierre Letouzey