| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The `ide` folder contains two different binaries, the language server
`coqidetop` and `coqide` itself.
Even if these binaries are in the same folder, the only thing they
have in common is that they link to the protocol files. In the OCaml
world, having "doubly" linked files in the same project is considered
a bit of an ugly practice, and some build tools such as Dune disallow it.q
Thus, to clean up the build, we move the common protocol files to its
own library `ideprotocol`.
This helps towards Dune integration and towards having an IDE
standalone target, such as the one that was implemented here:
https://github.com/ejgallego/coqide-exp
|
| | |
|
| |
|
|
|
|
| |
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.
|
| |\ |
|
Emilio Jesus Gallego Arias
Paul Steckler
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