jsCoq + CoqDB Working Day

Participation Instructions

• When: Thursday, March 31st, 14h00 Paris time (08h00 NYC time - 05h00 Seattle time)
• Where: Online on Zoom

Please:

• add your name to the list of participants below.
• feel free to edit / suggest topics below

Schedule

Schedule (Paris time):

• 14h00 - 15h20: CoqDB discussion
  • 30 mins: Emilio will lead a presentation on current state, uses cases, existing tools...
  • 25 mins: Collective discussion (introduce your use cases and ideas)
  • 25 mins: Breakout sessions, if needed.
• 15h20 - 15h40: Break
• 15h40 - 16h00: jsCoq, introduction (led by Shachar and Emilio)
  • state of the project , see also https://github.com/jscoq/jscoq/issues/261
  • top priorities / issues / roadmap; among those
    • storage backend
    • build / toolchain / addons setup
    • hybrid editing
    • generating jsCoq pages?
    • proof exploration
  • discussion, move to breakout rooms
• 16h00 - 16h50: Breakout groups
• 16h50 - 17h00: Break
• 17h00 - 18h00: Roadmap discussion, follow up, wrapping up.

CoqDB Topics

Gathering / DB of Coq objects: There are several pieces of code that scan the list of objects defined in .v files, for example coq-dpdgraph, coq-serapi, Alectryon, coqdoc, bug-minimizer/finder etc... We hope to discuss about a common implementation.

jsCoq Topics

jsCoq General discussion

(Pulled from https://github.com/coq/coq/wiki/CoqWG-2022-02#jscoq-session)

• integrate the waCoq backend in the main branch

• integrate coq-layout-engine

• finish dune build rules

• From Evariste G:

  • "Hack" on the possibility of spawning multiple workers (adjusting the views to a completely different use of the UI)
  • redesign of some UI elements
  • better docs
  • add some features from interesting plugins to jscoq (i.e. hover over and see docs)
  • brainstorm other ideas if there is time.

Landing Page

Refactor the jsCoq landing page.

Some thoughts (Hanneli):

Who is going to see this landing page?

• If you are visiting the page and you never used Coq, how can you make a distinction between what is good and bad style? (Isn't it subjective too? This is a hard question...)
• If you are a total beginner, you probably wan to get a general sense of what you can do with Coq
• If you are an exp. user who needs a quick space to try out some proofs, you might have your own standards.

Participants

• Hanneli T. (co-organizer)
• Emilio J. Gallego Arias (co-organizer)
• Lasse Blaauwbroek (interested in participating in the "CoqDB" discussion)
• Laurent Théry