CoqWG 2018 12 19

Organization

Coq Working Group 19th of December, from 10am to 5pm by visioconference.

Recording of the morning session.

Tentative schedule

10h-12:00

• Changes in Coq since the last WG (Vincent, 15mn?) Link ?

• What about removing the opaque proofs from the safe_env: https://github.com/coq/ceps/pull/40 (Enrico, 40 minutes) Pending on checking this is doable with the current modules/functors. Allows the kernel to be unaware of the stm (no more Futures). Everyone seems ok with the change.

• Organize command line arguments (and maybe the state, in the future) using objects: https://github.com/coq/ceps/pull/39 (Enrico, 20 minutes)

• Current status of II/IR and call for help (Matthieu, 10 min) TODO: write a mockup of the design! Pierre-Marie and Maxime could help.

• Coq Users in Paris Meetup (@ejgallego @Zimmi48, 15mn?)

• Decide whether to vendor plugin_tutorials (15mn?) Licence is ok. Where to put them?

14h-17:00

• Experience report: type classes in Mathematical Components (Vincent, 30mn?)
• Format of _CoqProject file (Arthur, 15mn?).
  • It would be great if any valid argument for coqc and coqide could be included in the contents of _CoqProject.
  • Currently only a subset of flags is recognized, others can be passed using -arg but it is really ugly.
  • Moreover, the _CoqProject parser does not share the same parsing technology as coqtop.
  • What would it take to parse _CoqProject using the same tooling as what coqtop uses, and accept all the same flags?
• Discussion about adding a flag to name ssr-introduced variables (Arthur, 15mn?)
  • SSR policy is that variables introduced anonymously are given special names that are inaccessible to the user.
  • For some type of formalizations (e.g. formal metatheory), introducing all names explicitly is not a viable option.
  • A first issue with SSR names is that the goals become hard to read name is longer than they could be.
  • A second issue is that sometimes it is still convenient for the user to refer to these names, especially during development phases, or when the user has good reason to believe that the name assigned is robust enough.
  • Furthermore, the new mechanism of => [^foo] for providing name templates leads to names that are "partially use-specified, and partially generated", so it is not clear whether they should be accessible or not.
  • Arthur suggests to make anonymously introduced variables accessible by default, and provide a optional flag for users who really want to prevent themselves from using generated names.
• Additional extensions to ssr move and rewrite patterns (Arthur, 15mn?)
  • Abitity to refer to subgoals by label, e.g. /n:{mytac} or /side:{omega}: https://github.com/coq/coq/issues/9158
  • https://github.com/coq/coq/pull/6705
  • https://github.com/coq/coq/issues/9130
  • TC introduction > was implemented.
  • What about viewing > as a standalone pattern? Same for +? https://github.com/coq/coq/pull/9200
• Drop of vio support and strategy for merging the PR that removes .vio checking with the PR that implements vos (Arthur, 30mn?)
  • Adding vos for compilation of interfaces without proofs: https://github.com/coq/coq/pull/8642
  • Removing vio support and vio to vo conversion: https://github.com/coq/coq/pull/8783 Yet this removes "too much" w.r.t. the previous PR.
  • Question of how to resolve the atomicity of the write of .vo files (and .vos files) to ensure safety for make -j: is it possible to write into .vo.temp and make a mv at the end?
• Status and future of the abstract tactic https://github.com/coq/coq/issues/9146 (@ejgallego, 15mn?)
• A report on implementing an LSP server for Coq (Maxime, 10 min)
• Attributes syntax and roadmap (Matthieu, Théo, 30min, probably closer to ∞).