Coq Call 2023 10 31 - coq/coq GitHub Wiki

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?