| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
not to be used.
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes
|
|
This has been a mess for quite a while, we try to improve it.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
TODO coqproject handling (for now it can be done through -arg I guess)
|
|
Not sure if the idetop.set_options was correctly changed, ocaml types
pass at least.
|
|
|
|
We alert users that `Vernacstate.Proof_global` is a Coq internal
module and should not be used to workaround lack of state threading.
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: vbgl
|
|
This is necessary to prevent Coq from sending ill-formed output in some
scenarios involving `Timeout`.
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
|
|
This is a fairly small cleanup on the `vernac_interp` function, which
makes code cleaner and for example would allow to have `Load` inside
`Load`. [Not that we would ever want that]
|
|
We try to do a bit of cleanup for the `with_fail` function, this still
is delicate code.
|
|
|
|
Fixes #8320
|
|
|
|
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
|
|
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
Reviewed-by: gares
|
|
|
|
|
|
This fixes #9484 .
|
|
Before #9263 this type was returned by the STM's `parse_sentence`, but
the type was lost on the generalization to entries.
|
|
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
We make `coqc` a truly standalone binary, whereas `coqtop` is
restricted to interactive use.
Thus, `coqtop -compile` will emit a warning and call `coqc`.
We have also refactored `Coqargs` into a common `Coqargs` module and a
compilation-specific module `Coqcargs`.
This solves problems related to `coqc` having its own argument
parsing, and reduces the number of strange argument combinations a
lot.
|
|
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.
|
|
It seems that this command should be classified as modifying the parser.
Fixes #9419
Thanks to @gares
|
|
DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.
This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.
Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.
Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
Reviewed-by: ejgallego
|
|
This makes the implementation of Timeout on unix more reliable
since only the main thread will receive the signal for
timeout.
|
|
This makes code paths clearer (we still factorize a lot of the
treatment), and we seize the opportunity to forbid anonymous
`Declare Instance` which is not a documented construction, and seems to
make little sense in practice.
|
|
|
|
|
|
Reviewed-by: ejgallego
Ack-by: SkySkimmer
Ack-by: gares
Ack-by: ppedrot
|
|
|
|
AFAIK `Fail Instance` cannot open a goal.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
proofs.
We forbid commands that may open proofs inside proofs.
|
|
|
|
Since some state handling refactoring, `purify_stm` was no longer
protecting against assignement of cur_id, resulting in confusing
behavior w.r.t. cache.
|
|
|
|
(fix #9204)
|
|
|
|
workers
|
