| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
This is almost a full rewrite of the contributing guide. The goal was
to have a more structured, and more exhaustive guide, where all our
processes are documented, and from which all the useful documentation
is linked to.
The document lists contribution types in the order in which it is most
natural to go through them: from contributions to the ecosystem, to
issues, to code contributions, to taking part in the maintenance.
However, it seemed important to not neglect this last part if we want
to ease the onboarding of new maintainers (and not just of occasional
contributors).
A table of content makes it easy to go through the document (which is
too long to be read from begin to end).
The guide documents our processes in the way they are today, without
changing anything, but this should be a good basis to make them evolve
in the future. Insufficiently documented tools and processes are
mentioned as such.
|
|
This removes spurious Ack-by lines
|
|
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
|
|
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
We remove the special error printing pre-processing in favor of just
calling the standard printers.
Error printing has been a bit complex for a while due to an incomplete
migration to a new printing scheme based on registering exception
printers; this PR should alleviate that by completing the registration
approach.
After this cleanup, it should not be ever necessary for normal
functions to worry a lot about catching errors and re-raising them,
unless they have some very special needs.
This change also allows to consolidate the `explainErr` and `himsg`
modules into one, removing the need to export the error printing
functions. Ideally we would make the contents of `himsg` more
localized, but this can be done in a gradual way.
|
|
Fixes #10465
Following discussion we don't allow a generic `/usr/bin/python`
shebang anymore. We thus move all the scripts [but one] to python3,
and add python3 to the Azure base environment.
Unfortunately we still depend on python2 for the update-compat.py
script, see #10491
We thus have to complement #10467 adding python2 back to Nix,
until #10491 is fixed.
|
|
Compcert needs a new menhir.
|
|
|
|
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
And also clean INSTALL file of useless reminder of the procedure to
install using a package manager.
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
- fix the printers themselves after discharge was moved to the kernel
- change the test to make it more robust
In addition to checking that there is no "Error|Unbound" in the
output, ensure that the "go" function at the end of base_include
is defined. If there are any errors in base_include it won't be defined.
This makes us find out that the test was silently failing in all CI
jobs except trunk+make. It failed to find the "include" file and so
failed with "could not find file include.", which we didn't detect.
To fix this:
- change automatically included paths in Coqinit.init_ocaml_path to be
based on coqlib instead of coqroot. This way top_printers.ml and
base_include can find the compiled ml objects.
- fix for dune: adapt the script to use include_dune when INSIDE_DUNE,
add dependencies to test-suite/dune.
The dependencies should be calculated automatically once Dune has
better support for debug, or we implement proper support for test
printers.
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
|
|
|
|
|
|
obligation ones.
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Remove other types of lines before copyright headers.
|
|
|
|
|
|
|
|
ml-style headers.
|
|
|
|
works on MacOS X
Reviewed-by: SkySkimmer
|
|
Works fine here, cc: #9975
|
|
|
|
Unfortunately, "+" regular expressions are not supported by default
with MacOS X's sed.
It is told that it would work with option -E though, but the syntax
seems then different.
|
|
|
|
Ack-by: ejgallego
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
Reviewed-by: vbgl
|
|
Reviewed-by: SkySkimmer
|
|
definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
|
|
|
|
|
|
- Switch gtksourceview to 3.24.11
- Add appropriate set of icons and some other files GTK3 requires
- Add fix for ocamldebug so that this can be debugged
|
|
|
|
The stm.ml changes show that for the other classifications either the
vernac_when was ignored, or there was an assert on it forcing it to be
Now or Later depending on the vernac_type.
One may also note that the classification used in top_printers
`VtQuery,VtNow` would have failed those asserts...
|
|
|
|
Closes #10353
May be blocked on #10352
|
|
|
|
The main idea of this PR is to distinguish the types of "proof object"
`Proof_global.t` and the type of "proof object associated to a
constant, the new `Lemmas.t`.
This way, we can move the terminator setup to the higher layer in
`vernac`, which is the one that really knows about constants, paving
the way for further simplification and in particular for a unified
handling of constant saving by removal of the control inversion here.
Terminators are now internal to `Lemmas`, as it is the only part of
the code applying them.
As a consequence, proof nesting is now handled by `Lemmas`, and
`Proof_global.t` is just a single `Proof.t` plus some environmental
meta-data.
We are also enable considerable simplification in a future PR, as this
patch makes `Proof.t` and `Proof_global.t` essentially the same, so we
should expect to handle them under a unified interface.
|
|
Reviewed-by: aspiwack
Ack-by: ejgallego
Reviewed-by: ppedrot
|
