jsCoq and CoqDB Working Day
- 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 (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.
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.
(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.
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.
- Hanneli T. (co-organizer)
- Emilio J. Gallego Arias (co-organizer)
- Lasse Blaauwbroek (interested in participating in the "CoqDB" discussion)
- Laurent Théry
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.