Skip to content

Call 03 04 2023

Jump to bottom
Emilio Jesús Gallego Arias edited this page Apr 3, 2023 · 5 revisions

When and Where

Notes

  • general roundtable: Bhakti, Tomas, and Emilio did a brief introduction of their background and work ; Emilio notes the CoREACT project going on at IRIF that deals with diagrammatic reasoning.

  • Bhakti asked about general Coq UI roadmap, Emilio did point out the upcoming UI meeting coordinated by Benjamin, explained a bit the history of the project and pointed out to coq-lsp FAQ's

  • We discussed a bit the role of experimentation in HCI research, and highlighted coq-lsp approach

    • In particular Emilio remarked that breaking stuff is very welcome!

  • backwards compatibility + older versions on opam?

    We discussed a bit the way coq-lsp handles versions, indeed it is not very clear. As of today we do:

    • patches land on main, Emilio explain this is often convenient due to Coq patches still neccesary for coq-lsp features
    • we maintain a branch for Coq versions v8.15-v8.17 , at release time, we git merge from main to 8.17, then to 8.16, etc...
    • we do tag all the corresponding versions, and do releases for the versions that can go to opam
    • as an example we did upload to opam the 0.1.6 release for Coq 8.17, using dune-release
    • we agree the whole setup is confusing and we should improve the docs and process as much as we can
    • Bhakti highlights that they've been working on Coq 8.16, so it makes sense for them to submit patches to that branch and for us to forward port

  • support for "stepping through" proofs

    • Bhakti is interested in recovering a bit of navigational help from the usual "step thru a proof" UI experience
    • Using a regex sounds like a fine approach to determine the end of the sentence.
    • Emilio points out that a call to get sentence info could be used too, Bhakti was interested in implementing it. A good start would be to take the proof/goals request and strip all that is not needed
    • In general, Emilio thinks this kind of user cases do belong to "document exploration" capabilities, Emilio encourages to think out of the box and to try all kind of visual aids, etc....
    • A bit of discussion on how document evaluation strategies do work was also had.
    • We also note that PG behavior can implemented very easily on top of LSP, just send the prefix you have highlighted

  • roadmap update: Emilio points out he's mostly focused on full-project integration for the next releases.

  • next meeting when we want to, for now scheduled to 24 tentatively.

Clone this wiki locally