| Commit message (Collapse) | Author | Age |
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Note that we don't look inside -arg for eg -coqlib.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We fix as suggested by @JasonGross by reading file names from the
_CoqProject when coq_makefile was invoked with one.
I made coqdep only look at the .v files from _CoqProject because it's
easier this way. Since we're going through the _CoqProject parser we
could have coqdep understand more of it but let's leave that to
another PR (and maybe someone else).
Some projects pass vfiles on the command line, we keep the list of
these files to pass them to coqdep via command line even when there is
a _CoqProject.
Multiple project files is probably broken.
|
|\
| |
| |
| | |
camlp4
|
| |
| |
| |
| | |
longer use camlp4.
|
|\ \ |
|
| |/ |
|
|/ |
|
|\ |
|
| |
| |
| |
| |
| | |
This should help with #5675, in particular with
https://github.com/coq/coq/issues/5675#issuecomment-349716292
|
|/
|
|
|
| |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
|\ |
|
| | |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
`make clean`.
|
| |/ / /
|/| | | |
|
| | | |
| | | |
| | | |
| | | | |
Was lost during the coq_makefile 1 -> 2 translation.
|
| |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We remove coqmktop in favor of a couple of simple makefile rules using
ocamlfind. In order to do that, we introduce a new top-level file that
calls the coqtop main entry.
This is very convenient in order to use other builds systems such as
`ocamlbuild` or `jbuilder`.
An additional consideration is that we must perform a side-effect on
init depending on whether we have an OCaml toplevel available [byte]
or not. We do that by using two different object files, one for the
bytecode version other for the native one, but we may want to review
our choice.
We also perform some smaller cleanups taking profit from ocamlfind.
|
|\ \ \ |
|
| |_|/
|/| | |
|
| |/
|/|
| |
| | |
Fixes #6120.
|
|/
|
|
|
|
|
| |
As it is, running a `Makefile.coq` on Windows produces the following error:
`cut: ': No such file or directory`
Changing to double quotes fixes this.
|
|
|
|
| |
execution
|
|\
| |
| |
| | |
coq_makefile are in sync (supersed #1039)…
|
| | |
|
| |
| |
| |
| |
| |
| | |
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).
|
|\ \
| |/
|/| |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
|/ |
|
|\ |
|
| |
| |
| |
| |
| | |
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.
|
|
|
|
| |
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
|
| | |
|