Changes in Coq since the last WG (20181022)
From October 22^nd^ to December 16^th^
- Enable non-insiders to get an overview of what’s going on and who’s working on what
-
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)
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.
8824: Pierre-Marie improved the performance of the kernel by dropping convertibility checks on domains of pattern branches in pattern-matching
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
FProdnodes so that they contain term closures instead offconstr. 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.
They allow to dynamically enable or disable the VM and native compilers.
From the author:
Hopefully this is helpful when researching universe inconsistencies in a monomorphic context.
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).
Théo then improved the manual by indexing the different uses of :> (9105).
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)
so as to use recent versions of OCaml and Camlp5
Théo then refined that change to prevent some failures (9119)
and then improved the related documentation (9022)
This revealed a few issues in the checker and will probably prevent similar problems in the future.
so as to properly reflect what will be in 8.9
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.
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
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).
More specifically printing (8950); and compilation-related functions now have their own module (8950).
He then allowed to specify default options (8826).
External plugins [can] use the
coqpptools in lieu ofcamlp5macros (8763).
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)
Quoting the change-log:
Binders for an
Instancenow act more like binders for aTheorem. Names may not be repeated, and may not overlap with section variable names.
- 8827: Revert "[ci] Pin
CI_REFtoplugin_tutorialto use not yet merged commit." - 8797: [doc] [api] Update
odocto 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_extensionfunction. - 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
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq 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.