| Age | Commit message (Collapse) | Author |
|---|
|
Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.
Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.
|
|
|
|
|
|
Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and
kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program
rather than a pipeline of sed and awk text processing.
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
Reviewed-by: ejgallego
Ack-by: SkySkimmer
Ack-by: gares
Ack-by: ppedrot
|
|
The variable QUICK enables the quick compilation chain:
- all v files are compiled with -quick to vio files (also
-native-compiler no, since it is quicker)
- then all vio files are turned to vo files $NJOBS at a time
All occurrences of .vo use now .$(VO) that can be either
.vo or .vio depending of QUICK being defined. Targets that
only make sense for .vo files have to use $(VAR:.$(VO)=.vo)
|
|
|
|
It's a bit cleaner this way, especially wrt the number of toplevel directories.
Also fix warning about undefined GRAMMARCMA while we're at it.
|
|
|
|
This makes the make-based build system stop linking to Camlp5's
gramlib and instead links to our own gramlib.
We use the style done in the packing of `Stdlib` in OCaml 4.07.
As to introduce a minimal amount of noise in history we use an
autogenerated `gramlib__pack` directory.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
|
|
We make `config` into a properly library. This is more uniform and
useful for some clients. This also matches what was done in Dune.
Next step would be to push dependencies on `Coq_config` upwards, only
the actual toplevel binaries should depend on it.
We also remove the stale `camlp5.dbg` and refactor the dbg files a
bit, isolating the bits that are specific to the plugin / lib building
method used by makefile.
|
|
We had a brief leftovers of the ocamlbuild experiment that are not
relevant anymore as it was removed from the tree a few years ago.
p.s: The amount of cruft we have in the `dev/build/windows` folder is
staggering, see for example what `git grep ocamlbuild` returns.
|
|
This PR removes support for `ocamldoc` in favor of `odoc`.
Following a recent discussion in OCaml's discord, it turns out that
basically all the ecosystem has migrated to odoc, thus we follow suit
and may focus on `odoc` for Coq's ML API documentation.
|
|
|
|
|
|
|
|
|
|
There's no need to build dependencies for it.
|
|
For now we only copy the templates, but we could do more fancy stuff.
This helps to be compatible with build systems that take care of these
files automatically, see:
https://github.com/coq/coq/pull/6857#discussion_r202096579
|
|
coqtop.opt$(EXE).
|
|
|
|
Fixes #7758.
|
|
The parser is stupid and the syntax is almost the same as the previous one.
The only difference is that one needs to wrap OCaml code between { braces }
so that quoting works out of the box.
Files requiring such a syntax are handled specifically by the type system
and need to have a .mlg extension instead of a .ml4 one.
|
|
|
|
Building this target installs the files that are used by merlin:
- .merlin files (.merlin);
- bin-annot files (.cmt, .cmti);
- source files (.ml, .mli).
Plug-in developpers can thus work with an “installed” version of Coq.
|
|
|
|
We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:
- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.
In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:
- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.
|
|
|
|
|
|
This removes the "leftover files without known source" error in favor
of automatic handling.
|
|
|
|
The original contribution is from Clément Pit-Claudel. I updated
his code and integrated it with the Coq build system. Many improvements
by Paul Steckler (MIT).
This commit adds the infrastructure but no content.
|
|
|
|
longer use camlp4.
|
|
|
|
repository. Also removing FAQ-related build rules.
|
|
When statically linking plugins, the "DECLARE PLUGIN" macro takes care
of properly setting up the loaded module table.
This setup was also done by `coqmktop`, thus in order to ease
bisecting, we didn't take care of it in the `coqmktop` deprecation.
Fixes #6364.
|
|
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.
|
|
|
|
|
|
- timing needs time and python
- check for compiled files without source looks in the install
directory (except for make -f Makefile.ci which doesn't check), as
such the install directory has been renamed to _install_ci and isn't
searched.
|
|
This is crucial for the search for binary files without known
sources (commit 7d1fc1), since coq_makefile currently doesn't
install in user-contrib the ML sources of plugins.
This could also helps for variables such as $(EXISTINGML).
|
|
This is a followup of 7d1fc15. Without this fix, you're warned of leftover files,
but even a 'make clean' is then refused, so you cannot get rid of them easily
(apart via a git clean -xfd).
|
|
|
|
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.
|
