Organization of the week

Before the week

Read carefully the previous announcing mail, especially the Homework section.

Participants

• Reynald Affeldt (not available Thu 8:00-9:00 Fri 8:00-9:00, NB: +7h jetlag with France)
• Xavier Allamigeon (Tue morning, Wed morning)
• Yves Bertot (not available Tuesday afternoon)
• Quentin Canu (not available Wednesday from 16:00 CEST and Thursday morning)
• Cyril Cohen (available Tue - Fri, 9:00 - 19:00 CEST, minus lunches and tea breaks)
• Marie Kerjean (available on mornings)
• Pierre Roux
• Kazuhiko Sakaguchi
• Pierre-Yves Strub (not available Tuesday morning)
• Enrico Tassi (available Tue, 9:00 - 18:00 CEST, Wed - Fri more like 10:00 - 17:00 :-)
• Laurent Théry
• Anton Trunov

Kickoff Session

Everyone joins https://jitsi.riot.im/HB-mathcomp on Tuesday April 6th at 9:00 CEST

If we get unwanted visitors, we will put a password and post it on Zulip #mathcomp private stream.

• 9:00 - 9:15 - chit chat

• 9:15 - 9:45 - Enrico ports one structure in order.v to refresh our memory.

  He will follow the porting process described below (as everyone else is expected to do).

  Here is a recording

• 9:45 - 10:00 - break

• 10:00 - 12:00 - We form three groups, dispatching Cyril / Enrico / Kazuhiko, each on a different file.

  Each member of each group ports one structure to try his setup and the process and finally gives the lead to another member of the group.

We will by then all have a working setup and everyone can take their own file(s) either alone or in groups, following the process below. If you need help, tag Cyril or Enrico or Kazuhiko on Zulip (or anyone else really) to get them to join your jitsi.riot.im.

Porting Process

Everyone pushes commits on the math-comp/math-comp repository, hierarchy-builder branch without force push.

Please respect the following methodology, which is supposed to ensure that we do not run into conflicts and that everyone gets assistance as soon as possible.

1. Find an untaken file at #733 or in the dependency graph

   Make sure the file is accessible by a green path before taking a file.

2. Tick the tickbox "taken" for your file in #733

3. Declare you start porting the file on Zulip by

   • joining/creating the rendez-vous renater link dedicated to your file: https://jitsi.riot.im/HB-mathcomp-<file without .v> e.g. https://jitsi.riot.im/HB-mathcomp-order

   • opening one topic named HB-mathcomp-<file without .v> for your file e.g. HB-mathcomp-order on #math-comp private Zulip stream and posting the visio jitsi.riot.im link immediately as the first post of the topic.

   Strictly respecting the naming conventions will make sure everyone finds their way to you.

   Indeed in case of problem, tag Cyril or Enrico or Kazuhiko (or anyone else really) on Zulip to get one of them to join your visio room on jitsi.riot.im.

4. Share your screen and start porting the file alone or in a group.

   • Set up your dev environnement, you can also follow this more complete tutorial

     1. If:
        • it is the first time: clone the mathcomp repo and checkout the branch hierarchy-builder

          git clone [email protected]:math-comp/math-comp && cd math-comp && git checkout hierarchy-builder
          

        • otherwise to a pull rebase (assuming the math-comp repo is under origin)

          git pull -r origin hierarchy-builder
          

     2. Make sure you have Coq+HB

        • Either install Coq 8.13 + HB 1.1.0 through opam

          opam update && opam install coq.8.13.1 coq-hierarchy-builder.1.1.0
          

        • or run nix-shell from the root of the repo

          • you must have installed nix and cachix as described on math-comp wiki: Using nix

          in case we need to patch HB this is what will make it work out of the box

     3. Uncomment your file in mathcomp/Make
     4. compile your file, e.g. order.v make -j8 -k -C mathcomp ssreflect/order.vo
     5. launch your preferred editor (emacs/proofgeneral, vscode or vscodium, coqide are all supported).

   • Edit the file

     • replace structures with type carriers with HB instructions (HB.mixin and #[mathcomp] HB.structure). Do not change morphism hierarchies or predicate hierarchies (for now),
     • adapt notations like [fooBar of T] mimicking other files (eg ssralg.v)
     • you may create HB.factories if you want, but do not create additional structures, except if they are substructures (e.g. IsSubZmodule in ssralg.v).
     • replace Canonical declarations of the above structures by HB.instance.

   • When you want to stop, there are three cases

     • if you did not finish, comment the rest of the file and make sure everything compiles by running make -j8 -C mathcomp. Do not just evaluate to the end of the buffer since there might be open sections and modules. Then commit, pull -r and push without force git add order.v && git commit && git pull -r && git push then untick your "taken" box at #733.

       As a courtesy for the next people working on the file, you may add "STOP" as the first line of the commented out code, so that it is easier to find.

     • if your file fully compiles, without commenting code, but did not update the doc, re-enable some disable parts, or tidied the content, then follow the above instructions (check compilation, commit, pull -r and push without force, untick "taken") and additionally tick the box "compiles but needs more work" at #733.

     • if you finished: the doc is complete, there are no unexpected commented code, i.e. if the code would be ready to release, then follow the above instructions (check compilation, commit, pull -r and push without force, untick "taken", untick "compiles but needs more work") and additionally tick the box "finished" at #733.