Coq Users and Developers Workshop 2023

Seventh Coq Users and Developers Workshop, June 26th - June 30th, 2023, Sophia-Antipolis (Nice, France)

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

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

Location

The Workshop takes place at the Inria Sophia-Antipolis. Travel and accommodation hints (page from another event organized in the same place).

Sponsors

This workshop is sponsored by Inria.

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).

Monday:

• round table (who/what/when)
• 3PM, Intro: reduction algorithms/machines overview (PMP)
• 4PM, Visio with Michael on the Rosetta stone project

Tuesday:

• 10:30 AM - Demo: completion in vscoq (ITU)
• 02:00 PM - Demo: coq-lsp (Emilio)

Wednesday:

• 10:30 AM - Demo: Getting started with Nix and Coq-toolbox (Theo)
• 5:18 PM - Excursion to the Juan Les Pins beach:
  • take the A bus at the stop in front of Inria, direction "Antibes les Pins", stop at "Regence" 40 minutes trip
  • walk to the beach (take a look at the "Time Out" fast food and "Instant Chapati", good options for a sandwich on the beach later) 7 minutes trip
  • Enjoy (If you need a ride back to Sophia, please tell me ASAP)

Thursday:

• 10:30 AM - Demo: Lean importer (Gaetan)

Friday:

• debriefing (room Euler Bleu) :
  • 09:50 - 10:00 - setup (sound, screen sharing....)
  • 10:00 - 10:10 - P. Roux - coercion hook
  • 10:10 - 10:20 - ITU - vscoq code completion
  • 10:20 - 10:30 - M. Sozeau - Certicoq / universes
  • 10:30 - 10:40 - A. Borges - Bug squashing
  • 10:40 - 10:50 - A. Seo - Autosubst porting & co
  • 10:50 - 11:00 - E. Gallego - Various
  • 11:00 - 11:10 - T. Porter/ T. Reichel - Search
  • 11:10 - 11:40 - ... the others ...
  • 11:40 - 12:10 - E. Crance, D. Fissore, Y. Foster, G. Gilbert, T. Ringer, K. Sakaguchi, M. Soegtrop, E. Tassi - Rosetta stone of meta programming languages

Projects for the week

• 4PM - Rosetta stone of extension languages for Coq

  • Enrico, Michael, Gaetan, Nicolas, Yannick, Enzo, Yves

• Autosubst on recent Coq version

  • Ana? , Audrey?

• Hook into the Coercion system

  • Pierre

• One step reduction for teaching and debugging

  • Ana

• Nix for Coq

  • Theo, Anton, Maxime, Matthieu, Yannick

• Coqbot

  • Theo

• Search command enhancement

  • Thomas P, Thomas R, Talia, Yves

• TC in elpi

  • Davide

• VScoq/LSP - solve pain points - completion

  • Hjalte, Simon, Jakob, Romain

• Efficient normalization

  • Talia

• GPT plugin for Coq

  • Talia

• Building dataset from Coq (serapi & co)

  • Talia

• Editor/compiler setup to hack Coq - start from the one in Coq's sources

  • Talia, Yannick

• Parallel compilation

  • Jim, Enrico

• Documentation / refman / syntax

  • Jim, Theo

Registration

Registration to this event is free but mandatory for organization purposes. To register you should simply add your name in the list of participants below.

Please include your e-mail address (in a human-readable form).

• Enrico Tassi (enrico.tassi at inria.fr)
• Théo Zimmermann (theo.zimmermann at telecom-paris.fr)
• Jim Fehrle (com gmail at fehrle jim)
• Matthieu Sozeau (matthieu.sozeau at inria.fr)
• Talia Ringer (tringer at illinois.edu)
• Gaëtan Gilbert (gaetan.gilbert@inria.fr)
• Yannick Forster (yannick.forster at inria.fr)
• Ana Borges (ana.agvb at gmail)
• Anton Podkopaev (anton.podkopaev at jetbrains.com)
• Yves Bertot (Yves.Bertot at inria)
• Christopher Mary admin@anthroplogic.onmicrosoft.com
• Audrey Seo (alseo at cs.washington.edu)
• Chris Lam (lam30 at illinois.edu)
• Pierre Roux (pierre.roux at onera.fr)
• Maxime Dénès (maxime.denes at inria.fr)
• Pierre-Marie Pédrot (pierre-marie.pedrot at inria.fr)
• Andrei Kozyrev (andrei.kozyrev at jetbrains.com)
• Nicolas Tabareau (nicolas.tabareau at inria.fr, only Mon-Wed)
• Enzo Crance (enzo.crance at inria.fr, Mon–Thu)
• Romain Tetley (romain.tetley at inria.fr)
• Thomas Reichel (reichel3 at illinois.edu)
• Thomas Portet (thomas.portet at inria.fr)
• Semen Panenkov (semen.panenkov at jetbrains.com)
• Davide Fissore (davide.fissore at inria.fr)
• Simon Green Kristensen (sigk at itu.dk)
• Hjalte Sorgenfrei Mac Dalland (hjda at itu.dk)
• Jakob Israelsen (jais at itu.dk)
• Hugo Herbelin (hugo.herbelin at inria.fr)
• Emilio J. Gallego Arias (e (at) x80 . org)
• Paolo Torrini (paolo.torrini at inria.fr)
• Michael Soegtrop (msoegtrop at apple.com)

Organizers

• Enrico Tassi

Proposed Projects and Ideas

If you already have a project in mind, share it here (briefly)

• Coq modulo rewriting rules github.com/yannl35133/coq
• Any of these projects, depending on interest (Talia):
  • Efficient normalization, possibly by way of learning to optimally normalize
  • Coq ChatGPT or GPT-4 plugin
  • Search engines and databases for formal proofs; better Search functionality
  • Lemmas and automation for hset-preserving containers
  • Better infrastructure for Coq datasets
  • Help porting proof repair plugins to latest Coq and getting them in CI
  • Help using Ltac2
• Examples of plugins in various Coq metaprogramming languages (Louise)
• "Coercion" hook to enable programming "coercions" in coq-elpi for instance (Enrico, Cyril, Pierre)
• Working on generalized universe constraints and universe polymorphism (Matthieu, Pierre-Marie)
• Autosubst-Ocaml for Coq 8.17 (Yannick) -- a good first project to practice writing OCaml code interfacing with the Coq kernel
• Discussion on Nix for Coq
• Emilio's ideas:
  • Build related (Dune / Coq Universe):
    • Improve overlay tooling to understand "package locks"
    • Coq Universe: tooling for package lock / universe branches
    • Coq Universe: experiments on fast-ci
    • Have dune record package meta-data when installing Coq theories
  • jsCoq: work on ProseMirror (advanced editor) integration
  • Coq:
    • incrementality for opaque proofs
    • infrastructure for async vernaculars
    • vo file reification
  • coq-lsp:
    • Improved goal rendering / Goal UI
    • Improved Windows support
    • Flèche Command line extensible compiler (lots of possibilities here)
    • Document-level plugins
    • Improved hover and linting setup
    • Improved statistics
    • Improved whole-project support (including panel view)
    • Web extension / jsCoq
    • Improved markdown editing / advanced editors
    • Literate LaTeX support
    • Integration with Hammers / STMCoq
    • Debugger
    • General documentation improvements

Debriefing

To be filled in during the last day