Coq Users and Developers Workshop 2024 - coq/coq GitHub Wiki

Eigth Coq Users and Developers Workshop, July 1st - July 5th, 2024, Nantes Université (Nantes, France)

This page collects useful info for the participants in the 8th 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.

All Coq related projects are welcome.

More information can be found on the wiki or asked on the Zulip channel: https://coq.zulipchat.com/#narrow/stream/433315-CUDW-2024

The event will be in person only, no remote attending.

We want the event to be safe to attend. We will enforce the Coq code of conduct

IMPORTANT: The CUDW is free, but for organization purposes please register yourself in alphabetical order in the list below, with intended arrival and departure dates.

Location

The Workshop takes place at the LS2N in Nantes, from Monday July, 1st to Friday, July 5th. Travel and accommodation hints here or here (pages from other events organized in the same place).

A map showing the precise location of the LS2N building can be found here.

The meeting will take place in building 34, room ABC (ground floor) on Monday, Tuesday and Friday. On Wednesday and Thursday, it will be moved to building 11, room 3 (ground floor). Getting to room ABC is easy, people from inside can see you outside. Room 11-3 is harder to reach, try to follow an organizer and remind them to show you the room the days before. If you are stuck outside, do not hesitate to ping people on the Zulip channel.

Social Event

There will be a social event on Tuesday night. Meet at "Les Filles du Marronnier" at 19:00 (3 Boulevard Gabriel Lauriol, Nantes).

Program

The schedule will run from Monday afternoon (1pm) to Friday after lunch (~ 2pm). The room is available the entire week (arriving early/leaving late is possible), from 9am to 6pm.

Organization

For any question please contact Pierre-Marie Pédrot by e-mail or (faster) on the Coq Zulip.

Registered participants

IMPORTANT: The CUDW is free, but for organization purposes please register yourself in alphabetical order in the list below, with intended arrival and departure dates.

  • Gaëtan Gilbert (full week)
  • Hugo Herbelin (full week, from Monday end of afternoon)
  • Janno [Jan-Oliver Kaiser] (full week)
  • Christopher Lam (Tuesday-Friday)
  • Thomas Lamiaux (full week)
  • Yann Leray (full week)
  • Assia Mahboubi (full week)
  • Kenji Maillard (full week)
  • Mara Malewski (full week)
  • Pierre-Marie Pédrot (full week)
  • Josselin Poiret (Tuesday-Friday)
  • Pierre Rousselin (Wednesday afternoon-Friday)
  • Pierre Roux (full week)
  • Matthieu Sozeau (full week)
  • Nicolas Tabareau (full week)
  • Éric Tanter (Mon-Tue)
  • Enrico Tassi (full week)
  • Kazuhiko Sakaguchi (full week)
  • Tomas Vallejos (full week)
  • Théo Zimmermann (Tuesday afternoon-Friday)

Talks

  • Thursday 10:30: Presentation of various universe / sort polymorphism mechanisms and what remains to be done (Matthieu and Nicolas)
  • Tactics: move
  • Tactics: Ltac/Vanilla tactics vs Ssr tactics (Pierre Roux, Assia, Thomas, probably thursday)
  • Forward reasoning in ssr (Assia)
  • Status of work on unifying Definition, Theorem, Fixpoint, CoFixpoint, Derive, and more (CEP #42, Hugo)

Discussions

  • 14h - 15h30 Move on from Vanilla rewrite to SSReflect rewrite (Thomas)

  • 15h45 - 17h00 Vanilla vs Ssreflect of what is basic and common, pros and cons

    If ever the time is ripe for instilling a new dynamics on tactics, here is a technical document written in 2017 which goes in the direction of providing the best of two worlds.

Topics

If there is a specific topic you would like to work on, or discuss about with the core devs, we recommend that you write it down here as well. This will allow to elaborate a schedule so that people can work in parallel groups, and synchronize regularly.

  • (Janno) Primitive projections, specifically removing compatibility constants. It seems like we cannot get the behavior of the kernel right as long as they still exist (https://github.com/coq/coq/issues/18977)
  • (Janno) Reviving https://github.com/coq/coq/pull/17839 with new Constr constructors instead of (ab)using primitives
  • (Thomas Lamiaux) Platform docs Writing Tutorials and How (Ltac2, etc...)
  • (Thomas Lamiaux) A better set of tactics for Coq: Reuse some part of SSReflect ?
  • (Thomas, Pierre, Théo) Discuss the Cep about documentation, in partcular its integration with Coq (CI, etc...)
  • (Nicolas, Matthieu) implementation of a sort and universe polymorphic standard library (branch here)
  • (Théo) Finalizing the migration to GitHub Projects v2 for release management (deciding what features are missing, what could be done differently).
  • (Hugo) Design decisions around CEP #42: syntax of sealed attribute, default opacity for Theorem :=, a language of attributes/annotations to tell whether unresolved evars are turned into goals, turned into obligations, resolved by the obligation tactic, resolved by the typeclass mechanism, resolved by an ad hoc tactic.
  • (Enrico) "Blog" post on how to add a quickfix to Coq
  • (Enrico) understand how to "bind" ssreflect to Ltac2