Coq Call 2022 11 02

• November 2nd 2022, 4pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics and notes

• Coq wiki

  • Coq wiki stored in github, previously was stored in house (vintage MoinMoin software) but got migrated to ease maintenace
  • Problems: limited, not indexed by Google
  • Advantages: very easy maintenance
  • Key question: "What is the alternative"?
  • We continue discussion in Zulip; will resume discussion in future call

• Job announcement boards https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneous/topic/job.20announcements

  • coq-club has been the place for jobs announcements so far, but losing visibility
  • OCaml has 3 systems (mailing list, discourse, webpage), lean uses Zulip
  • there is some overlapping we have between Zulip and Discourse, the point is raised about this duplicity, but we decide to discuss that not now
  • for now, we decide to put a link to a new Discourse tag "jobs" on Coq's website ( Théo ) , https://coq.discourse.group/tag/jobs

• Coq native bench ?

  • we now have a new capability for the bench to enable compilation of cmxs files for packages
  • we propose a new syntax will be coqbot bench native=on
  • the name of the bench can be a misleading, because of the way the test is implemented. If you do a bench with native =on what will happen is:
    • bench will configure Coq to generate .cmxs files for all .v files compiled by the bench, this modifies coqc behavior in 2 ways:
    • for each foo.v file, coqc will generate foo.ml with the "OCaml" code for foo
    • coqc will call ocamlopt to compile this file to foo.cmxs
    • moveover, when compiling regular scripts .v to .vo, calls to native_compute will actually use native compute.
  • There are few instances of that case in the bench as of today, so doing bench native=on becames dominated by the .ml to .cmxs generation
  • This effectively measures the OCaml compiler, which is very brittle (and changes a lot among OCaml variants and versions)
  • In particular, it is very hard to interpretet such numbers in any meaningful way
  • Thus, bench native=on is not really a bench, but more of check that things didn't change
  • Maxime and Emilio make the point about coordination, in particular about how to organize the performance analysis