| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
Now that we place imperative module declaration on top of module
interpretation we can remove the abstraction layer used in
`Declaremods`, so the `interp_modast` parameter goes away.
Improvement suggested by Gaëtan Gilbert.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: vbgl
Reviewed-by: SkySkimmer
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
|
|
proof data on top of declare.
Reviewed-by: ppedrot
|
|
|
|
top of declare.
This PR is a follow up to #10406 , moving the then introduced
`proof_entry` type to `Declare`.
This makes sense as `Declare` is the main consumer of the entry type,
and already provides the constructors for it.
This is a step towards making the entry type private, which will allow
us to enforce / handle invariants on entry data better.
A side-effect of this PR is that now `Proof_global` does depend on
`Declare`, not the other way around, but that makes sense given that
closing an interactive proof will be a client of declare.
Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into
tactics due to `abstract`, at some point we may be able to unify all
them into a single file in `vernac`.
|
|
We replace some uses of `raise (UserError ...)` with
`CErrors.user_err`, ideally we would like to make the error raising
API not depend on the exception themselves, but that's still a long
way to go.
We also rename the `Timeout` exception as to clarify purpose in the
codebase, given that it has 3 different ones as of today.
cc: #7560
|
|
Reviewed-by: SkySkimmer
|
|
We use the `(coq.pp ...)` dune directive which will produce correct
error messages for `.mlg` files.
Unfortunately we cannot yet use the automatic opam generation features
of Dune 1.10, as this does require a fully native Dune build.
Dune 1.6-1.10 has quite a few other improvements that could be used by
Coq, for example for promote modes.
I have fixed a couple of documentation issues. `Drop` and `ocamldebug`
have been tested in this version.
|
|
TLC and CPDT are not actually tested. No point in keeping them as if they were.
|
|
Reviewed-by: ejgallego
|
|
We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.
This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.
We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
|
|
|
|
We update the URLs to the new ones, even if the previous continue to work.
|
|
|
|
|
|
Ack-by: ejgallego
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: jfehrle
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: mattam82
|
|
We only want stdout, so if there's something in stderr it will both
make a wrong output and make it harder to debug.
|
|
|
|
|
|
|
|
|
|
|
|
the windows crash)
|
|
|
|
|
|
|
|
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.
|
