Coq Call 2021 03 17 - coq/coq GitHub Wiki

• March 17th 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Support the Ltac debugger in CoqIDE https://github.com/coq/coq/pull/13783

Notes

• Ltac debugger: more work needed by Emilio and Jim on a common PR

• Emilio writes: Plan for coqnative kinda looks like:

  • use dune for Ocaml parts [in parallel]
  • coq_makefile for stlib
  • unification of coqlib / loadpath code among tools inlcuding coqdep
  • removing coqdep_boot which is unused after use dune for OCaml have coqnative use sys.init