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 ([email protected])
- 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)
- 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. -
@fajb: I'd like to discuss what could be done to help debugging a failure of the CI. Currently, I find it very painful and time consuming. In my dreams, the CI would generate a minimal repro case which I could run on my local machine. Another dream would be to get the exact instant where the failing proof and a succeeding proof diverge.
-
@sorinica: I would like to know the technical details that allow to integrate cyclic induction reasoning in Coq.
-
@ppedrot: I am willing to work on https://github.com/coq/ceps/pull/40
-
@mattam82: I'd like to reorganize the reference manual.
-
@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.
-
@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.
-
@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.
-
@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.
-
@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.
-
@Zimmi48: will be happy to talk to people and give a hand on various projects (@fabj on CI, @mattam82 on the manual, @gares on Nix, @palmskog on automation for coq-community).
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
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.