| Age | Commit message (Collapse) | Author |
|---|
|
We need to update in Docker:
- dune to 1.4.0: as it honors `-p` on test stanzas
- dune-release to 1.1.0: support for OPAM 2.0 + fixes
This makes `dune-release distrib` / `dune-release opam pkg` work.
TODO: we need to figure out what is going on with the
versioning. Should we do `dune subst` on `pinned`?
|
|
This includes many changes, please have a look at the newly generated
docs.
|
|
|
|
This fixes the CI until this commit is merged into master.
|
|
We had a brief leftovers of the ocamlbuild experiment that are not
relevant anymore as it was removed from the tree a few years ago.
p.s: The amount of cruft we have in the `dev/build/windows` folder is
staggering, see for example what `git grep ocamlbuild` returns.
|
|
|
|
Those optional arguments did not really make sense. It was pretty clear from
our code base, as all instances where triplicating the same type for TYPED,
RAW_TYPED and GLOB_TYPED.
|
|
|
|
Fixes #8337
|
|
Not a big point on running the checker on Appveyor I think, this will
save a bunch of time and improve reliability.
|
|
"Declaration" hooks can be polymorphic on their return type, however
this facility doesn't seem used in the codebase.
We thus remove the polymorphism with the hope to be able to reify the
control later on.
|
|
|
|
|
|
We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.
This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.
Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
This satisfies a wish by @ppedrot
|
|
And fix a typo that was previously there.
|
|
|
|
|
|
|
|
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This was broken due to a typo when introducing the archive download
method.
We also remove default [master] values from basic-overlay which hid
this issue.
|
|
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
|
|
|
|
|
|
This was mostly a matter of adding backquotes and indentation where
needed. There were also some "combining grave accent" used in place of
proper backquotes.
I cleaned only the changes of the most recent releases.
|
|
The Dune `release` profile is used by OPAM so that should cover the
testing.
We also update the dependencies:
- camlp5: 7.01 had some bugs regarding grammar; we could use 7.02,
however this version it is not in OPAM. So I guess that leaves us
with 7.03 again.
- lablgtk < 2.18.5 does not support OCaml >= 4.05.0.
|
|
|
|
|
|
|
|
|
|
Implemented by merging addon changes in V8.8.2 (keeping everything on master)
|
|
|
|
Fixes #8621
|
|
compat updates to do as part of a release.
|
|
|
|
|
|
This PR removes support for `ocamldoc` in favor of `odoc`.
Following a recent discussion in OCaml's discord, it turns out that
basically all the ecosystem has migrated to odoc, thus we follow suit
and may focus on `odoc` for Coq's ML API documentation.
|
|
Also test that the compat updating script hasn't become outdated on the
CI.
|
|
As requested in
https://github.com/coq/coq/issues/8311#issuecomment-415976318
the release process describes the steps to take.
All automatable steps are taken by the new script
dev/tools/update-compat.py
I've tried to make the script relatively easy to update if functions get
renamed or moved, but since it's doing unstructured source manipulation,
it is sort-of fragile.
We could plausibly add a file to the test-suite to ensure that we catch
script-breakage early, but this would require dropping compatibility
support much earlier in the development cycle (the compatibility changes
would have to come right when the new version is branched, rather than
shortly before the beta release).
|
|
I forgot to update `.PHONY` and to put the proper flags in the new
workspace file.
|
|
build to …
|
|
|
|
_log.txt and _err.txt so that they can be viewed immediately in gitlab
|
