| Age | Commit message (Collapse) | Author |
|---|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
Reviewed-by: gares
Ack-by: herbelin
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
|
|
Contrarily to the comments, Coq_config.date was not the "release date" but
just another "compile date".
|
|
We expose the representation function in UGraph and change the printer
signature to work over the representation instead of the abstract type.
Similarly, the topological sorting algorithm is moved to Vernacentries.
It is now even simpler.
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
When encountering
```Coq
Module M : T.
...
Lemma c :...
...
Qed.
...
End M.
```
every field `c` without body in `T` but with a body in `M` is
registered as opacified in a table along with all constants
`opacified(c)` without body in the environment at this point (i.e.,
all axioms potentially used by c).
Then, when printing axioms, if `c` appears in the final environment it
is replaced by `opacified(c)` in the resulting list of axioms.
|
|
Add headers to a few files which were missing them.
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
|
|
Prevent errors when under annotating binders.
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
The `-boot` option was used to:
- suppress loading of the rc_file
- allow to save modules with prefix `Coq`
There is no good reason disable saving of modules with `Coq` prefix by
default, thus we remove this option.
Fixes: #9575
|
|
In passing add -coqlib to coqchk's usage message.
|
|
Instead, if the coqlib is special, we set it explicitly in the command
line, as Dune does.
This is a continuation of #9523.
In Sphinx, we stop using -boot, and pass `-coqlib` through the
environment instead.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
|
|
|
|
|
|
At the same time, we made the safe_env threading explicit.
|
|
For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.
With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.
We also rename some files from the checker so that they don't clash with
kernel files.
|
|
univs
|
|
Followup for #8341.
Not making a test as that's too difficult with our current infrastructure.
|
|
The relevant logic is already in `Envars`, so it makes sense to make
it private and don't expose the low-level implementation of the logic.
|
|
Makes printing rules more explicit and should close #6799.
|
|
|
|
The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with `Feedback.msg_error`.
As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of `msg_error`
must raise an exception of print at a different level [for now].
|
|
|
|
|
|
It is not doing the same thing as coqtop, and the corresponding coqtop
semantics is irrelevant in the checker as the latter does not rely on ML
code.
|
|
It has exactly the same effect as -R, because there is no such thing as
implicit relativization for object files in coqchk, contrarily to what
Require does in coqtop.
|
|
|
|
This is useful for tools such as `coqchk` or `coq_makefile` that want
to handle feedback on their own.
|
|
|
|
|
|
This fixes longstanding bug likely introduced in the first `pp` to
`Feedback` migration, namely the checker didn't register a feedback
printer, thus no calls to `Feedback.msg_*` were printed in the
checker.
This closes bug: https://coq.inria.fr/bugs/show_bug.cgi?id=5587
We fix this by adding a custom printer to the checker, this is correct
as the checker owns now the full console, however a cleanup should
happen in any of these two directions:
- all the calls to feedback are removed, and the checker always uses
its own printing mechanism.
- all the calls to `Format/Printf` are removed and the checker always
uses the `Feedback` mechanism.
Currently, I have no opinion on this.
|
|
An incoming commit is removing some toplevel-specific global flags in
favor of local toplevel state; this commit flags `Flags` use so it
becomes clearer in the code whether we are relying on some "global"
settable status in code.
A good candidate for further cleanup is the pattern:
`Flags.if_verbose Feedback.msg_info`
|
|
|
|
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
|
|
|
|
|
|
|
Was PR#257: [checker] Fix/fine tune printing.
|
|
in error messages
|
