Coq Call 2020 05 20

• May 20th 2020, 4pm-5pm Paris Time
• The link to the visio room will be provided on Zulip the day of the call: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Coq.20Call
• Add your topics below

Topics

• 8.12 update after branching
• #11170: Memory corruption in VM
• Brief update about UI work (Emilio, if Hugo can attend)
• Update about ongoing declare / proof handling work (Emilio)
  • hooks / chaining is an issue
  • extra needs noted by Pierre-Marie ?
  • vio path / restrict / universes ?

Notes (from Matthieu)

8.12 update after branching

Branched on monday. Release notes in preparation. Not much to wait for for the beta.

Reminder we have a critical bug: #11170: Memory corruption in VM. We should ask Pierre Roux, Benjamin Grégoire or Xavier Leroy if he would have the expertise to fix it, other members of the development team are not feeling competent to do so.

Brief update about UI work (Emilio, if Hugo can attend)

Emilio presents some timeline:

=> pre-2012: REPL

=> 2012-now:

• STM [from paralITP]

=> 2014-now:

• jsCoq [Gallego, Itzhaky, Jouvelot, Pin]
• [protocol is different from the XML, based on a tweaked STM OCaml-API]
• SerAPI exposes basically the same these days
• Protocol designed with help of cpitclaudel

=> 2014-abandoned

• pg-xml [Steckler, ?]
• protocol has a lot of state => client suffers requires lots of sync

=> 2014-now:

• vsCoq [Siegbell]
• currently maintained by Dénès

=> 2015-now:

• SerAPI [Gallego, Palmskog, Pit-Claudel, others...]
• lost focus as a UI server

=> 2016-now:

• LSP prototype for Dedukti/lambdapi [Blanqui, Gallego, others]

=> 2018-now:

• Isabelle-"LSP" [Wenzel]

=> 2019:

• Coq-LSP prototype [Gallego, Laporte]

=> 2020:

• document manager ? [Dénès, Tassi]

2019 Plans [after first coq-lsp prototype]

Work on server still not possible:

1. rework handling of proofs

• ~80% done [Gallego, Gilbert, Pédrot] [Proofs GH project]

• obligations close to regular path

• still some issues: vio mode and universes

• question by Enrico: what are the goals? => remove internal low-level structures => enforce large amount of invariants statically => large removal of duplicate code, better API [no need for callers to worry about universes, etc...] => fixing some problems (bugs) with side-effects => removing inversion of control => single API for constant declaration with holes => issues with declaration of mutual entries

API now is:

val declare_definition
  :  name:Id.t
  -> info:CInfo.t
  -> types:EConstr.t option
  -> body:EConstr.t
  -> Evd.evar_map
  -> GlobRef.t

where CInfo.t contains locality, hook, kind, implicits, etc...

2. rework handling of state [emilio's focus for 8.13]

• ~20% done [Dénès, Gallego, Gilbert, Herbelin, Pédrot]

• handling of enviroments

• notation state

• a bit more on parsing state

"Global.env () / universes => this will allow to have a better api for opaque proofs

"the API the document needs would benefit from reflecting more invariants"

• global is moving to vernac

3. "just an idea" let's think about it [once the API is a bit more functional] incremental checking

• waiting on 1 & 2
• inspired by Dune model
• quite a few questions open

deps --[action]--> targets

- [env | proofview | universes] --[check_proof]--> finished proof

trace_of_env : env -> Trace.t

Proof.
| apply: foo => {u1 : uctx}
| apply: bar => {u2 : uctx}
Qed. ->{targets} (u : UState.t * p : Proof.t * Summary.t)

u1 ≈ u2

-{deps}(u,p)->
Lemma tooo : foo.
Proof.
Qed.

4. cross-prover efforts:

• discussions mainly with Makarius about LSP, at some point we should find a common ground [possibly with Lean]

2020 Status

• Work on 2 above: prioritary, essential.

• with OCaml multicore team: Coq + Multicore

• Diego Diverio: INRIA Saclay Engineer for LSP

  • common infra for "Tocatta, Dedukteam, Partout", to be used by "coq-lsp" / "ocaml-lsp" why3 mode just released "gitlab.inria/why3"
  • also an intern will work on that

• Once 2 is to a reasonable point:

  • incremental checking prototype [based on Dune's lang]
  • LSP: thin layer on top of it

Other topics:

• notations
• searchs

Discussion LSP commentary, Hugo's questions:

• LSP, what does it solve:

  • core communication protocol
  • nice extra goodies [completion, etc,...]
  • maintenance quite a bit easier
  • easy to implement [first prototype done in an afternoon]

• LSP, what it does not solve:

  • architectural problems in Coq
  • architectural problems in OCaml
  • "large-scale & industrial user needs"

• Overall, LSP is convenient over a custom protocol, but not solving all the problem to type check proof documents interactively.

"Emilio => working on state of Coq"

• Quick review of Hugo's questions: https://github.com/coq/coq/pull/12337#issuecomment-629766568

  • Not using serAPI for ui protocols

  • LSP-Coq a failed experiment?

  • pg-xml revival project by Erik Martin Dorel?

  Much work needed on cleaning up the APIs w.r.t. global state handling.

More Discussion

• Emilio's take away => many tries , none of them still "works for me"
• Problems identified:
  • Maintenance of protocol =[fix]=> use LSP
• Current design of Coq's API has bad impedance =[fix]=> rework of API, deprecation of STM