Hydras & Co. 0.9

This release has been tested for compatibility with Coq 8.13-8.15 and MathComp 1.12-1.14. The gaia-hydras package requires Coq 8.14 or later.

Release highlights

The experimental bridge to the Gaia project allows now to import some definitions and theorems of the so-called Ketonen-Solovay combinatorial machinery into the Gaia environment (see Chapter 7 of the documentation).

The first topics treated in this version are: canonical sequences, accessibility, and a few rapidly growing hierarchies of arithmetical functions.

Revision book to page 82. deprecate a few symbols by @Casteran in #130

Full Changelog: v0.6...v0.9

Hydras & Co. 0.6

This release has been tested for compatibility with Coq 8.13-8.15 and MathComp 1.12-1.14.
The gaia-hydras package requires Coq 8.14 or later.

Release highlights

• Build a bridge with the Gaia library by @Casteran in #112, #115, #117 and #120
• Use LibHyps by @Casteran in #119

Other changes

• Move definition of gaia-hydras package to nixpkgs. by @Zimmi48 in #98, #99 and #101
• Update README.md on gaia and reference JFLA 2022 paper by @palmskog in #104 and #107
• Fix scheme issue by @Casteran in #116
• Test compatibility with Coq 8.15 by @palmskog in #119

Full Changelog: v0.5...v0.6

Hydras & Co. 0.5

Release highlights

• Inclusion of Ackermann sub-library originating from Goedel (@Casteran and @palmskog, #20, #21).
• New gaia-hydras package bridging the ordinals in the Gaia library and the Hydra-battles library (@Casteran and @palmskog, #56).
• Snippets included in the book are now automatically extracted from the code with the help of Alectryon 1.4 and a custom driver (@Casteran, @cpitclaudel and @start974, #44, #47, #48, #57, #66, #67, #71, #73, #78, #84, #97).
• Introduction of Docker-Coq-Action and Coq Nix Toolbox-based Continuous Integration. Documentation is automatically generated in a CI / CD pipeline and uploaded to the coq-community website (@palmskog, @start974 and @Zimmi48, #2, #6, #11, #22, #40, #41, #42, #58, #62, #63, #68, #69, #75).
• Warning-free compilation with Coq 8.13 and 8.14. Drop compatibility with Coq 8.11 and 8.12 (#16, #18, #37, #52, #89, #97).
• Addition and refactoring of type classes Comparable, TotalPreOrder, Decision (@Casteran, @palmskog, @start974, @Zimmi48, #39, #43, #76, #79).
• Switch license to MIT (#4).