Skip to content

Coq Users and Developers Workshop 2020

Jump to bottom Edit New page
Emilio Jesus Gallego Arias edited this page Apr 14, 2021 · 90 revisions

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
  • Wednesday
  • Thursday
  • Friday

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

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]
  • 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

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 like Info
  • 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 and of_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 of coqorg/coq:dev and coqorg/coq:8.13-alpha, triggered by a merge in coq@master and coq@v8.13.
  • 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 the coq-native package for each Coq in 8.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

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.

CC0

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.

Home

Installation of Coq

Documentation pages in this wiki

Events

Clone this wiki locally