BreakOut 2020 12 01 envs

Link to Gaëtan's notes

present: Gaëtan, Emilio, Enrico, PMP

We discussed how kernel environments are handled in interactive proofs.

Let st denote states, containing the global env, then we have this situation:

:st0
Lemma foo : T.
by tac1; abstract tac2
:stP
{Qed,Defined}
:st1

• 1st question: how are the situations on Defined / Qed different?

  • Qed:

    • in stP: run close_proof

    • in st0 declare / Qed the constant side effects get inlined

      Extra Q: what happens with universe declarations, are they handled correctly by inlining?

  • Defined:

    • in stP: run close_proof

    • still in stP: declare / Qed side effects are still in the env

      is it still necessary to call export_private_constants in this case?

      • the the STM calls Proof.save with st0 instead of stP, so in this case yes
      • we could drop that requirement, however PMP notes that spurious constants registered during backtracing would arise
      • Note that the STM replays imperative vernacs over st0, which is an issue

• 2nd question: is it feasible to get rid of sideff inlining? GG: need private constants (sub constants?)

• 3 ideas:

  • move the st handling logic to declare, if still using st0 for Defined, that would require exporting the effects, and handling nested proofs. Seems tricky but still better than having the client do it.
  • remove side-effect replay and use stP? Doable.
  • handling Defined as Qed? Could lead to issues due inlining / increase checking time. PMP makes a point about transparent abstract

Next discussion was about Safe_typing.push_private_constants, whose use in refine.ml adds loads of duplicated side-effects. PR to assess CI impact submitted https://github.com/coq/coq/pull/13536, discussion still ongoing. Only impacts Rewriter, likely due to wrong tactic code?