| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
proof for coqwc
|
| |\ \ |
|
| | |/
|/| |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | | |/
| |/| |
|
| |/ / |
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | |
| | | |
| | | |
| | | | |
Fixes BZ#5700
|
| | | |/ |
|
| | |/
|/|
| |
| | |
URLs on Windows are the same as on Unix, they use / not \.
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
wrongly tagged as keywords
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Make sure that when plugin writer does not use -bypass-API,
API is opened by default.
|
| | |/ /
|/| |
| | |
| | | |
On NixOS in particular, /usr/bin/time doesn't exist.
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
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.
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | | |
Minor clean up, no sense in having these as they do nothing.
|
| | |/ /
|/| |
| | |
| | | |
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)
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
Maxime Dénès
Paul Steckler
Guillaume Melquiond
Ralf Jung
Enrico Tassi
Tej Chajed
Théo Zimmermann
Matej Košík
Emilio Jesus Gallego Arias
Hugo Herbelin
Jason Gross
Pierre-Marie Pédrot
Jason Gross