| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We move toplevel/STM flags from `Flags` to their proper components;
this ensures that low-level code doesn't depend on them, which was
incorrect and source of many problems wrt the interfaces.
Lower-level components should not be aware whether they are running in
batch or interactive mode, but instead provide a functional interface.
In particular:
== Added flags ==
- `Safe_typing.allow_delayed_constants`
Allow delayed constants in the kernel.
- `Flags.record_aux_file`
Output `Proof using` information from the kernel.
- `System.trust_file_cache`
Assume that the file system won't change during our run.
== Deleted flags ==
- `Flags.compilation_mode`
- `Flags.batch_mode`
Additionally, we modify the STM entry point and `coqtop` to account
for the needed state. Note that testing may be necessary and the
number of combinations possible exceeds what the test-suite / regular
use does.
The next step is to fix the initialization problems [c.f. Bugzilla],
which will require a larger rework of the STM interface.
|
| |\ |
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
empty queues.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | | |
Undo & friends is very expensive in batch mode as backtracking state
is not kept and thus should be recomputed.
We thus warn the user.
|
| | |/
|/|
| |
| |
| |
| |
| | |
This was not used anywhere; it looks like dead code from some previous
attempt.
`get_hint_ctx` looks also very very suspicious.
|
| | | |
|
| | | |
|
| | | |
|
| |/
|
|
|
| |
While this is a good workaround, Enrico has a minimal example of the
underlying issue that we will send to the OCaml team.
|
| |\ |
|
| | |
| |
| |
| | |
Minor clean up, no sense in having these as they do nothing.
|
| |/ |
|
| |
|
|
|
| |
We only delay monomorphic proofs in quick mode, so that their universe context
will always be empty.
|
| |
|
|
|
| |
We aditionally return the abstract universe context inside the option. This
is relatively painless as most uses were using the option as a boolean.
|
| | |
|
| |\
| |
| |
| | |
`VernacStartTheoremProof`
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
`VernacStartTheoremProof` contained a stale bool parameter from 15
years ago, which is unused today.
|
| | |/
|/|
| |
| |
| |
| | |
This is a fix for a mistake in
d8874dd855d748aaaf504890487ab15ffd7a677d , where we forgot to
propagate the route parameter.
|
| | |
| |
| |
| |
| |
| | |
Used to report to the UI an Error feedback message whenever a
worker was non making any progress. This is wrong since no-progress
is fine (as long as one does not specify "solve")
|
| |\ \ |
|
| | |/
| |
| |
| |
| |
| |
| |
| | |
This is necessary in order for clients to identify the results of
queries. This is a minor breaking change of the protocol, affecting
only this particular call.
This change is necessary in order to fix bug ####.
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.
We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Reminder of (some of) the reasons for removal:
- Despite the claim in sigma.mli, it does *not* prevent evar
leaks, something like:
fun env evd ->
let (evd',ev) = new_evar env evd in
(evd,ev)
will typecheck even with Sigma-like type annotations (with a proof of
reflexivity)
- The API stayed embryonic. Even typing functions were not ported to
Sigma.
- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
at all (despite still being so).
- There was no good story for higher order functions manipulating evar
maps. Without higher order, one can most of the time get away with
reusing the same name for the updated evar map.
- Most of the code doing complex things with evar maps was using unsafe
casts to sigma. This code should be fixed, but this is an orthogonal
issue.
Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.
|
| |\ \ |
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
| | |
| |
| |
| |
| | |
We remove the emacs-specific printing code from the core of Coq, now
`-emacs` is a printing flag controlled by the toplevel.
|
| |/
|
|
|
| |
Any users of this API should coordinate with the ongoing work in PRs
numbered #459 and #566.
|
| |\ |
|
| | |
| |
| |
| | |
As suggested by @gares, now the meaning becomes way clearer.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |/
|
|
| |
This is a minor cleanup.
|
| |\ |
|
| |\ \ |
|
| | |/
| |
| |
| |
| |
| |
| |
| | |
We allow for a dynamic setting of the STM debug flag, and we print
some more information about the result of `process_transaction`.
We also fix a printing bug due to mixing `Printf` and `Format`, which
are not compatible.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
| |/
|
|
| |
Now it is a private field, locations are optional.
|
| |\ |
|
Emilio Jesus Gallego Arias
Maxime Dénès
Hugo Herbelin
Matej Košík
Pierre-Marie Pédrot
Enrico Tassi
Amin Timany
Jason Gross
Gaetan Gilbert