Rocq'n'share 2025 - rocq-prover/rocq GitHub Wiki

2025-06-27-rocq-n-share

The first Rocq'n'share meeting (previously known as Coq Users and Developers Workshop) will take place at Inria Paris from Tuesday June 24th to Friday the 27th.

Note, on Monday the 23rd there will be an independently organized workshop in honor of Georges Gonthier at Inria Paris.

Rocq'n'share is a meeting place for developers of The Rocq Prover and of its extensions: tactic languages, metaprogramming languages, libraries, plugins, verification frameworks, compilers, decision procedures...

The goal of the meeting is to disseminate knowledge on the implementation of Rocq and its extension frameworks, discuss design decisions, improve documentations (tutorials, how-tos, ...) and hack together on specific projects.

The program will be a mix of scientific/technical talks in the mornings and small group design/programming sessions in the afternoons.

Have a look at the schedule and join the Zulip channel for the latest news!

Summary

Registration

Registration is free but mandatory. To register, simply add your name to the list of participants at the end of this page to be able to enter the building during the workshop. You will be asked for your ID to enter the building.

Practical information

(Courtesy of the Iris workshop 2025 organizers)

Location: Inria Paris

The workshop will take place at Inria, 48 rue Barrault, Paris, France (directions; map).

We will use different rooms depending on each day:

Rooms

  • Tuesday: Emmy Noether (30p)
  • Wednesday/Thursday: Gilles Kahn (20p) + Sally Floyd (12p)
  • Friday: Anita Borg (38p).

We also have the Robin Milner room available for the week (19p)

Directions to Inria

  • From Charles de Gaulle airport (CDG) or from Gare du Nord, take RER line B (headed South) until Denfert-Rochereau or Cité Universitaire.

  • From Denfert-Rochereau, either walk 20 minutes to Inria (itinerary) or take metro line 6 (headed East, towards Nation) to Corvisart.

  • From Cité Universitaire, walk 12 minutes to Inria (itinerary). As you exit the station, immediately enter Parc Montsouris, and cross the park, walking North-East.

  • From Corvisart, walk 7 minutes to Inria (itinerary).

  • From Orly airport (ORY), take metro line 14 until Olympiades.

  • From Olympiades, take bus number 62 (headed West, towards Porte de Saint-Cloud) to Vergniaud. Once you exit the bus, turn the corner into rue Barrault (itinerary).

Traveling to Paris

Buy mainline train tickets from the French railway company, SNCF, from trainline, or through your usual travel agency. Or fly to Paris Charles de Gaulle airport (CDG) or Paris Orly airport (ORY).

Food

Lunches are not provided but there are many places around where you can find food near Inria

Links (click to expand)

  • Pastry, bread, and sandwiches:

    • Laurent Duchêne, a high-end pastry shop, is only 5 minutes away, and well worth a visit, if only to buy a great croissant au chocolat or chausson aux pommes.
    • Délice de Paris 13, 5 minutes away, is a typical boulangerie.
    • Lorette, 10 minutes away, has organic bread and good pastry.

  • Drinks:

    • Café Circus, 2 minutes away, is a typical Parisian café (coffee, tea, drinks).
    • La Folie en Tête, 3 minutes away, is a nearby bar (drinks).
    • Biérocratie, a beer cellar, sells a wide selection of beers (some chilled) (closed Monday).

  • Restaurants:

    • Café Circus, a typical Parisian bar, serves lunch and dinner and offers a good quality/price ratio.
    • Fabbrezza makes good pizza.
    • La Bonne Heure is a tiny vegan/vegetarian place (making a reservation is highly recommended).
    • Les Cailloux is an unsophisticated trattoria.
    • Chez Gladines and Auberge Etchegorry serve hefty French Sud-Ouest cuisine.
    • Lancetta is a true Italian place; somewhat high-end and expensive.
    • Chez Nathalie serves French cuisine; somewhat high-end and expensive.
    • Marso & Co serves French cuisine; leans on the chic and expensive side. Lunches will ha

Accommodation

Here are some suggestions for accommodation. The number of stars is the hotel's official rating and is also an indication of its price range. The hotel's distance to Inria is indicated in minutes on foot.

Links (click to expand)

The following hotels are closest to Inria Paris:

The following hotels are a bit further away:

Bed and breakfast:

Talk proposals

Add talk proposals here, they will be scheduled during the week (15, 30min or 1h slots)

  • A new, correct and complete algorithm for cumulativity checking with algebraic universes (Matthieu Sozeau) (30min).
  • 'Erased': a new sort for proof-relevant but computationally-irrelevant data (Johann Rosain, Matthieu Sozeau, Théo Winterhalter) (30min).
  • Toolkits for the Proof Toolkit (Emilio, 30-60 min)
  • Rocq state system explanation (summary, libobject, proof state, etc) (Gaëtan, IDK)
  • HConstr: context-aware hashconsing (Gaëtan, 30min or possibly less?)
  • Proposing a roadmap for the standard library (Cyril, remotely or in presence, 1h) http://cyrilcohen.fr/StdlibRoadmap2025.pdf
    • HB primer (Enrico Tassi, if there is interest among the participants)
  • Single step reduction for rewrite and debug convenience (Quentin Corradi).
  • Automatically generated goal names (Dario Halilovic) (30min)
  • Proof-engine performance potential (Andres Erbsen) (15min)
  • Software-engineering ideas for Rocq theories: stronger Opaque, reduction to first-order values, unification modulo projections and aliases (Andres Erbsen) (10min)
  • Waterproof: An educational tool built on top of Rocq (Pim Otte, Jim Portegies if scheduled Tuesday/Wednesday) (30min)

Project proposals

Add project proposals here, to be scheduled during the week. We'll gather small groups working on each of these at the beginning of the week.

  • Use proper identifiers rather than 0...100 for notation levels (Pierre Roux)

  • Ltac2:

    • port ring tactic from ltac1 to ltac2
    • write some (much need) docs for ltac2 at the same time (Thomas Lamiaux)
    • ...

  • Equations

    • port equations tactics from ltac1 to ltac2 (Thomas Lamiaux)
    • Making Equations more attractive to newcomers with an OCaml background (Yves)
    • Squash bugs in Equation's pattern matching compiler and improve some error messages (Mathis Bouverot)
    • Improve handling of with clause (probably needs ltac2)

  • Emilio:

    • Dune:
      • several minor items / bug triaging
      • (lang rocq ...) support
      • transitive package dependencies
      • rocq universe
    • coq-lsp:
      • multi-threading support
      • lazy proof checking
      • syntax coloring
      • completion
      • side panel
      • better search
      • vscode.dev
      • infoview work
      • newProfile visualization
      • goal display for tac1; tac2.
      • boxLayout
      • stabilization of memprof limits patches / interruption testing
      • several codeActions (insert goals at point)
    • petanque:
      • datasets
      • mcp support
      • LSP server / pytanque / async requests
    • jsCoq 2:
      • porting to Rocq 9.0
      • editor improvements
      • improve maintenance
    • General dev infra:
      • improvements to overlay system
      • improvements to CI setup

  • Migrate Nix Toolbox to flakes and to Rocq Prover organization. Write guides for the Rocq website. (Théo and Cyril)

  • Porting developments to the new algebraic universes + sort polymorphism + elimination constraints prelude (Matthieu).

  • Revive namespaces blueprint and make a prototype implementation (Enrico)

  • Devcontainers template in rocq-community (Enrico)

    • Docker images for the platform (atop the ones for the docker action)

  • Making math-comp maintenance less painful (Enrico)

  • LLM4Docq, a collaborative platform for semi-automated annotation of MathComp, with two goals:

    • A plugin to retrieve premises in natural language, both for mathcomp users and models (e.g. Crrrocq).
    • Train a model for auto-formalization (docstring + current source code -> formal statement), and for annotation (formal statement + current source code -> docstring).

  • MetaRocq:

    • Discussion/Fix universe level problems that arise when using MetaRocq as a metaprogramming language (see for example issue #1108).

  • Dump every lia query on the CI in smtlib format (Andres)

  • Waterproof:

    • Waterproof in the browser (connected with JsCoq projects)
    • Formalizing Infinite Descent exercises

  • Port and fix this code to Ocaml and Rocq to generate recursors for nestes inductive types

  • bikeshed syntax for abstract tactic block https://github.com/rocq-prover/rocq/pull/19023

Attendees (Mandatory to get in!)

  • Wassim Ait-Moussa
  • Abdelghani Alidra
  • Yves Bertot
  • Sylvain Borgogno
  • Mathis Bouverot-Dupuis
  • Ali Caglayan
  • Cyril Cohen
  • Pierre Corbineau
  • Quentin Corradi
  • Andres Erbsen
  • Thiago Felicissimo
  • Yannick Forster (Tuesday only)
  • Emilio J. Gallego Arias
  • Alain Girault (Thursday only)
  • Georges Gonthier
  • Basile Gros
  • Dario Halilovic
  • Jan-Oliver Kaiser
  • Kacper Korban
  • Ambroise Lafont (maybe)
  • Thomas Lamiaux
  • Assia Mahboubi (Tuesday only)
  • Kenji Maillard
  • Gregory Malecha
  • Niyousha Najmaei
  • Julien Narboux
  • Pim Otte
  • Pierre-Marie Pédrot
  • Clément Pit-Claudel
  • Jim Portegies
  • Pierre Rousselin
  • Pierre Roux
  • Matthieu Sozeau
  • Vojtěch Štěpančík
  • Théo Stoskopf
  • Nicolas Tabareau (Tuesday and Thursday)
  • Enrico Tassi
  • Romain Tetley
  • Tomas Vallejos
  • Quentin Vermande
  • Théo Winterhalter
  • Li-Yao Xia
  • Théo Zimmermann

Organizers

  • Matthieu Sozeau
  • Yannick Forster

To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.

CC0

By contributing to the Rocq 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.

⚠️ **GitHub.com Fallback** ⚠️