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

Fifth Coq Users and Developers Workshop, June 3rd - June 7th, 2019, Sophia-Antipolis (Nice, France)

This page collects useful infos for the participants to the 5th 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.

Location

The Workshop takes place at the Inria Sophia-Antipolis (how to reach the Inria center, accommodation infos).

Sponsors

This workshop is sponsored by Inria.

Program

The schedule will run from Monday afternoon (1pm) to Friday after lunch (~ 2pm). We will have lunch at the Inria cafeteria.

Gitter room

https://gitter.im/coq/CUDW2019

This is the preferred channel for public discussion with other participants and with the organizers. Feel also free to contact the organizers directly by e-mail.

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

  • Ahmed Alharbi (аkааlhаrьi ат рrоtоnmail)
  • Yves Bertot (Yves.Bertot at inria.fr)
  • Frédéric Besson ([email protected])
  • Lasse Blaauwbroek (lasse at blaauwbroek dot eu)
  • Simon Boulier ([email protected])
  • Cyril Cohen (cyril.cohen at inria.fr)
  • Frédéric Dabrowski (frederic.dabrowski at univ-orleans.fr)
  • Maxime Dénès (maxime.denes at inria.fr)
  • Jim Fehrle (jim.fehrle at gmail.com)
  • Yannick Forster ([email protected])
  • Gaëtan Gilbert ([email protected])
  • Hugo Herbelin (Hugo.Herbelin at inria.fr)
  • Karl Palmskog (palmskog at utexas.edu)
  • Pierre-Marie Pédrot ([email protected])
  • Talia Ringer ([email protected]) (staying at "Le Pré Catalan" in Antibes/Juan-les-Pins)
  • Kazuhiko Sakaguchi ([email protected])
  • Michael Soegtrop (michael dot soegtrop at intel.com)
  • Matthieu Sozeau (matthieu.sozeau at inria.fr) (staying at "Le Pré Catalan" in Antibes/Juan-les-Pins)
  • Claude Stolze (claude.stolze at inria.fr)
  • Sorin Stratulat ([email protected])
  • Enrico Tassi ([email protected])
  • Laurent Théry ([email protected])
  • Théo Zimmermann (theo at irif.fr)

Organizers

  • Maxime Dénès (maxime.denes at inria.fr)

If you need additional funding, please contact the organizers.

Proposed Projects and Ideas

  • @ejgallego: I'd like to a recreation of my current dev setup from scratch, and record it so it can be watched in Youtube. This setup includes a fully composed build, mu-repo, and some other goodies.

  • @ejgallego: I'd like to see a demo of Octobox and other ideas / tools people use in managing their Github/Gitlab workflows. @Zimmi48: I'd be happy to do such a demo.

  • @jfehrle: I'd like to investigate/discuss: 1) what it would take to get Coq to accurately report the series of tactics applied by auto or Ltac and 2) given a proof term, how difficult it would be to produce a list of tactics that generates the proof term. I think these could be useful both to beginners and experienced users and would make Coq tactics somewhat less of a black box. (Hugo, Théo)

  • @fajb: Zify (Maxime)

  • @sorinica: I would like to know the technical details that allow to integrate cyclic induction reasoning in Coq (Pierre-Marie, Matthieu)

  • @ppedrot: I am willing to work on https://github.com/coq/ceps/pull/40 (Enrico)

  • @mattam82: I'd like to reorganize the reference manual. (Théo, Jim)

  • @tlringer: I have a lot of Coq plugins that are not on the latest Coq version and are not in the CI. I would love to spend a day or two actually doing the work to get them all into the CI. (Enrico)

  • @LasseBlaauwroek: I would like to see about adding a number of plugin extension points into coq:

    • Letting plugins receive command line options
    • Hooking into the end of a batch compilation
    • Integrating with the internal version control system of coq
    • Hooking into the start end end of proof modes
    • Catching and modifying the execution of tactics
    • I would like to know how to register new datatypes that can be used for tactic arguments (this is already possible, I just don't know how).
    • Is is possible for a plugin to not need to be loaded?
    • Hook into the Require command
  • @tlringer: Can we please talk about good evar hygiene, even if briefly? I lack the basic understanding of that part of the API, and as a result I often end up ignoring universe inconsistency errors. I would like to figure out the best way to manage evar maps as I thread them throughout my code. I likewise don't understand the econstr interface and how to use it effectively; I just convert everything to constr (Yves)

  • @tlringer: I am also interested in developing versions of rewrite and simpl that are more powerful and offer more control. I have a lot of rewriting and refolding machinery in my plugins that can help with this. I can also work on consolidating some of the existing rewrite tactics so that there is less confusion (Hugo, Matthieu, Enrico)

  • @gares: problems with OPAM, user experience with nix (with @CyrilCohen). Wondering about having the opam-coq-archive automatically translated to nix, published and have instructions on using nix (Karl, Cyril, Théo, Maxime)

  • @SimonBoulier: rebase #9004 to have commands and attributes to have type-in-type, unsafe (co)fixpoints and non positive (co)inductives (Maxime, Gaëtan)

  • @SimonBoulier: print implicit arguments in curly braces {} (Hugo)

  • @SimonBoulier: look at extraction of native integers / string (with use in MetaCoq in mind) (Maxime)

Talks

  • @SimonBoulier: I can do a small talk about formalization of universes in MetaCoq (Tuesday 2pm)

  • @tlringer: I am also interested in proof optimization. I have some work in progress on this, and would love to complete it and run it on the standard library to find more efficient proofs. I would also love to talk to anyone who is interested in proof optimization (Wednesday 2pm)

  • @tlringer: I have a lot of completed work on automatically searching for and proving certain kinds of equivalences between types. If any of this is interesting, I am willing to contribute it back to Coq instead of keeping it in a plugin only, and I think that would be fun. I would also enjoy extending it to discover and prove new equivalences and relations between types that I do not currently support (Wednesday 2pm + ε)

  • @LasseBlaauwbroek: If people are interested I can give a demonstration of my Machine Learning system that tries to learn from user-written tactics (Thursday, 2pm)

Social Event

Wednesday afternoon, we’re gonna leave around 3pm to go to plage de la Garoupe in Antibes, from where we can start a tour of the peninsula:

https://randoxygene.departement06.fr/littoral/tour-du-cap-d-antibes-9360.html

We can take bus Line 1 followed by 2 to get there from Inria in about 45min-1 hour. This easy walk takes about 2 hours, with many potential stops to get refreshed in the sea, so bring swimming suits, water and sunscreen!

Dinner Monday

Meet at Place Général de Gaulle in Antibes at 20:30. Bus 1 & 100 from Sophia.

Debriefing

  • Matthieu: fix to univ not finalized, metacoq + extraction
  • Yannick: proving substitution for extraction (metacoq), port metacoq to 8.9
  • Cyril: OPAM -> Nix is possible, use mathcomp for metacoq proofs (extraction of ssrbool is broken)
  • Frederick: PR for coqpp empty rules, ongoing PR for apply t in H1, H2
  • Sorin: learnt stuff for circular induction, possible paths for implementing it
  • Yves: chat, experiments/bedugging with the windows installer
  • Claude: 2 PR on CoqIDE
  • Theo: chat + plan on improving refman
  • Gaetan: helped people, improve internal API
  • Simon: give talk about metacoq, type-in-type and unsafe fixpoint, printing implicit arguments surrounded by {}
  • Maxime: progress on two bugs (universes + evars), with Enrico and Pierre-Marie about parsing &ident for Ltac2
  • Kazuhiko: improve warnings about ambiguous coercion path
  • Karl: chat about OPAM repo, Nix, coq package index website, metacoq build stuff, mathcomp ecosystem, package coqhammer, extraction of data out of vio files with Enrico
  • Lasse: give talk about ltacrecord, ported ltacrecord to master, talk to people in order to remove most of modifications to Coq, and to improve the code
  • Enrico: random help, Elpi 1.3
  • Talia: give talk about pumpkin patch and devoid, PRs to improve plugin tutorial, learnt about state/sigma, chat with people about future projects
  • Pierre-Marie: talk, fixes at random, social engineering
  • Michael: chat with people, teaching Coq in the industrial context, CoqIDE on windows fixes
  • Jim: chat with people to get better Info auto also for ltac code in general, plan to encourage the move to typeclasses_eauto and have good Info for that one, plan to improve the doc, some work on mlg->refman