BreakOut 2020 11 30 Lasse
attending: Emilio Gallego, Gaëtan Gilbert, Lasse Blaauwbroek
As of now: hack to redefine every tactic as a "side-effect" that is to
say, modifying the Summary
. This creates many problems.
Suggestion: Keep tactic state in the evar_map
, a first-try PR would go like this:
- modify
Declare
, such that: -
Proof.start
reads from the summary and updates theevar_map
with the custom state. - Add a field to
proof_object
to keep the custom state at end of proof. - update
close_proof
andclose_delayed_proof
to put the state in the new field. - update
save
andsave_lemma_proved_delayed
to push the state into summary.
Comments:
GG: what happens with nested proofs? does it matter? EJGA: I think with the above the proofs would look like independent. This may actually be a good thing. just call it not supported I guess
Lemma foo : ...
Proof. (* pstate gets state 0 *)
Lemma bar: ...
Proof. (* pstate gets state 0 *)
Qed. (* summary set to state 1 *)
(* inject_non_pstate *)
Qed. (* summary set to state 1', not accounting for state 1 *)
EJGA: see inject_non_pstate
Some extra discussion about comTactic
, suitability of API for
multicore , incremental checking.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.