Coq Users and Developers Workshop 2020 - coq/coq GitHub Wiki
Sixth Coq Users and Developers Workshop
This page collects useful info for the participants to the 6th Coq Users and Developers Workshop.
The Coq Users and Developers Workshop is an event that brings together the core developers of Coq and people interested in understanding, improving or extending the system.
Date
The CUDW 2020 is taking place from 2020/11/30 to 2020/12/04.
It was originally going to take place from 2020/06/22 to 2020/06/26, but was postponed due to the ongoing COVID epidemic.
Location
The CUDW 2020 is hold remotely, with a BBB visio room and a Zulip chat stream.
Sponsors
This workshop is sponsored by Inria.
Program
Official Schedule is 10:00-17:00 UTC+1, but nothing prevents you from sticking around on the Zulip outside these timeslots. The BBB room is also always available, but breakout rooms may end if everybody leaves BBB for several minutes.
Plenary Sessions (15:30-16:30 UTC+1):
- Monday
- 15:30-16:15: Coq Internals and Development Setup (Emilio J. Gallego Arias)
- (UNOFFICIAL:) Jason Gross PhD defense at 17:00. A link will be provided on the Zulip.
- Tuesday
- 15:30-15:50: A tour of MetaCoq (Matthieu Sozeau) recorded video
- 15:50-16:10: Coq platform (Michael Soegtrop) recorded video
- Wednesday
- 15:30-15:45: Towards better Coq batch incremental proving (Karl Palmskog) recorded video
- 16:00-16:20: Coq-Elpi in a nutshell (Enrico Tassi) recorded video
- Thursday
- 15:30-15:40: Demonstration of Roosterize, a tool for suggesting Coq lemma names using deep learning (Karl Palmskog) recorded video
- 15:40-15:55: Demo of Tactician, a tactic machine learning plugin (Lasse Blaauwbroek) recorded video
- Friday
- 15:30-15:50: Using Alectryon for Coq's reference manual (Clément Pit-Claudel) recorded video
Recap: 16:30-17:00
Every day, people will summarize what they did that day.
Zulip room
The CUDW 2020 has a dedicated Zulip stream.
https://coq.zulipchat.com/#narrow/stream/255971-CUDW-2020
This is the preferred channel for public discussion with other participants and with the organizers. It is recommended to subscribe to it in order not to miss any notifications about the CUDW. Feel also free to contact the organizers directly by e-mail.
Registration
Registration to this event is free but should be done for organization purposes. To register you should simply insert your name in the list of participants below, ideally alphabetically.
List of participants
- Reynald Affeldt
- Lasse Blaauwbroek (@LasseBlaauwbroek @Lasse)
- Yves Bertot (@ybertot)
- Ana de Almeida Borges
- Cyril Cohen (@CohenCyril)
- Maxime Dénès
- Jim Fehrle (@jfehrle)
- Emilio Jesús Gallego Arias (@ejgallego)
- Paolo Giarrusso (@Blaisorblade)
- Gaëtan Gilbert
- Jason Gross (@JasonGross)
- Samuel Gruetter (@samuelgruetter)
- Alexander Gryzlov
- Hugo Herbelin
- Marie Kerjean
- Fabian Kunze
- Assia Mahboubi
- Kenji Maillard
- Erik Martin-Dorel (@erikmd)
- Guillaume Melquiond
- Karl Palmskog
- Zoe Paraskevopoulou
- Pierre-Marie Pédrot
- Pierre Pomeret-Coquot
- Clément Pit-Claudel (@cpitclaudel)
- Pierre Roux (@proux01)
- Michael Soegtrop (@MSoegtropIMC)
- Matthieu Sozeau (@mattam82)
- Enrico Tassi
- Anton Trunov (@anton-trunov)
- Pierre Vial
- Théo Zimmermann (@Zimmi48)
- Arthur Azevedo de Amorim
- Andrej Dudenhefner
Organizers
- Pierre-Marie Pédrot
Proposed Projects and Ideas
Emilio J. Gallego Arias
Talks
-
Coq's Internals: I'd like to a recreation of my current dev setup and Coq's main architectural components, and record it.
-
Coq + Dune presentation?
Open discussion
-
Best practices for OCaml in 2020 / OCaml community survey
-
Dealing with backward-incompatible changes (see https://github.com/coq/coq/issues/13532)
Architectural and Internal Projects / Discussion
- Invariants w.r.t. Global.env on
Declare.Proof.save
are not clear and indeed the API doesn't enforce correct usage from the callers - Porting Coq to OCaml multicore [already done, but structural issues to be discussed]
- global heap may be an issue https://github.com/coq/coq/pull/12629
- Consolidation of the Grammar extensions, in particular removing duplications between gramlib and Coq, and integrating generic arguments into Gramlib.
- Further refactorings of the vernacular data type, including:
- a distinguished type for tactics
- separation of meta-commands [relative to the documents] vs regular vernaculars
- refactoring of the loadpath / init libraries
- general interface for interpretable objects?
Build system and Tooling Projects / Discussion
- [dune] composition of public Coq libraries
- [dune] add
dune coqtop
shell wrapper - Automated workflow for overlays
- [dune] Replacement of ML makefiles with wrapped dune calls
- [plugins] use findlib to load plugins
- migration windows CI to github actions
- finish coqnative integration
- .coq-pkg implementation
- per-file catapult information
- [dune] coqdoc support
- [dune] ocamldebug support
- general dune hacking is also welcome
- [dune] support %{coq:version}
- [dune] use dune-buildinfo lib
- [dune] port test-suite to dune
UI Projects
- adding https://github.com/janestreet/patdiff support [as a vendored library]
SerAPI
- For aleyctron: attach qualified names dumpglob information to ast nodes
- For Vicent: support for internalization of vernaculars AST
- [general] multiple format output
- [general] refactor common init code, push upstream
JsCoq
- many little projects can be done.
Requests
- I'd like to see a demo of Octobox and other ideas / tools people use in managing their Github/Gitlab workflows.
Enrico
- finish make -> dune transition
- [Emilio] I was thinking of doing "working groups" like 2/3 hours, this could go inside the Dune working group.
Matthieu
- Settling down the design of inductive-inductive types and writing a CEP for it
- Discussing ways to integrate the MetaCoq+CertiCoq compiler pipeline into the kernel as an alternative conversion and as a tactic for reduction (provides certified compilation of closed terms of inductive type).
Jason
- Maybe dusting off my branch that adds a
Debug
vernacular likeInfo
- Maybe look into adding profiling to Ltac2
Zoe
- CertiCoq support for primitive objects.
Clément
Jim
I plan to be asleep through most of the workshop, but I'd be interested in a discussion about Coq Goals/Top 10 Improvements to Coq, as well as a discussion of how we can better serve the Coq community. But the sessions would have to be at 4 PM (or preferably later) for me to participate.
Cyril
Rework nix setup for Coq, coq-community projects and mathcomp projects (at least).
Ana Borges
Add support for primitive signed integers.
- Monday: A work group was formed. We decided to expose signed comparison operations and signed division in the kernel (and then use this to write libraries about them). We have a preliminary version of the signed comparison functions.
- Tuesday: Exploration of the 32 bit implementation of the comparison operations and division; printing and parsing signed primitive ints.
- Wednesday: Attempt at printing and parsing signed primitive ints, but it was not very successful.
- Thursday: Printing and parsing done. Draft PR: #13559
- Friday: Signed division and remainder, extraction,
to_Z
andof_Z
.
Coq Platform
- Installers for Mac and Windows
- I hope I find a lot of testers and can fix issues they find
- Make the official release for Coq 8.12.1
Lasse
- Gather feedback on Tactician (after a beta is out either on Monday or Tuesday)
- Have a conversation about removing Tactician's biggest hack (involving the STM / vernacular)
- Have a conversation about the potentially rather sensitive topic of gathering user statistics.
- Add Tactician to the Coq CI
Nicolas
- Talk about the introduction of rewrite rules in Coq (https://github.com/coq/ceps/pull/50) Maybe a short presentation Thursday morning followed by a working/discussion group.
Erik
- Extend docker-keeper to support "keywords triggers": replacing the previous nightly build of the
coqorg/coq:dev
Docker image with automatic rebuild ofcoqorg/coq:dev
andcoqorg/coq:8.13-alpha
, triggered by a merge incoq@master
and[email protected]
. - Still pending: a similar evolution to replace the nightly build of
mathcomp/mathcomp:coq-dev
. - Discussion with Théo then Karl about the upcoming changes for
docker-coq
images: only single-switch images, and the addition of thecoq-native
package for each Coq in8.5 ≤ _ < 8.13
. - Discussion with Karl about a proof-of-concept that allows one to use
coq-community/docker-coq-action@v1
to build (quasi)monorepos, containing several.opam
files that may depend each other. So, no extension of docker-coq-action is needed to implement this use case.
Talk Proposals
- Jim requested a talk on the Coq platform goals and status - i will be happy to give one if others share this interest (Jim: my original suggestion was for a discussion about goals--thinking that our goals are implicit rather than explicit and that it's worth considering them holistically. Also that I'd like to know what others think are the most valuable goals.)
- Clément: I could give a brief demo about porting Coq's reference manual to Alectryon and we could discuss whether we want to do that and whether that requires a new Alectryon backend that uses Coq's XML API or whether there are plans to integrate SerAPI into Coq.
- Clément: Alternatively, I could give a live-code demo of Alectryon.
- [Lasse]: If there is interest I can give a short demo of Tactician. I am not available Tuesday afternoon.
Social Event
We will be sharing a drink remotely on Thursday, 3rd of December after the CUDW (around 17:00 UTC+1).
Discussions summaries / notes
- Breakout 2020/11/30 11:00 am on Tactician and Coq's API integration
- Breakout 2020/12/01 11:00 am on Dune + Linter API for document servers
- Breakout 2020/12/01 13:00 pm on low level proof and constant internals
- Breakout 2020/12/03 10:00 pm on silent Coq builds
- Breakout 2020/12/03 13:00 pm on build system problematics
- Breakout 2020/12/03 2pm on MetaCoq