| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
Ack-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
|
|
Reviewed-by: Zimmi48
|
|
repository
Reviewed-by: SkySkimmer
Ack-by: ejgallego
|
|
This improves reproducibility of the CI environment.
The chosen commit has GTK+3 at 2.24.9.
|
|
Reviewed-by: SkySkimmer
|
|
This removes spurious Ack-by lines
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
The current code does some "opacification" for `Let`s, however that's
pretty fragile in general and not all codepaths do respect it.
We need to decide what to do.
|
|
Reviewed-by: SkySkimmer
|
|
creation.
Reviewed-by: herbelin
|
|
|
|
|
|
We can statically enforce that opaque definitions are always impure by
means of typing, leading to quite a few simplifications.
|
|
This is the last call to the kernel that makes a difference between opaque
definitions depending on their polymorphic status.
|
|
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.
|
|
module.
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
command line (part 1)
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
|
|
|
|
Incidentally fix some missing newline in coqc help, and give proper
help for coqidetop and the "coq*worker"s.
|
|
This is now the "coqidetop" binary which specifically know how to
collect extra arguments.
|
|
- Binding coqc execution to the generic support for Coq binaries
(i.e. to start_coq).
- Moving init_toploop to the init part of coq executables so that coqc
can avoid to call it. By the way, it is unclear what workerloop
should do with it. Also, it is unclear how much the -l option should
be considered an coqidetop or coq*worker option. In any case, it
should be disallowed in coqc, I guess?
- Moving the custom init part at the end of the initialization
phase. Seems ok, despites the few involved side effects.
|
|
We lose track of it at some time in "known_state" and assume that the
reference cur_opt has not been modified in between the time it was set
(in "new_doc") and "known_state".
|
|
|
|
Incidentally moving parsing of "-batch" to the coqtop binary.
|
|
In particular, method init does not do parsing any more.
This allows for instance to let coqidetop treats itself the
"-filteropts" option.
|
|
|
|
A few semantic changes:
- several queries (-where, -config, ...) are accepted
- queries are exclusive of other arguments
- option -filterops is exclusive of other arguments if it contains
another query (this allows to get rid of the "exitcode" hack)
|
|
|
|
|
|
IMHO this functionality doesn't belong in the main code flow of
`Lemmas`, so for now we move it out to its own module, as a principle
to hopefully refactor it more.
We also do some very minor refactoring in `Lemmas`.
|
|
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.
|
|
for list prints in gramlib
Reviewed-by: ejgallego
|
|
Compcert needs a new menhir.
|
|
Order
Reviewed-by: Zimmi48
|
|
gramlib
This means we don't need to ignore the result of the fold. cf #10471
Using Format.pp_print_list instead of a custom iteri was suggested by
Jean-Christophe Léchenet (eponier)
|
|
|
|
Reviewed-by: cpitclaudel
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
