Main problem: keeping per-plugin and per-tactic state in the summary.

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 the evar_map with the custom state.
• Add a field to proof_object to keep the custom state at end of proof.
• update close_proofand close_delayed_proof to put the state in the new field.
• update save and save_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.