| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
| |
Make sure that when plugin writer does not use -bypass-API,
API is opened by default.
|
| |
|
|
|
| |
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)
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
| |
This goes towards an approach where a local layout can be seen as an
installed layout.
|
| |
|
|
| |
Restores compatibility with 8.6
|
| | |
|
| | |
|
| |
|
|
| |
and avoid duplication
|
| | |
|
| |
|
|
| |
The .mli only acknowledges the current API. I'm not guilty your honor!
|
| | |
|
| |
|
|
|
| |
This removes some remaining support for camlp4 in the infrastructure
and documents the change.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
We now build Coq with `-safe-string`, which enforces functional use
of the `string` datatype. Coq was pretty safe in these regard so only
a few tweaks were needed.
- coq_makefile: build plugins with -safe-string too.
- `names.ml`: we remove `String.copy` uses, as they are not needed.
|
| | |
| |
| |
| | |
No functional changes.
|
| | | |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
| |
|
|
| |
The aux file for foo/bar.v is foo/.bar.aux, not .foo/bar.aux.
|
| | |
|
| |
|
| |
This gives better behavior both when including the `coq_makefile` `Makefile` into other `Makefile`s and when setting `STDTIME` through an environment variable.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing
changes made to da99355b4d6de31aec5a660f7afe100190a8e683.
Hugo asked for more discussion on this topic, and it was not in the roadmap. I
merged it prematurely because I thought there was a consensus. Also, I missed
that it was changing coq_makefile. Sorry about that.
|
| | |
| |
| |
| |
| | |
Coqc now expects physical names for input files, so fix coq_makefile
accordingly.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
make install does not install these *.cm(o|a) files either.
You could always do manually :
- make bytefiles : to build the bytecode *.cm(o|a) files
- make install-byte : to install these files
- make byte : to compile the whole development with the bytecode version
of Coq (this builds the *.cm(o|a) files, but also the .vo via coqc -byte).
Technically, the behavior of make is controlled by the OPT variable,
which could be -byte or -opt. For instance, 'make byte' corresponds to a
'make OPT:=-byte'
Note that coqdep is used with the new option "-dyndep var" : when seeing
a Declare ML Module "foo", "coqdep -dyndep var" does not decide whether to
depend on foo.cma or foo.cmxs, but rather use some Makefile variables such
as foo$(DYNLIB), whose content is later set according to $(OPT)
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| |\ \ \
| | |/
| |/| |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The COQLIBS variable contains some -Q and -I options, which are not
supported by the checker. So this commit introduces a COQCHKLIBS variable
that contains the proper options for coqchk. For the sake of homogeneity,
the COQDOCLIBS variable is also preprocessed in the same way. This means
that both variables have the same value, but they are kept separate in
case the user would like to override one and not the other.
This commit also removes some deprecated options from "coqchk --help".
They are not removed from coqchk itself to preserve backward compatibility
in the branch.
An open question is whether coqchk should support dummy options such as -Q
(interpreted as -R) or -I (ignored).
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This purely cosmetic effect is obtained by the same variables
$(SHOW) and $(HIDE) as in the main Makefile of Coq.
If you prefer the earlier raw output : make VERBOSE=1
|
| | | |
| | |
| | |
| | |
| | | |
Without this, dependencies upon a .ml4 (or a .mlpack) won't be handled
correctly.
|
| | |/
|/|
| |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
Enrico Tassi
Matej Košík
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Hugo Herbelin
Gaetan Gilbert
Vadim Zaliva
Erik Martin-Dorel
Guillaume Melquiond
Jason Gross
Maxime Dénès
Pierre Letouzey
Matthieu Sozeau
Jason Gross
Gregory Malecha