Skip to content

CoqWG 2018 10 22

Jump to bottom Edit New page
Maxime Dénès edited this page Nov 22, 2018 · 2 revisions

Schedule

Monday:

  • 10-10.30: SProp integration (Gaëtan)
  • 10.30-11: Build system (Emilio)
  • 11-11.30: Coq 8.9 status (Guillaume)
  • 11.30-12: Release plan for 8.10 and round-table on current projects (everyone, led by Matthieu)
  • 12-14: lunch
  • 14-17: Discussion of current PRs and work on PRs
    • Attributes in 8.9 ?
    • unifall status (Matthieu)

Tuesday:

PRs that need to be discussed (possibly around a computer)

Issues that need to be discussed (possibly around a computer)

Notes for 22/10 (by MS)

SProp integration

  • Problems with Extraction hard to sell to users. Evaluate how hard it is to adapt to case inversion
  • Evaluation of memory pressure, reason for performance issue? PMP will investigate.

Build System

  • Tried by P. Letouzey ocamlbuild
  • Make-based system is buggy (packing, parallel builds)
  • Switch to a dune-based system (handling coq but also later plugins)
  • Linking / external plugins can use it
  • Windows building should be easier, and faster.
  • Transition possible and not too costly apparently.

8.9 release

  • blocked by elpi/opam 2 issue.
  • too many backports, how to reduce that: recall devs to reconsider their milestones.
  • credits to do.
  • nametab PR for completion?
  • Merge script to be updated by Guillaume.
  • Backporting easy in the ideal case, time-consuming in the dependent case
  • PMP proposes 3-branches setup to fix (again).

Roundtable on current projects, potential 8.10 features

  • MS: unifall / reachable from evars on the way.

    • Possibility to have an apply resolving only its evars

  • Emilio: functionalization for better parallelization and IDE apis.

    functionalization: Lots of technical issues (STM, side-effects, proof-engine and universe interactions).

    • Cleanup by reducing parallelism in code
    • "Futures are not the solution" ?

    UI issues: working towards a language server protocol (VS code, Emacs... interfaces). Currently possible but hackish. Requires important changes in the STM, and in particular a document model.

    Question of the risk of losing support for CoqIDE (Debian will remove gtk2 support soon), leaving no "officially" supported interfaces in the near future. The features we want are more or less what VSCode-Lean has. Assia points big installation and interface problems for new users, driving away some. The interface issue is a big risk that engineers Maxime and Vincent can help with.

    Proposal: try to establish a clear roadmap of the work on IDEs/document model that the main interested developers agree on. Meeting between Maxime, Emilio and Enrico at least.

    JSCoq is currently blocked by a js_of_ocaml bug...

  • Théo: still working on eauto. Will work more on the infrastructure.

  • Hugo: bugfixes and improvements as usual.

    • Integration of small inversion: new "invert" tactic or integration with "destruct" (subject to usual compatibility worries).

    Hugo and PMP discuss about libraries of tactics targeted at different users (experts vs novices, domain-specific vs general purpose).

  • Pierre-Marie:

    • Vendoring of camlp5 (more platform availability, less compilation/compat issues)
    • Cleaning-up the module system and removal of certain parts (mainly about canonical names for now)
    • Integrating Ltac2 in the main repository

  • Gaëtan:

    • SProp integration
    • Universe cleanups
    • Cleaning up the primitive projections / constants link

  • Vincent and Maxime:

    • Primitive Integers (and arrays?)
      • Removing iterators, keeping the operations, for a cleaner patch.
      • Should be available in v8.10.
    • Checker refactoring
      • Universes are different
      • Mod_subst
      • Try to share code but with fine-grain dependencies thanks to dune.
    • Refactorings/coqlib/generic tactics based on variable constants (e.g. rewrite, congruence, ...)
    • Website / Coq package index. Need for more meta-data than what is available in opam files? Brainstorming session on the question.

Notes for 23/10 (by MS)

Discourse

  • open an instance?
  • level of moderation work? Ask Gabriel.
  • How to fund it? One-time Coq consortium funds? Discussion with InriaSoft needed.
  • Proposal to moderate collectively (discuss would be closed by default).

Consortium News

  • Migration period between Inria Foundation back to Inria for employees of the Coq consortium...
  • Cannot accept funding easily right now, except maybe for gifts.
  • Yves is trying to clarify the situation with Inria. In the short term Inria supports the consortium.

Benchmarks

  • Emilio will take maintainership of the coq-bench script, with Maximes' help. Plan is to rewrite it in ocaml/improve it and maybe move away from Jenkin's CI.

"CI" issues

  • Need a quick identifiable way to contact the RM
  • Make it clear that if we merge something in master then it will be part of the next release.
  • Emilio says there's no problem with the CI policy and CompCert meets the requirements to stay in CI.

About vos/vok and vios

The two solutions look subtly different to achieve similar goals. We'd need Enrico's expertise to know why store the entire state. PMP proposes adding a diffing notion to the state so that stored states are no longer quadratic. It seems this would help having finer-grained parallelism without blowing up the memory usage. We would need some larger user feedback on the use of vios. Functionalization of states would certainly be a prerequesite.

To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.

CC0

By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.

Home

Installation of Coq

Documentation pages in this wiki

Events

Clone this wiki locally