| Age | Commit message (Collapse) | Author |
|---|
|
|
|
workers
|
|
|
|
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`]
CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit`
cannot be currently installed, thus we have to add a switch to the
test suite to disable `unit-tests`.
Many deprecation warnings happened in 4.08 so we use the `release`
profile to make them not fatal. Using a 4.08 build profile would be an
option too.
|
|
- deprecate the old 5-tuple accessor in favor of a view record,
- move `name` and `kind` proof data from `Proof_global` to `Proof`,
this will prove useful in subsequent functionalizations of the
interface, in particular this is what abstract, which lives in the
monads, needs in order no to access global state.
- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
|
|
|
|
This is a reduced version of #8503 as to provide a way to build the
reference manual with Dune.
Dune 1.6 supports (experimentally) directories as targets, thus we
introduce a rule that will call `sphinx` to build the manual.
This only provides build, however generation of `.install` rules is
not done, it will be hopefully addressed in #8503.
Note that we set `expire: 1 month` for all the artifacts we build with
Dune. IMHO this makes most sense as not to abuse Gitlab's hosting,
however of course we could consider a different deployment strategy if
wanted.
|
|
Hopefully we will re-enable it back soon, I am preparing a refactoring
that should make it more robust w.r.t paths and changes on Windows
which will enable to use a faster build system.
But now it is timing out 100% of the times [due to #8655] so it is not
useful.
|
|
comments.
|
|
|
|
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
|
|
|
|
|
|
|
|
We make `declaration_hook`s optional arguments everywhere, and thus we
avoid some "fake" functions having to be passed.
This identifies positively the code really using hooks [funind,
rewrite, coercions, program, and canonicals] and helps moving toward
some hope of reification.
|
|
The types are identical and we have no more reason for the split. Note
the following TODOS:
- discrepancy of `Ploc.after` with `CLexer.after`
- discrepancy of `Ploc.comments` with `CLexer.comments`
- `Ploc.dummy` vs `Loc.t option`
|
|
|
|
|
|
Co-authored-by: Michael Soegtrop <michael.soegtrop@intel.com>
|
|
We remove a few aliases present in the lower layers
[`Genintern/Tactypes`] from `Tacexpr`.
IMHO this enlarges the API for no good purpose, and difficults
analysis.
|
|
We update the Appveyor configuration so it uses OPAM 2.0, and thus it
can install newer packages.
|
|
|
|
|
|
|
|
optional.
|
|
Thanks to @Zimmi48 as always for the careful review.
Co-Authored-By: ejgallego <e+git@x80.org>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
pidetop relies on some rather low level API from STM, which we'd like to
change. It does not seem maintained much anymore, and still hasn't moved
to github.
|
|
|
|
|
|
|
|
We remove the `Proof_types` file which was a trivial stub, we also
cleanup a few layers of aliases.
This is not a lot but every little step helps.
|
|
This makes the make-based build system stop linking to Camlp5's
gramlib and instead links to our own gramlib.
We use the style done in the packing of `Stdlib` in OCaml 4.07.
As to introduce a minimal amount of noise in history we use an
autogenerated `gramlib__pack` directory.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Looks like we forgot to adapt this when we split off the sphinx job
and stopped using -with-doc yes.
|
|
|
|
|
|
|
|
|
|
|
|
This is very preliminary but you should get the idea. The script tries
to build contribs, then creates a branch and sets the remote properly
as to submit a PR.
Usage example:
```
./dev/tools/create_overlays.sh ejgallego 9999 ltac2 elpi
```
This only works for contributions hosted in github for now.
|
|
We group the extension API and datatypes under `Vernacextend`.
This means that the base plugin dependency is now `coq.vernac` from
`coq.stm`.
This is quite important as for example the LSP server won't like to
link the STM in.
LTAC still depends on the STM by means of the ltac_profile part tho.
The next step could be to move the extension point below `Vernacexpr`.
|
|
This is convenient as to have better automation.
|
|
|
