Coq Call 2022 11 02 - coq/coq GitHub Wiki

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