Coq Call 2020 05 13

• May 13th 2020, 4pm-5pm Paris Time
• The call will be on rendez-vous: https://rendez-vous.renater.fr/coq-call BBB (room now deleted)
• Add your topics below

Topics

• Very brief update on 8.12 [Théo & Emilio]
• Getting a detailed list of things to do and open problems about the switch to dune (Enrico).
  • https://github.com/coq/coq/projects/15
  • Native compute [main open problem specification on when to enable/disable] https://github.com/ocaml/dune/pull/3210
  • CI jobs: async / quick , similar problem to native compute, how to enable / disable ?
  • vok / vos support : specification needed, targets depend on Coq version
  • Non-blockers:
    • dune coqtop
    • dune coqdoc
    • dune coqchk
• More on plans w.r.t. linkall and static initialization (Emilio)
• Update about ongoing declare / proof handling work (Emilio)
  • hooks / chaining is an issue
  • extra needs noted by Pierre-Marie ?
  • vio path / restrict / universes ?
• Possibility of making canonical structures with function fields a bit more useful? (Janno)
  • See https://github.com/coq/coq/issues/11189#issuecomment-559107164
  • also: why only -> and not dependent forall?
  • How much work would be involved? Could I (Janno) implement any of it?

Notes (from Matthieu)

8.12

Branching on friday seems going well (20 PRs left to merge)

Dune

Getting a detailed list of things to do and open problems about the switch to dune (Enrico).

https://github.com/coq/coq/projects/15

• CI jobs: async / quick , similar problem to native compute, how to enable / disable ?

Current design tied to make. Problem seems to be what happens when changing profiles of builds. One way would be to invalidate compiled files from a different profile when switching. Profiles are not necessarily shared among multiple libraries (e.g. coq and ltac are separate libraries that are composed). Will need to patch dune to allow a profile to set coq flags.

• vok / vos support : specification needed, targets depend on Coq version

Different design where vos/vok are actually just vo files would simplify the build (no specific rules)

• Native compute [main open problem specification on when to enable/disable] https://github.com/ocaml/dune/pull/3210

Slightly harder problem because the need to disable native means cleaning up the stale files afterward. dune supports this logic for ocaml already, when removing a module.

It seems we can simply follow the path of using configure to generate the profile with or without native-compute. And merge the PR above!

Dune beta is coming soon.

About vos/vok, we could either make dune handle them natively (similarly to native files), or move them back to vos. Probably in both cases we still need to handle the change of mode through a configure flag/profile.

Side-remark: a project on vo-related gathers issues/PRs about the format, which can now include arbitrary binary segments (PR by Pierre-Marie).

• Non-blockers:
  • dune coqtop
  • dune coqdoc
  • dune coqchk

Canonical Structures and ->

Possibility of making canonical structures with function fields a bit more useful? (Janno)

• See https://github.com/coq/coq/issues/11189#issuecomment-559107164
• also: why only -> and not dependent forall?
• How much work would be involved? Could I (Janno) implement any of it?

Removing the non-dependency check is not enough. Discussion to continue on Zulip.

Other topics of Emilio moved to next week.