Changes in Coq since the last WG

From October 22^nd^ to December 16^th^

Foreword

Aim

• Enable non-insiders to get an overview of what’s going on and who’s working on what

Methodology

• List of all merged PRs in the period

  git log --since='2018-10-22' --until='2018-12-16' --pretty=oneline | grep 'Merge PR' | sed -e 's/^.*Merge PR #\([0-9]*\): \(.*\)$/\1: \2/'
  

• A bit of triage (this document)

• Subjective selection of what stands out (this talk)

Performances

8708: Pierre-Marie improved the performance of conversion by changing an unfolding heuristic.

To quote the author:

We favour unfolding of variables over constants because it is more frequent for the former to depend on the latter. This has huge consequences on a few extremely slow lines in mathcomp, up to dividing by 3 single-line invocations that were taking about 30s on my laptop before the patch.

8841: Pierre-Marie implemented a performance optimization

8824: Pierre-Marie improved the performance of the kernel by dropping convertibility checks on domains of pattern branches in pattern-matching

8255: Pierre-Marie improved type-checking of application nodes

This PR implements a type-checking algorithm for application nodes that is asymptotically faster than the current implementation. It does it by changing the representation of FProd nodes so that they contain term closures instead of fconstr. The rationale is that it contains an open term, and we reuse the same trick as already implemented for lambda and case representation. Then we leverage this to substitute lazily values in product types.

Features

8870: Maxime updated the -bytecode-compiler and -native-compiler flags of coqc and coqtop

They allow to dynamically enable or disable the VM and native compilers.

8515: Gaëtan redesigned how commands declare and handle their attributes (8515, 8917)

8766: Emilio implemented basic support in Nametab for efficient completion

8779: Pierre-Marie removed the “implicit tactic” feature

8451: Gaëtan added a Subgraph option to the Print Universes command

From the author:

Hopefully this is helpful when researching universe inconsistencies in a monomorphic context.

8987: Maxime deprecated hint declaration/removal with no specified database

9001: Emilio removed the deprecated option Automatic Introduction

8920: Gaëtan deprecated the “Typeclasses Axioms Are Instances” option

8890: Hugo improved some interaction between notations and coercions

8850: Gaëtan added private universes for opaque polymorphic constants

This lets opaque polymorphic constants have universes which are needed for the body but which do not need to be provided when using the constant (because we guarantee that some acceptable universe always exists, and since the constant is opaque it can't be observed).

8965: Jason enabled user-defined string notations

8811: Gaëtan added EConstr-aware functions to produce kernel entries

9015: Vincent added a warning when, in type classes, the RHS of :> is not a class

Théo then improved the manual by indexing the different uses of :> (9105).

Build-system, CI

Emilio improved the dune-based build-system (8802, 8762, 8744, 8903, 8912, 8901, 8960, 8959, 9035, 8948, 9068, 9106, 9151, 9147)

and Gaëtan also contributed (8956, 8961)

Théo improved default.nix (8821, 8836)

8711: Emilio improved CI for MS-Windows

8868: Vincent updated the Docker image used for CI

so as to use recent versions of OCaml and Camlp5

8918: Gaëtan fixed overlays on Windows CI

8927: Kamil Trzciński (from Gitlab) improved performances of CI on gitlab

Théo then refined that change to prevent some failures (9119)

Vincent proposed nix helpers for debugging external projects from CI (8978, 9057)

9018: Emilio provided a script to automatically setup overlays

and then improved the related documentation (9022)

9033: Gaëtan fixed installation of the stdlib documentation

9016: Gaëtan improved the log of failed builds on appveyor

9021: Gaëtan improved the merging script

9087: Maxime added a job building the stdlib with async-proofs on

Test suite

Hugo improved the test-suite (8786, 9193)

8655: Vincent made the test-suite run the checker on all generated .vo files

This revealed a few issues in the checker and will probably prevent similar problems in the future.

Documentation

github user sampablokuper improved the manual (8799, 8798, 8766)

8813: Vincent fixed a few rendering issues in the manual

8737: Tej Chajed improved a few error messages w.r.t. record fields

8851: Matthieu wrote the credits for Coq 8.9

Théo improved the manual (8845, 9036, 9121, 9196, 9073)

8809: Emilio improved the developer’s documentation

8884: Guillaume improved the rendering of the credits

8926: Théo fixed the CHANGES file

so as to properly reflect what will be in 8.9

Théo documented the merging process (8098) and the creation of code owner teams (9053)

8408: Enrico improved the HTML rendering of the ssreflect library documentation

8894: Gaëtan improved an error message related to polymorphic universes

8975: github user soraros improved the documentation of the micromega tactics

8911: Jim ensured that all flags and options are documented

9150: Emilio enabled the “incorrect doc comment” warning and fixed comments accordingly

Standard library

8365: 李弈帥 (Yishuai Li) contributed the ByteVector type to the Strings library

ByteVector provides convenience in processing structured bytes. For example, to parse a binary file of a certain format, we can convert the string into ByteVectors. For numeric fields, we can convert it to Bvector and get its value in N.

The motivation comes from coq-http2 that specifies the behavior of HTTP/2 servers. The encoder and decoder use ByteVector to represent the frames, whose fields are mostly of fixed size.

8812: Vincent made ssreflect use Coqlib

8815: 李弈帥 (Yishuai Li) contributed lemmas about numbers and vectors

8888: Vincent Semeria proved that the set of real numbers is uncountable

8807: Larry Darryl Lee Jr. added two lemmas to the List library

7221: 李垚 (Yao Li) implemented the OrderedTypeEx interface for strings

Refactoring

Hugo performed some cleaning in the kernel

He removed some code duplication by moving fold_constr_with_full_binders into the kernel (7186) and moved Global.constr_of_global_in_context to Typeops and renamed Global.type_of_global_in_context to Typeops.type_of_global (8687).

8707: Pierre-Marie separated the kernel implementation for the term cache and its reuse in the out-of-kernel CBV reduction, allow[ing] for further cleanups of static or unused data

8777: Pierre-Marie cleaned the side-effects API, moving it into Safe_typing

8753: Emilio made config a “proper” library

8684: Maxime did some cleaning in the kernel

8825: Emilio moved object_name into Libobject

8688: Hugo made the evar_map printers from Termops take an environment as arguments

8844: Gaëtan moved the abstract tactical to its own module

8871: Emilio moved a few functions from Libnames to Nametab

8773: Maxime refactored the checker

so as to reuse the code that is shared with the kernel, instead of copying it

Gaëtan then removed the printers used for debugging the checker (8949), improved the error message when validation fails (9005), and sanitized the checking of inductive types (9032).

Emilio then removed some code duplication (9063).

Emilio renamed Vernacinterp to Vernacextend (8919, 9003)

8914: Emilio decoupled CoqProject_file and Feedback

8902: Emilio added CAst.t nodes into the tactic AST

7925: Pierre-Marie moved Names.transparent_state to its own module TransparentState

8982: Emilio improved the control of “open proof” exceptions

8929: Gaëtan refactored liftings

Emilio refactored the toplevel

More specifically printing (8950); and compilation-related functions now have their own module (8950).

He then allowed to specify default options (8826).

8705: Emilio turned hooks into optional arguments

9169: Emilio ported rtauto and auto to the new proof engine

CoqPP

Pierre-Marie worked on coqpp

External plugins [can] use the coqpp tools in lieu of camlp5 macros (8763).

8667: Emilio derived gramlib from Daniel de Rauglaudre’s camlp5 (8667, 9023, 9064, 9065)

8843: Gaëtan removed .ml4 files from coqIDE sources

Pierre-Marie removed the deprecated Token module and dead-code from gramlib (8899, 8907, 8915, 9069)

Pierre-Marie ported the parser to the type-safe API of Camlp5 (introduced in version 7.06) (8923), but reverted this change (8944) and made it again (9051)

Gaëtan fixed CoqMakefile w.r.t. .mlg dependencies (8966)

Emilio and Gaëtan changed the make-based build-system to pack and link gramlib (8985, 9074)

8945: Emilio finally removed all dependencies to Camlp5

9127: Pierre-Marie remover leftover code that used to handle ml4 files

Cleaning

8741: Matthieu improved the handling of evars in type-classes

8780, 8781: Gaëtan performed some cleaning w.r.t. projections

8864: Maxime removed many calls to Environ.empty_env

8752: Gaëtan removed fragile pattern matching in CClosure

8852: Matthieu cleaned the handling of obligation evars

8866: Gaëtan added a check for universe instances in Typing

8889: Matthieu improved “Program” hooks

8760: Gaëtan improved the printing of universe names

7881: Github user whitequark reimplemented Store using Dyn

Emilio removed the cook_proof and start_proof stubs from Pfedit (8999, 9002)

9017: Jim removed undocumented options for profiling in ssreflect

8998: Emilio removed the Proof_type module

9046: Gaëtan made the Goptions.declare_* functions return unit

9072: Maxime cleaned the STM flags

9102: Emilio removed some aliases from Tacexpr

8096: Maxime enhanced the libobject API

9172: Emilio reworked the proof interface

Bug fixes

Hugo fixed bugs in notations (8806, 8867, 8187)

Guillaume fixed bugs in CoqIDE (8803, 8804)

Matthieu fixed a type-classes bug (8849)

Pierre-Marie fixed a bug in Ltac (8759)

Emilio fixed an anomaly in printing (8834)

Hugo fixed a bug related to tactic-in-terms and notation scopes (8745)

Gaëtan fixed a few bugs in the checker (8877, 8882, 8874, 8996)

Pierre-Marie fixed an algorithmic issue in the vernac guardedness checker (7952)

Enrico made the ssreflect dispatch intro pattern stricter (8856)

Enrico reverted 7936: “Do not allow spliting in res_pf, this is reserved for pretyping” (8934)

Jasper Hugunin made the behavior of “Automatic Introduction” more uniform (8820)

Maxime fixed the substitution of inline global reference in tactics (8972)

Quoting the change-log:

Binders for an Instance now act more like binders for a Theorem. Names may not be repeated, and may not overlap with section variable names.

Pierre-Marie improved the handling of bound universe names (8601)

Hugo fixed the grounding of open terms in fixpoints (8892)

Gaëtan fixed bugs related to universes (8936, 8854, 8974)

Vincent fixed the VM compilation of int31 eliminators (8886)

Enrico fixed typeclasses resolution in case/elim patterns (8955)

Gaëtan fixed the top name in CoqIDE (8991)

Hugo fixed a few issues in CoqIDE (8968)

Enrico fixed some race in the stm (8712)

Gaëtan made the Init module not exported (9013)

Jim fixed bugs in proof diffing (8967, 9101)

Gaëtan prevented redeclaration of constraints in Include (8995)

Maxime fixed a race condition triggered by fresh universe generation (9155)

Hugo fixed the debug printers: gramlib needs Loc (9197)

Hugo fixed a warning that was too often raised

Other PRs merged in the period

• 8827: Revert "[ci] Pin CI_REF to plugin_tutorial to use not yet merged commit."
• 8797: [doc] [api] Update odoc to new release 1.3.0
• 8814: Comment Environ.set_universes
• 8765: Give code ownership of merging doc to pushers team to notify members when it changes.
• 8751: Rename checker/{main->coqchk}
• 8750: [ci] [doc] Notes about branch names.
• 8895: gitignore test-suite/misc/poly-capture-global-univs/src/evil.ml
• 8842: Towards seeing Global purely as a wrapper on top of kernel functions
• 8857: [library] Better sizing for libobject hashtbl.
• 8896: Expose Typing.judge_of_apply
• 8928: Fixes #8910: typo in nameops.ml
• 8947: Ensure termination of file_exists_respecting_case
• 8958: [clib] Remove unneeded get_extension function.
• 8938: [Plugins] Remove some dead code
• 8962: [ci] Add paramcoq to CI.
• 8979: Skip submodules in HoTT CI script.
• 8957: Fix -top for univbinders output test.
• 8976: CoqHammer CI
• 8906: [Goptions] More detailed error messages
• 8992: put protocol/ in ide/.merlin
• 9026: [Documentation/Combined Scheme] Typo
• 9031: Rename gh->bug_ test files
• 9049: [default.nix] Add graphviz for STM DAG printer
• 8924: Misc updates to codeowners
• 9044: Remove pidetop from CI
• 9055: [dev] fix create_overlay wrt branch names containing /
• 8933: Make initial evar map argument to check_evars_are_solved optional.
• 9075: [ci] Set windows jobs to allow_failure: true
• 8986: Put -indices-matter in typing_flags
• 7696: Remove some univ_flexible_alg from cases
• 7033: Remove obsolete files from dev/doc
• 9089: Fix #9076 (warning appears when running test suite)
• 8727: [options] New helper for creation of boolean options plus reference.
• 9094: [lib] Remove leftover flag print_mod_uid
• 7153: Make OrderedTypeFullFacts a module functor
• 9041: [Windows CI] Do not build any addon if WINDOWS is not enabled_all_addons.
• 9054: [ci] [appveyor] Move Appveyor to OPAM 2.
• 9104: coqide: Remove unused win32_kill C function
• 9109: Fix numeral notations doc by indenting
• 9112: [release doc] vX.X branches are now automatically protected.
• 9134: CI: track dev branch of coq-simple-io
• 9140: [ci] Add four color theorem proof to CI
• 9177: add relation-algebra to CI test suite
• 9077: Rename generated directory gramlib__pack -> gramlib/.pack
• 9145: Do so that an error message follows the "Error:" header on the same line
• 9217: [ci] [appveyor] Temporally disable test suite on Appveyor.
• 9211: Fixing incorrect mention of coercions as being part of the interning phase
• 9210: Fix issue #9176 : Windows: change cygwin repo
• 9117: Accept argument names for extra arguments with "extra scopes"
• 9194: Fixing uses of sed in #8985 which do not work on MacOS X