Coq Users and Developers Workshop 2019
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.
The Workshop takes place at the Inria Sophia-Antipolis (how to reach the Inria center, accommodation infos).
This workshop is sponsored by Inria.
The schedule will run from Monday afternoon (1pm) to Friday after lunch (~ 2pm). We will have lunch at the Inria cafeteria.
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 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 (fbesson@inria.fr)
- Lasse Blaauwbroek (lasse at blaauwbroek dot eu)
- Simon Boulier (simon.boulier@inria.fr)
- 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 (forster@ps.uni-saarland.de)
- Gaëtan Gilbert (gaetan.gilbert@inria.fr)
- Hugo Herbelin (Hugo.Herbelin at inria.fr)
- Karl Palmskog (palmskog at utexas.edu)
- Pierre-Marie Pédrot (pierre-marie.pedrot@inria.fr)
- Talia Ringer (tringer@cs.washington.edu) (staying at "Le Pré Catalan" in Antibes/Juan-les-Pins)
- Kazuhiko Sakaguchi (sakaguchi@coins.tsukuba.ac.jp)
- 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 (sorin.stratulat@univ-lorraine.fr)
- Enrico Tassi (enrico.tassi@inria.fr)
- Laurent Théry (Laurent.Thery@inria.fr)
- Théo Zimmermann (theo at irif.fr)
- Maxime Dénès (maxime.denes at inria.fr)
If you need additional funding, please contact the organizers.
-
@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
autoor 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)
-
@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)
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!
Meet at Place Général de Gaulle in Antibes at 20:30. Bus 1 & 100 from Sophia.
- 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
&identfor 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 autoalso for ltac code in general, plan to encourage the move totypeclasses_eautoand have goodInfofor that one, plan to improve the doc, some work on mlg->refman
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.
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.