Coq Call 2022 02 23

• February 23, 2022, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• CEP 62
• #15714 Make processed part of script read only when Coq is busy (Jim)
• Plans for next months (HH)

Notes

• CEP 62

  Intro:

  • interface files serve also as a way to de-functorialize your development since only one implementation of each module is typically needed
  • at the same time they make a development agnostic on the implementation, e.g. the target architecture and some compiler passes
  • separation impl from api ease reading (proper tooling would also solve this)

  Technical problems:

  • universes:

    • the CEP authors have use cases which are not very universe polymorphic, write universe constraints by hand in the interfaces may be feasible. Having them not fully checked (a la .vio) is also OK, a full check on CI at night would suffice. Ali reports it did not work well in HoTT, but they are on the opposite side of the spectrum w.r.t. universe polymorphism
    • with an interface the non-determinism one gets by async checking of proofs is less severe, since the value of public stuff is fixed in the interface

  • Require:

    • need for more fine grained ways of requiring a file:
      • only the interface
      • interface + implem, to please extraction but also fully check universes

  • Leakage:

    • a leaking effect (eg hint) from a Require in the implem should not leak to the interface

  • Print Assumptions:

    • needs to understand interfaces and print it depend on X not on X.foo X.bar ... (too verbose)

  • Effort:

    • interface files seem implementable, #[public] is hard
    • separate interface file seems a lot of copy&paste but there is another CEP helping
    • if we go now for separate files, nothing prevents in the future to have attributes which help generating the interface (even if at that point nobody would find worth it to add that feature)

  • Next:

    • Another call on the topic, a specific WG, Enrico sends a doodle on Zulip

• #15714 Make processed part of script read only when Coq is busy (Jim)

  • editing the green area does not work if Coq is busy (not a regression)
  • proposes: checked/being-processed code read only while Coq is busy
  • non-locking is nicer for UIs, but it is not a change that can go into a hotfix (needs to change the protocol)
  • maybe allow editing comments anyway (even when Coq is busy, the lexer tags comments so the new boolean condition could check for it, but locs would be shifted)
  • Ali: the PR fixes most issue, maybe not the initial one by MS / Jim: it should
    • Discussion/testing continues on Zulip

• Plans for next months (HH)

Postponed to next week