| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
| |
We update the instructions a bit providing the name of the Debian
packages, we also mention Nix and add to .gitignore a
Sphinx-autogenerated file.
|
| | |
|
| | |
|
| |
|
|
| |
longer use camlp4.
|
| | |
|
| |
|
|
|
| |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |\
| |
| |
| | |
wrongly tagged as keywords
|
| | |
| |
| |
| |
| |
| |
| | |
One file was already ready for testing. We add another one.
Note that we have to remove the machine-dependent lines in the output
tex files.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
| |
Rules for ignoring *some* PDF files had been added one by one to `.gitignore`
but some were still missing (for the corresponding latex files in `dev`).
This rule is actually better since we are not tracking any PDF file.
|
| |
|
|
|
|
|
| |
of this file
There is now a warning if the content of micromega.ml isn't what MExtraction.v would
produce.
|
| |
|
|
|
|
| |
See now https://github.com/coq/bignums
Int31 is still in the stdlib.
Some proofs there has be adapted to avoid the need for BigNumPrelude.
|
| |\ |
|
| | |
| |
| |
| | |
generate them later.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Plugin-writers can now use:
-bypass-API
parameter with "coq_makefile".
The effect of that is that instead of
-I API
the plugin will be compiled with:
-I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
|
| | | |
|
| | | |
|
| |/ |
|
| |
|
|
| |
"plugins/micromega/MExtraction.v"
|
| | |
|
| | |
|
| |
|
|
| |
The .mli only acknowledges the current API. I'm not guilty your honor!
|
| | |
|
| |
|
|
|
|
|
|
| |
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
|
| |
|
|
|
| |
- Move the git clones to a specific subfolder to avoid pollution.
- Do not fail when git clone already exist (but make sure it is up-to-date).
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This file was only used during ocamldebug sessions (in the dev/db
script). It was containing a large subset of the core cma files,
up to the printing functions. There were a few notable exceptions,
for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug.
But printers.cma was troublesome to maintain : almost each time an ML file
was added/removed/renamed in the core of Coq, dev/printers.mllib
had to be edited, in addition to the directory-specific .mllib
(kernel/kernel.mllib and co). So I propose here to kill this file,
and put instead in dev/db several "load_printer" of the core cma files.
For that to work, we need to compile kernel/kernel.cma with the right
-dllib and -dllpath options, but that shouldn't hurt (on the contrary).
We also source now the camlpX cma in dev/db, via a new generated file
dev/camlp4.dbg containing a load_printer of either gramlib.cma or
camp4lib.cma.
If one doesn't want to perform the whole "source db" at the start
of an ocamldebug session, then the former "load_printer printers.cma"
could be replaced by:
source core.dbg
load_printer top_printers.cmo
See for instance the minimal dev/base_db.
|
| |\| |
|
| | | |
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
For now, the pack name reuse the previous .cma name of the plugin,
(extraction_plugin, etc).
The earlier .mllib files in plugins are now named .mlpack.
They are also handled by bin/ocamllibdep, just as .mllib.
We've slightly modified ocamllibdep to help setting the -for-pack
options: in *.mlpack.d files, there are some extra variables such as
foo/bar_FORPACK := -for-pack Baz
when foo/bar.ml is mentioned in baz.mlpack.
When a plugin is calling a function from another plugin, the name
need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz).
Btw, we discard the generated files plugins/*/*_mod.ml, they are
obsolete now, replaced by DECLARE PLUGIN.
Nota: there's a potential problem in the micromega directory,
some .ml files are linked both in micromega_plugin and in csdpcert.
And we now compile these files with a -for-pack, even if they are
not packed in the case of csdpcert. In practice, csdpcert seems
to work well, but we should verify with OCaml experts.
|
| |/
|
|
|
|
| |
This add LtacProfiling. Much of the code was written by Tobias Tebbi
(@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq
v8.5 and Coq trunk.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
This makes the core free from particular protocol choices.
It should help with the ppx serialization project and shrinks clib.cma a
bit.
|
| |\ |
|
| | | |
|
Paul Steckler
Emilio Jesus Gallego Arias
Maxime Dénès
Jim Fehrle
Jason Gross
Enrico Tassi
Théo Zimmermann
Hugo Herbelin
Jason Gross
Pierre Letouzey
Matej Košík
Pierre-Marie Pédrot
Matej Kosik