| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
| |
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
|
| | |
|
| | |
|
| |\
| |
| |
| | |
fiat-crypto/OSX
|
| | |
| |
| |
| | |
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.
|
| |/ |
|
| |
|
|
|
|
|
|
| |
This fixes #6350 (and even comes with a test case).
Refering to other directories as `-R … ""` is maybe not best practice,
but some people out there do it, so as long as it does not cause too
much trouble, we can continue to support it.
|
| |
|
|
|
| |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| |
|
|
|
| |
This allows to fix the non-printing of error messages produced when
parsing arguments.
|
| |
|
|
| |
This was apparently either silently doing nothing or failing.
|
| |
|
|
|
|
|
|
| |
Nevertheless making option -o of coq_makefile recommended as discussed
in PR#6040.
This is one way to resolve the inconsistency with the usage which says
that all arguments are optional.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
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)
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
Benjamin Barenblat
Gaëtan Gilbert
Enrico Tassi
Maxime Dénès
Gaëtan Gilbert
Théo Zimmermann
Joachim Breitner
Hugo Herbelin
Ralf Jung
Guillaume Melquiond
Matej Košík
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Vadim Zaliva
Erik Martin-Dorel
Jason Gross
Pierre Letouzey
Matthieu Sozeau