| Age | Commit message (Collapse) | Author |
|---|
|
Related: coq/bignums#17
[ci skip]
|
|
This PR deprecates the use of `coqtop` as a compiler.
There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.
We adapt the documentation and adapt the test-suite.
Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.
The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.
|
|
Apparently it's deprecated / doesn't always work, see
https://tex.stackexchange.com/questions/84041/why-does-calm-n-give-m
See #9429 (we also need to fix the distributed file on the server).
|
|
Reviewed-by: Zimmi48
Reviewed-by: vbgl
|
|
In response to review comments by Zimmi48
|
|
We now support --master and --release. On the master branch, we support
four compatibility versions, while on releases and release branches, we
support only three compatibility versions.
We also support --git-add to automatically run `git add` with new and
updated files, and to run `git rm` with deleted files.
|
|
The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
|
|
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.
|
|
|
|
|
|
|
|
We do a couple of changes:
- Splitting notation keys into more categories to make table smaller.
This should (a priori) make printing faster (see #6416).
- Abbreviations are treated for printing like single notations: they
are pushed to the scope stack, so that in a situation such as
Open Scope foo_scope.
Notation foo := term.
Open Scope bar_scope.
one looks for notations first in scope bar_scope, then try to use
foo, they try for notations in scope foo_scope.
- We seize the opportunity of this commit to simplify
availability_of_notation which is now integrated to
uninterp_notation and which does not have to be called explicitly
anymore.
|
|
|
|
|
|
|
|
|
|
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 is documented in dev/doc/changes.md.
|
|
|
|
Now that the checker is using the regular kernel files it can also use
the normal printers.
|
|
Following discussion in #7042, we write down an advice to give time
for last comments before merging potentially controversial PRs.
We document a practice that is becoming standard in order to improve
PR merging time: some other maintainer can self-assign if the main
maintainer is not responding.
Encourage component maintainers to announce when they won't be available.
We document the practice of code owner teams.
Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
|
|
|
|
|
|
We update the docs for the removal of `Sigma` and the deprecation of
`enter_nf`.
|
|
As noted by Gäetan, we didn't compile these. We also provide a recipe
to run `ocamldebug`. Try (after a build):
```
dune exec dev/dune-dbg
(ocd) source dune_db
```
or
```
dune exec dev/dune-dbg checker
(ocd) source checker_dune_db
```
for the checker.
|
|
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.
|
|
|
|
|
|
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
|
|
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.
|
|
|
|
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.
|
|
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).
|
|
|
|
|
|
|
|
|
|
As suggested on Gitter by @maximedenes we improve documentation and
update Kernel's `.merlin` so it actually reports on the stricter set
of warnings.
We also set the language version to the proper one so users will get a
better error message [the fact that we can use `(env_var ...)` with
the wrong Dune version is a Dune bug indeed].
|
|
Closes #7380. Ubuntu 18.04 and Debian Buster will ship this OCaml
version so it makes sense we bump our dependency to 4.05.0 as we can
use some newer compiler features.
|
|
The functions in `Termops.print_*` are meant to be debug printers,
however, they are sometimes used in non-debug code due to a API
confusion.
We thus wrap such functions into an `Internal` module, improve
documentation, and switch users to the right API.
|
|
After the introduction of `EConstr`, "normalization" has become
unnecessary, we thus deprecate the `nf_*` family of functions.
Test-suite and CI pass after the fix for #8513.
|
