| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
After #12504 , we can encapsulate and consolidate low-level state
logic in `Vernacstate`, removing `States` which is now a stub.
There is hope to clean up some stuff regarding the handling of
low-level proof state, by moving both `Evarutil.meta_counter` and
`Evd.evar_counter_summary` into the proof state itself [obligations
state is taken care in #11836] , but this will take some time.
|
|
|
|
|
|
|
|
|
|
|
|
This is needed in rewriter as to avoid hack; indeed it makes sense to
propagate this information to the callers of save.
|
|
This completes the refactoring [for now] of the core `Declare`
interface, and will allow much internal refactoring in the future.
In particular, we remove the low-level Proof_ending type, and instead
introduce higher-level constructors for the several declare users.
Future PRs will change the internal representation of proof handling
to better enforce some invariants that should hold for specific
proofs.
|
|
This allows us to remove a large chunk of the internal API, and is the
pre-requisite to get rid of [Proof_ending], and even more refactoring
on the declare path.
|
|
We unify information about constants so it is shared among all the
paths [interactive, NI, obligations].
IMHO the current setup looks pretty good, with information split into
a per-constant record `CInfo.t` and variables affecting mutual
definitions at once, which live in `Info.t`.
Main information outside our `Info` record is `opaque`, which is
provided at different moments in several cases.
There are a few nits regarding interactive proofs, which will go away
in the next commits.
|
|
This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
|
|
|
|
|
|
This improves the interface, and allows even more sealing of the API.
This is yet work in progress.
|
|
The module is now a stub. We choose to be explicit on the parameters
for now, this will improve in next commits with the refactoring of
proof / constant information.
|
|
At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.
|
|
Having two different modules led to the availability of internal API in
the mli.
|
|
|
|
|
|
Reviewed-by: CohenCyril
Reviewed-by: ppedrot
|
|
|
|
|
|
Add Zify <X> are documented.
Add <X> is deprecated as it clashed with the standard Add command
|
|
|
|
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
- insert boolean constraint (b = true \/ b = false)
- add specs for b2z
- zify_post_hook performs a case-analysis over boolean constraints
- Stricter typing constraints for `zify` declared operators
The type is syntactically checked against the declaration of injections.
Some explicit casts may need to be inserted.
|
|
The syntax of formulae is extended to support boolean constants (true,
false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb,
Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and
Z.ltb.
|
|
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: ppedrot
|
|
It was deprecated in 8.12 and not used in the wild.
|
|
eta-expansion of "match" branches
Reviewed-by: gares
Ack-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
|
|
We complete some arduous refactoring in order to bring all the
internals and code of constant / proof saving into the same module.
In particular, this PR moves the remaining parts of proof saving from
`Lemmas` to `Declare`.
The reduction in exposed internals is considerable; in particular, we
remove the export of the internals of `proof_entry` and `proof_object`
[used in delayed proofs], which will allow us to start to address many
issues with the current setup, such as #10363 .
There are still some TODOs, that will be addressed in subsequent PRs:
- Remove `declare_constant` in favor of higher-level APIs
- Then, remove access to `proof_entry` entirely
- Refactor current very verbose handling of proof info.
- Remove compat modules / API.
- Rework handling of delayed proofs [this may be hard due to state and the STM]
- Reify Hook API for the case where it acts as a continuation [that is to say, declaring constants from the Hook]
List of remaining offenders for `proof_entry` / `declare_constant` in
the codebase:
- File "vernac/comHints.ml"
- File "vernac/indschemes.ml"
- File "vernac/comProgramFixpoint.ml"
- File "vernac/comAssumption.ml"
- File "vernac/record.ml"
- File "plugins/ltac/leminv.ml"
- File "plugins/setoid_ring/newring.ml"
- File "plugins/funind/recdef.ml"
- File "plugins/funind/gen_principle.ml"
|
|
but ssrsearch is not loaded.
Fixes #12338
|
|
Reviewed-by: ejgallego
|
|
Analysis by Jason Gross:
> The previous semantics was to reset the file offset to 0 during the
> unlock operation, unless it fails, in which case you'd roll back the
> file offset to it's present position (and very dubiously not report
> any issues). The new semantics say to always roll the file offset
> back to it's initial position, meaning that the position is at the
> end of the file after unlocking. As far as I can tell, this results
> in appending marshelled blobs to the cache file on every call to
> add, rather than overwriting the cache file with the marshelled blob
> of the updated table. Presumably unmarshelling the concatenation of
> marshelled data can result in segfaults somehow? This also explains
> why the bug only shows up sometimes; you need to get the system into
> a state where it writes to the cache in a way that concatenates
> blobs in the right way, but once you have such a cache you'll
> segfault every time you read from it.
>
> I think we should probably assert false in the with block, or just
> remove it entirely http://man7.org/linux/man-pages/man3/lockf.3.html
> doesn't say anything about lockf erroring on unlocking). If we start
> seeing errors, we can turn it into a warning.
Closes: #12072
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: kyoDralliam
|
|
Error happened only when writing:
functional induction f x y z.
instead of
functional induction (f x y z).
Now the former is equivalent to the former: implicits must be omitted.
Hence small source of incompatibility, but a more homogeneous
behaviour.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
|
|
- new clauses "hyp:", "concl:", "headhyp:" and "headconcl:" to restrict
match to an hypothesis or the conclusion, possibly only at the head
(like SearchHead in this latter case)
- new clause "is:" to search by kind of object (for some list of kinds)
- support for any combination of negations, disjunctions and conjunctions,
using a syntax close to that of intropatterns.
|
|
Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
|
