| Commit message (Collapse) | Author | Age |
... | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
comments.
[ci skip]
|
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
[ci skip]
|
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
Clarification prompted by Jim Fehrle.
[ci skip]
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |/ / / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
in CArray
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
spawn timeout.
|
| |_|/ / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|/ / / /
|/| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
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
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
instances
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|/ / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/
|/| | | | | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
This follows the model of smartmap and smartmap2.
|
| |_|_|_|_|_|/ / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|/ / / / / / /
|/| | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
As per PR comment suggestion
|
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
There were a few spurious dependencies on the `Vernac` AST in the
pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing,
where they do belong more.
|
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
`Proof_global` is the main consumer of the flag, which doesn't seem to
belong to the AST as plugins show.
This will allow the vernac AST to be placed in `vernac` indeed.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |/ / / / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
This should hopefully alleviate memory problems on gitlab, by first
building the `lite` targets, and then building the remaining
not-that-big targets.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|/ / / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
lib.cma).
|
| |_|_|_|_|_|_|/ / / / / / / / / / /
|/| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
This closes #7580
c.f. https://github.com/coq/coq/pull/7559#issuecomment-390749207 and
https://github.com/coq/coq/pull/7559#issuecomment-390872924. This
should be reverted if and when we move to autogenerated docs for
warnings and errors, as suggested in #7373.
|
| | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |/ / / / / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | |
To reflect reality.
[ci skip]
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | |
multiple lines
|
| |_|_|_|_|_|_|/ / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
It seems that it is standard practice in the OCaml world to set the
`-cclib` flags at library creation time, at least in native libraries.
Indeed, this seems to make linking easier as seen for example in #7563.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / /
|/| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | |
The new implementation is 100% compatible with the previous one, but it
is more compact and does not use a tricky translation function from the
kernel.
|
| |/ / / / / / / / / / / / / / / / / /
|/| | | | | | | | | | | | | | | | | | |
|