CoqWG 2022 02 - coq/coq GitHub Wiki

Coq Hackathon and Working Group, Winter 2022

  • When: 15-17th February 2022
  • Where: Online
  • What: A meeting for people interested in hacking the Coq system, at all expertise levels

Participation and registration

To register, please add your name and any other relevant information [such as days you are attending] in the "Participants" section below.

The Hackathon will take place online, using Coq's Zulip Join our Zulip!

We will use BigBlueButton for the video conferencing system; we have two rooms, a core room, where breakout sessions will happen, and a dedicated room for the Bug Squashing party, find the links below:

To change the language of the interface click on setting on the right top corner!

We will record some of the sessions and upload them to the Coq Youtube channel https://www.youtube.com/channel/UCbJo6gYYr0OF18x01M4THdQ

For now, these are the raw recordings:

Please, fill the activity log below with what you did each day, thanks!

Schedule

We will be flexible organizing the breakout sessions along the day, depending on who is interested for each topic.

Each day will have a "core" slot where talks and panels will happen, the preliminary scheduling proposal is:

  • 06:00-09:00 (PST time)
  • 09:00-12:00 (EST time)
  • 14:00-17:00 (GMT/UK time)
  • 15:00-18:00 (CET/Paris time)
  • 23:00-02:00 (JST/Japan time)

Additionally, open and self-organized hacking sessions will happen before and after the "core" slot. People can indicate on their registration form when they will be available.

Note: All times are CET/Paris time (UTC+1) unless mentioned otherwise.

Tuesday 15th

  • Morning (starting around 10:00 CET/Paris time):

    • formation / scheduling of working groups
    • OCaml / Coq bootcamp

  • 15:30-16:30: Introduction to the Bug Squashing Party + Development setup and tools (Ali and Emilio)

  • 16:30-17:00: Hacking time / break

  • 17:00-18:00: Coq Internals Seminar (Emilio)

  • Evening (Paris time):

    • open hacking session

Wednesday 16th

  • Morning (starting around 10:00 CET/Paris time):

    • Bug Squashing Party (Ali)
    • Hacking Sessions

  • 15:00-16:00: Debugging and bugfix creation demo (Gaëtan Gilbert)

  • 16:00-16:45: Dune session (Emilio)

  • 16:45-17:00: Break

  • 17:00-18:00: Diversity session (Emilio)

  • Evening (Paris time):

    • Bug Squashing Party (Ali)
    • Hacking Sessions

Thursday 17th

  • 10:00 - 11:00: Contributing to /developing a Coq package using nix

  • Morning (starting around 10:00 CET/Paris time):

    • Bug Squashing Party
    • Hacking Sessions

  • 15:00-18:00: Standard library event (Arthur Charguéraud's talk "Obstacles to the Construction of a Standard Library for Coq", followed with discussions)

  • Evening (Paris time):

    • Bug Squashing Party
    • Hacking Sessions

Activity Log

Here we will register what was done every day.

Activities

Please propose or request activities here; we will do a preliminary program on Jan 26th , using the Coq Call (so you are invited to join the call and help with the program)

Proposed

Requested

  • Nix Tutorial
  • Plugin porting help (If you need help porting plugins, don't hesitate to ask!)
  • looking for collaborators for generating induction schemes for inductive types with nested lists, etc. (Qinshi Wang) (HH: the parametricity plugin could probably help)
  • Categorical logic and type theory (Brayan Escobar)
  • Organization of the Summer 2022 users and developer meeting (someone from Sophia should pick this up)

Participants

  • Ali Caglayan (organizer)
  • Emilio J. Gallego Arias (Inria) (organizer)
  • Ana de Almeida Borges
  • Koundinya Vajjha
  • Rathnakar Madhukar Yerraguntla (Mycroft92 on Zulip)
  • Cyril Cohen
  • Tomás Díaz
  • Pierre Roux (won't be able to attend on Tuesday morning)
  • Kenji Maillard
  • Erik Martin-Dorel (won't be available in part of Tue.morning−Wed.afternoon−Thu.afternoon)
  • Karl Palmskog
    • Can help out with: using Dune for Coq plugins, coqdoc dev, coq_makefile hacking...
  • Evariste G from Zulip (IRL H. T.)
  • Simon Parry (enthusiastic noob, can't make Tuesday morning)
  • Rodrigo Raya (EPFL)
  • Enrico Tassi (Inria)
  • Alex Gryzlov (IMDEA)
  • Qinshi Wang (Princeton University)
  • Pierre Courtieu (willing to update his knowledge of the internals of coq)
  • Gaëtan Gilbert (Inria)
  • Julin S (interested to know about how coq works)
  • Mukesh Tiwari (University of Cambridge, interested in knowing the internals of Coq)
  • Yu Zhang (Yale)
  • Stefan Malewski (University of Chile)
  • Pierre Jouvelot (Mines Paris, PSL University)
  • Justin Fargnoli (University of Rochester)
  • Maxime Dénès (Inria)
  • Yannick Zakowski (Inria, particularly interested in the Dune session and getting Vellvm to build using dune. May be missing Tuesday morning)
  • Calvin Beck (UPenn, interested in Dune session)
  • Brayan Escobar (Noob in coq, bachelor in math, interested in logic e.g. Categorical logic and type theory- Bart Jacobs)
  • Talia Ringer (Illinois, want to push on miniF2F)
  • Arpan Agrawal (CMI, currently working on a masters thesis on the type theories behind different proof assistants, excited to learn more Coq theory!)
  • Vincent Iampietro (Université de Montpellier, will be attending the Dune session)
  • Jean-Christophe Léchenet (postdoc at Inria)
  • Yves Daaboul (Université Saint-Joseph de Beyrouth)
  • Max Fan (undergrad at Illinois, new-ish to Coq -- interested in Coq DB)
  • Jason Gross (MIT, MIRI)
  • Gregory Malecha (BedRock Systems)
    • 2pm - 10pm (intermittent)
    • 1pm is possible with notice
  • Stéphane Desarzens (graduate student at University of Bern)
  • Paolo Giarrusso (Bedrock Systems)
  • Rodolphe Lepigre (Bedrock Systems)
  • Janno (Bedrock Systems)
  • TJ Barclay (Graduate student, University of Kansas)
  • Théo Zimmermann (Inria)
  • Kazuhiko Sakaguchi (University of Tsukuba, will be busy on my own stuff but wish to watch some sessions)
  • Lasse Blaauwbroek (IHES, will only be present intermittently)
  • Michael Sammler (MPI-SWS)
  • Natasha Klaus (https://formal.land, Coq proof engineer, interested in all news about COQ)
  • Assia Mahboubi (Inria, Thursday afternoon only)

Activity log

Description of activities / sessions

Bug Squashing Party

Program

Gaëtan will give a demonstration on Wednesday at 15:00CET.

See also Debian BSP

Participants

Diversity session

  • 10/15 minutes presentation (Emilio)
  • More presentations? (add your own)
  • Open discussion topics: (some ideas below, doesn't have to be like that)
  • Closing and list of concrete actions !

jsCoq session

(There was not enough time for it; moving to a separate event https://github.com/coq/coq/wiki/jsCoq--and-CoqDB-Working-Day )

  • integrate the waCoq backend in the main branch
  • integrate coq-layout-engine
  • finish dune build rules
  • From Evariste G:
    • "Hack" on the possibility of spawning multiple workers (adjusting the views to a completely different use of the UI)
    • redesign of some UI elements
    • better docs
    • add some features from interesting plugins to jscoq (i.e. hover over and see docs)
    • brainstorm other ideas if there is time.

Participants

  • Emilio J. Gallego Arias
  • Evariste G

Dune session

Dune is a state-of-the-art incremental build system, supporting OCaml and Coq. Dune itself is a very interesting piece of software, and can be used to build Coq projects in a compositional way. In this hacking session, I'd be happy to introduce the Dune rules for Coq projects, a list of TODOs and wishlist, and guide people willing to contribute to Coq's dune support.

A preliminary program is (feel free to add your topic):

  • introduction to Coq and Dune, overview of features, feedback from users
  • elaboration of TODO list based on feedback from users; some ideas:

    • coqdep on whole theories (Ali)

    • moving from make to dune for a project (Ali)

    • CoqIDE and editor support for dune files (what to do about _CoqProject?)

    • dune init support for coq projects and plugins.

    • extraction improvements

    • depending on external files

    • dune coqtop foo.v / dune coqc foo.v

    • dune rpc for Coq / CoqIDE

    • caching (but it should work already) Recall a rule is a pure function

      { deps } ---[action]---> { targets }

      cache just memorizes these computations, thus when it the cache has a hit for a rule that has been stored already, it won't run again.

  • tutorial on coq_rules.ml (the core of Dune + Coq support)
  • question and answers important document the discussion
  • hacking

Possible follow-ups:

  • (BedRock) status on new targets, like vos/vok (and maybe coqchk/coqdoc)
  • (BedRock) customizing the timing scripts (say, to enable using perf with custom options)
  • (BedRock, Rodolphe) jump-to-definition and IDE support

Recommended reading:

"Build Systems à la carte" https://www.cambridge.org/core/journals/journal-of-functional-programming/article/build-systems-a-la-carte-theory-and-practice/097CE52C750E69BD16B78C318754C7A4

Participants

  • Emilio J. Gallego Arias
  • Ali Caglayan
  • Karl Palmskog
  • Yannick Zakowski
  • Calvin Beck
  • Paolo Giarrusso
  • Rodolphe Lepigre

SerAPI session

  • What are SerAPI future plans?

Using nix for a Coq package

  • Cyril will do a demo of how to setup nix for a package, first on a package which is already configured (like mathcomp) then on a package which does not exist yet.

  • People are invited to try to do it at the same time. For this the prerequisite is to come with nix installed. I can come at 9:30 to try and help with the nix installation.

Participants

  • Cyril Cohen

Standard Library Discussion

  • Thursday 3pm: Talk by Arthur Charguéraud talk "Obstacles to the Construction of a Standard Library for Coq".

  • Think at standard contents organized thematically

    • As an experiment, gather contributors of contents about Boolean reasoning and about lists and see if they can converge in a common library (possibly providing several variants of the same notion, possibly providing several synonymous naming schemes, so as to support all possible needs and usages)

  • Typical basic contents missing

    • n-ary operators (bigops)
    • basic category theory, basic monadic reasoning
    • basic groupoid properties of equality

  • Adopt "standard" notations for:

    • pairs and dependent pairs
      • existT: (t;..;u) (Prelude) and (t;..;u:>T), {{t,..,u}}, [t&..&u] (deptacs), "exI(t,u) (NuPrlInCoq)
      • nested sigT: introduce a notation sigma binders, T? (works very well in MetaCoq)
      • projT1 and projT2: t.1 and t.2? (alternative: T.\pi1, T.\pi2 in MetaCoq)
      • fst and snd: t.(fst) and t.(snd), t.1 and t.2 (std++)
      • proj1_sig: `t (std++)
      • exist: t↾p (std++)
      • notation for projecting p-component out of n?
      • introduce another notation than * and + for prod (ugly to add a %type to disambiguate from mul and add)? In MetaCoq we use \times, and \sum for sigmas (existT). Also reuse the n-ary variants of mathcomp: [x t1, t2 & t3], [&& t1, t2 & t3]...?
    • arithmetic
      • successors: .+1, .+2, ... (MathComp, reused in HoTT)
    • equality
      • add an equality scope (as in HoTT)?
      • eq_rect/transport: rew p in t' and rew [P] p in t' (Prelude), p#t (HoTT, UniMath)
      • eq_trans: p@q (HoTT, UniMath), p•q (HoTT),
      • eq_sym: p^ (HoTT), !p (UniMath)
      • eq_refl: 1 (HoTT)
      • f_equal?
      • dependent pairs of equality: "(=t;..;u)" (Prelude)
      • extensional equality: f =1 g (MathComp)
    • lists, sequences, vectors
      • n-vector, or n-tuple (MathComp) for vectors?
      • several notations in std++
    • set-theoretic operators
      • several notations in std++, tlc
    • booleans
      • orb: t(+)u (MathComp), `t
    • monadic reasoning
      • several notations in ext-lib
    • general
      • provide if t is pat then u else v by default?
      • composition: provide a notation by default: f o g, f ∘ g (std++, UniMath), f ⚬ g (the former would block variable o though)? ...

  • Activating standard coercions by default? (Note that at some time, the decision was that it was making the pedagogy of Coq more complicated and Coq prelude removed its coercions)

  • Use Unicode more widely in basic contents?

  • Formalizing naming schemes, supporting synonyms?

  • Provide more basic tactics?

  • Standardizing the Prelude: What goes in or out?

    • Aim for compatibility
    • Probably needs to shrink
    • Plugins need to be more independent from stdlib