Coq Call 2023 10 31

• October 31st 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Dealing with fiat crypto timeouts (Gaëtan, 10min)
• How to implement adding a warning/docstring/deprecation to a library file (see #18193): by adding a new (generic) metadata method to library objects? And with which concrete syntax to associate metadata to a library file? (Hugo, 5-15 minutes)
• A preliminary implementation proposal for namespaces (CEP #25) (Hugo, 5-15 minutes)
• 8.19 will come with a clearbody attribute, can we seize this opportunity to provide also sealed/unsealed attributes (Hugo, 5-10 minutes)

Roles

• Chairman: ?
• Secretary: ?

Notes

• attending : Andres Erbsen, Gaetan Gilbert, Jason Gross, Hugo Herbelin, Pierre Marie Pédrot, Pierre Roux, Théo Zimmermann

• Fiat crypto timeout

  • GG : fiat crypto timeouts a lot (at 3 hours), even trying to use larger machines
    what should we do, current situation not reasonnable
  • what about separating the job for bedrock2 ?
    • not using bedrock master in fiat crypto
  • JG : do a reduced CI target
    • would require stats on what files trigger most CI failures
    • TZ : won't have time to extract those data before a few months
  • AE : takes much less than 3 hours on my machine
    • JS : we are using "make -j1" on CI due to limited RAM on CI machines
    • PMP : should we try -j2 on more beefy CI machines
    • GG : remember having tried but without observing any effect
    • TZ : should probably ping T Martinez
  • TZ : would it make sense to have two targets:
    • non beefy files compiled with -j2
    • then beefy files compiled with -j1
    • GG : we can just try -j2 and once it fails continue with -j1
  • JG : have the bedrock2 CI job just compile the submodule of fiat crypto
  • TZ : could we just have a specific branch of bedrock2 be used by fiat crypto
    • no, too likely to break
  • JG : will try to hack the CI in the coming weeks (AE could also do it)

• HH : Fiat crypto legacy currently failing on CI, submitted a PR to fiat crypto, it should just be merged

  • AE : CI failing there
  • HH : it seems to be using a too old version of Coq

• HH : deprecating files

  • PR : would like an attribute syntax (reusing deprecation(note="...", since="..."))
  • PMP : would prefer a "string" rather than something without letters like "###[attribute]"
  • TZ : something like Module Attributes [deprecated(note="...", since="...")] or Library Attributes [...]

• JG : the attribute syntax should be extended to support warnings instead of just deprecation

  • TZ : we already have a warning attribute to (dis)activate given warnings
  • GG : OCaml call that "alert"
  • JG : should give access to user to the warning categories
  • GG : figure details in the PR

• HH : clearbody, sealed/unsealed

  • GG : current bug in clearbody, in

    Section S. #[clearbody] Let x := 0. Definition foo : x = 0 := eq_refl.

    the definition should fail
  • PMP : could take the opportunity to add an "expand" attribute to Let to substitute or add a let/in when closing the section

• HH : namespaces, simple prototype

  • PMP : probably not worth discussing right now as most interested people are not here (Cyril, Enrico,...)
  • discussions on how to handle name clashes (allow them or not?)
  • TZ : what was the status of the namespace CEP?