Changes in Coq since the last WG (20181216)

Changes in Coq since the last WG

From December 16^th^, 2018 to February 3^rd^ 2019

Foreword

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

• 107 merged PRs in the period

Features

Extended introduction patterns

• Enrico extended the ssreflect introduction patterns (6705, 9200, 9341).

CoqIDE

• 9178: CoqIDE: Restoring configuration of default width/height of main window. (Hugo)

Standard library

• 8062: Add Z.div_mod_to_quot_rem tactic, put it in zify (Jason)

Refactoring, cleaning

• 9172: Rework proof interface (Emilio)
• Maxime did some cleaning and refactoring in the STM (9220, 9219, 9218, 9331, 9263)
• 9153: Move reduction modules to tactics (Emilio)
• Gaëtan did some refactoring in the kernel (9237, 9159)
• Gaëtan did some cleaning related to template polymorphism (8488, 9182, 9325)
• 9139: [engine] Allow debug printers to access the environment (Emilio)
• 9276: Remove dead code from CClosure (Pierre-Marie)
• 9027: Refactor checking of inductive types (Gaëtan)
• 8734: Make diffs work for more input strings (Jim)
• Maxime disabled Refine instance Mode by default (9270) and made Instance without a body always open a proof (9274)
• 9043: [windows] Cleanup cruft from dev/build/windows (Emilio)
• 9095: [toplevel] Deprecate -compile flag in favor of coqc (Emilio)
• 9395: Global [open Univ] in UState (Gaëtan)

Bug fixes

• In the STM, by Enrico (9206, 9335, 9372, 9399), by Gaëtan (9222, 9223), by Maxime (9048), by Emilio (9421)
• In automatic introduction, by Jasper (9160)
• In notations, by Hugo (9231, 9337, 9214)
• In ltac, by Gaëtan (9248)
• In printing, by Hugo (9249, 8373)
• In pretyping, by Gaëtan (9241)
• In interpretation, by Hugo (9292)
• In instances, by Maxime (9273), by Jasper (9307)
• In coqc and coqtop, by Maxime (9316, 9357)
• On MS-Windows, by Michael (9192, 9225)
• In universe polymorphism, by Gaëtan (9361)
• In canonical structures, by Enrico (9377)
• In the checker, by Gaëtan (9250)

CI, build systems, test suite

• 8856: Compile Coq with OCaml 4.08 (Emilio)
• 9215: Set up CI with Azure Pipelines (Gaëtan) (see also 9243, 9318 by Kayla Ngan, 9332)
• 9081: [dune] A new Makefile.dune target for each package (coq, coqide-server and coqide) (Emilio)
• 9265: Do not exclude "opened" bugs from report (Maxime)
• 9278: [ci] Annotate plugins and libraries (Théo)
• Exit travis, by Gaëtan (9224, 9383)
• 9277: [dune] Build refman with fatal warnings like in the Makefile build (Théo)
• 9088: Add CI job running test suite with async-proofs on (Maxime)
• 9440: Create deployment environment for Cachix (Théo)

Community, documentation

• 9183: List members of the code of conduct enforcement team (Théo)
• 9143: Documenting the internal role of to_string and print in Names (Hugo)
• Gaëtan improved the commit messages produced by merge-pr (9242, 9353)
• 9339: Move plugin tutorial to team ownership
• Various improvements to the user manual (9374 by Laurent, 9392, 9449 and 9402 by GitHub user akr, 9269 by Jim, 9384 by Théo, 9391 by David A. Dalrymple, 9424 by Ryan Scott, 9435 by Gaëtan).

Other PRs merged in this period

• 9238: CI: simple-io now depends on ext-lib
• 9266: Make @SkySkimmer an owner of test-suite/report.sh
• 9247: Fix typo in gallina specification language doc
• 9264: Fix shallow flag in vernac state
• 8977: Update .mailmap.
• 9282: [ssrmatching] update license banner (fix #9281)
• 9305: Remove formal-topology from CI (Maxime)
• 9309: [ci] Add Verdi Raft with dependencies to CI (Karl Palmskog)
• 9322: [ci] Update fiat-crypto legacy
• 9327: [Manual] Remove link to non-existing CSS file
• 9346: Add .nia.cache to .gitignore
• 9345: [ci] Update fiat-crypto to the new pipeline
• 9326: [ci] compile with -quick & validate after vio2vo
• 9340: Add badges linking to a selection of up-to-date Coq packages.
• 9308: Remove outdated gitignore coqprojectfile.ml
• 9239: [ci] [appveyor] Pass -j2 to Appveyor's build and build test suite again
• 9382: Transfer maintenance of appveyor infrastructure to the CI team
• 9347: At Qed, if shelved goals remain, emit a warning instead of an error
• 9394: [nix-ci] Maintenance
• 8637: Update -compat to support -compat 8.10
• 9362: Fix makefile .merlin for unit tests
• 9420: [doc] Remove emacs mentions from INSTALL
• 9417: Update update-compat.py script
• 8720: [Numeral notations] Use Coqlib registered constants
• 9442: Update pinned nixpkgs.
• 9448: [ci] [ocaml] Fix OCaml trunk builds.
• 9415: Simplify the GitHub issue template