https://github.com/QuickChick/QuickChick
Tip revision: ae0c2bc2a1308a44950c119e527c7d80d5d592e4 authored by Pierre Roux on 06 July 2024, 13:00:52 UTC
Adapt to https://github.com/coq/coq/pull/19310
Adapt to https://github.com/coq/coq/pull/19310
Tip revision: ae0c2bc
CHANGELOG.md
# Changelog
All notable changes to this project will be documented in this file.
The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)
and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html).
## [2.0.3] - 2024-04-05
- Add compatiblity with Coq 8.19
- Improve robustness of `QuickChick` by generating truly unique temporary directories
- Resolve extraction warnings:
+ Avoid extraction-opaque-accessed by not depending on `Qed` reflection lemmas.
+ Make `StringOT.compare` and `AsciiOT.compare` `Defined` instead of `Qed`
+ Disable extraction-reserved-identifier
## [2.0.2] - 2024-01-04
## [2.0.1] - 2023-10-08
- Add compatibility with Coq 8.18
## [2.0.0] - 2022-04-13
Major 2.0 Release of QuickChick
- Introduce the notion of `Producer`, a typeclass that abstracts both generators and enumerators.
- No longer support a Monad instance for `G (option A)`.
- bind notation for optional generators can be obtained by importing `BindOptNotation`,
`x <-- c1 ;; c2` with a double arrow, resolving typeclass resolution issues.
- Include support for deriving checkers for inductive relations based on
[PLDI 2022](https://lemonidas.github.io/pdf/ComputingCorrectly.pdf).
`Derive Checker for (P x1 x2 ... xn)`
Defines an instance of the `DecOpt` typeclass that can be access using `??` notation.
- Introduce an enumeration monad `E`, with the same API as generators. Automatic
type-based enumerators for an inductive `T` can be derived using `Derive` notation:
`Derive EnumSized for T.`
- Introduce the `EnumSizedSuchThat` typeclass for constrained enumeration, similar to
`GenSizedSuchThat`. Include support for deriving enumerators for inductive relations based on
[PLDI 2022](https://lemonidas.github.io/pdf/ComputingCorrectly.pdf).
`Derive EnumSizedSuchThat for (fun y => P x1 ... xn y xm ...).`
- Introduce convenient notation for deriving constrained generators:
`Derive Generator for (fun y => P x1 x2 ... y ... xm ...)`
- Introduce a mechanism for [Merging Inductive Relations](https://lemonidas.github.io/pdf/MergingInductiveRelations.pdf).
`Merge P with Q as R.`
- No longer support Coq 8.13 and 8.14
## [1.6.5] - 2022-04-13
- Support Coq 8.17
- No longer support Coq 8.11 and 8.12
## [1.6.4] - 2022-08-14
- Future proofing (internal changes, resolve warnings, keep up with the times)
## [1.6.3] - 2022-05-25
- Add `-use-ocamlfind` to invocations of `ocamlbuild`
- Add `--root=.` to invocations of `dune`, fixing tests using Dune
without a `dune-project` file
## [1.6.2] - 2022-04-08
- Fix Windows compatibility: pass on environment when running test executable
This fixes QuickChick in a Coq Platform "compiled from source" environment. (issue #269)
## [1.6.1] - 2022-03-03
- Add Windows compatibility
- Improve extraction of `randomRNat`, `randomRInt`, `randomRN` by using
`Random.State.full_int` instead of `Random.State.int`.
## [1.6.0]
- Remove all dependency on perl (replaced with cppo (OCaml preprocessor) at compile time; awk at runtime).
- Added more informative error messages when tests fail to compile or throw exceptions.
- Fixed inefficient extraction of Nat arithmetic; this previously caused tests to run in time quadratic in the number of generated test cases.
- Added `RelDec` instance for `eq`.
## [1.5.1]
- Support Coq 8.11 to 8.14.
## [1.5.0]
- Support Coq 8.13.
- No longer support Coq 8.12.
## [1.4.0]
### Added
- Support Coq 8.12.
### Removed
- No longer support Coq 8.11.
## [1.3.2] - 2020-07-11
### Added
- `QCInclude` command to replace `Declare ML Module`.
### Fixed
- Sound extraction of `modn`.
### Changed
- `Decimal.int` no longer depend on an external file for extraction.
## [1.3.1] - 2020-04-06
### Changed
- Add `-cflags -w -3` to `ocamlbuild` for running extracted code.
This silences the warning from using the deprecated `Pervasives` functions
until it's fixed by Coq (Issue #11359).
- Rename `src/unify.ml` to `src/unifyQC.ml` to avoid clashing with the
Coq module of the same name.
### Removed
- Remove our own reliance on `Pervasives`.
This will enforce OCaml >= 4.07 going forward,
but it's marked for deprecation anyways.
### Fixed
- Declare all scopes before using them.
- Fix most remaining warnings during compilation.
- Fix compatibility with ExtLib monad notations.
## [1.3.0] - 2020-03-19
### Added
- Support Coq 8.11.
### Removed
- No longer support Coq 8.10.
## [1.2.1] - 2020-04-09
Backport some fixes in [1.3.1] to Coq 8.10.
These changes are not included in [1.3.0].
### Fixed
- Fix most remaining warnings during compilation.
- Fix compatibility with ExtLib monad notations.
## [1.2.0] - 2020-01-30
### Added
- Support Coq 8.10.
### Removed
- No longer support Coq 8.9.
### Fixed
- `div`, `divn`, and `modn` no longer throw `Division_by_zero` exceptions.
## [1.1.0] - 2019-04-19
### Added
- Support Coq 8.9.
### Removed
- No longer support Coq 8.8.
### Fixed
- Examples use new generator combinators.
- Determine C source files with `*.c` rather than `*c`.
- Derive instances properly regardless of interpretation scope.
### Deprecated
- `-exclude` option in `quickChickTool` is deprecated. Use `-include` instead.
## [1.0.2] - 2018-08-22
### Added
- Functor and Applicative instances for generators.
- Decidable equivalence between `unit`s.
- `-N` option to modify max success in `quickChickTool`.
- Collect labels for discarded tests.
- `quickChickTool` takes Python and Solidity files.
### Changed
- Rename `BasicInterface` to `QuickChickInterface`.
- Rename `Eq` to `Dec_Eq`.
- Separate generator interface from implementation.
### Deprecated
- `elements` is deprecated in favor of `elems_`.
- `oneof` is deprecated in favor of `oneOf_`.
- `frequency` is deprecated in favor of `freq_`.
### Fixed
- Show lists with elements separated by `;` rather than `,`.
## [1.0.1] - 2018-06-13
### Added
- Support Coq 8.8
- `-include` option for `quickChickTool`.
- Highlighted success message for `quickChickTool`.
- Checker combinator `whenFail'`.
- Tagged mutants.
- Line number information of mutants.
### Fixed
- OPAM dependencies.
### Removed
- No longer support Coq 8.7
## [1.0.0] - 2018-04-06
### Added
- OPAM package `coq-quickchick` on [coq-released](https://coq.inria.fr/opam/www/).
[1.6.5]: https://github.com/QuickChick/QuickChick/compare/v1.6.4...v1.6.5
[1.6.4]: https://github.com/QuickChick/QuickChick/compare/v1.6.3...v1.6.4
[1.6.3]: https://github.com/QuickChick/QuickChick/compare/v1.6.2...v1.6.3
[1.6.2]: https://github.com/QuickChick/QuickChick/compare/v1.6.1...v1.6.2
[1.6.1]: https://github.com/QuickChick/QuickChick/compare/v1.6.0...v1.6.1
[1.6.0]: https://github.com/QuickChick/QuickChick/compare/v1.5.1...v1.6.0
[1.5.1]: https://github.com/QuickChick/QuickChick/compare/v1.5.0...v1.5.1
[1.5.0]: https://github.com/QuickChick/QuickChick/compare/v1.4.0...v1.5.0
[1.4.0]: https://github.com/QuickChick/QuickChick/compare/v1.3.2...v1.4.0
[1.3.2]: https://github.com/QuickChick/QuickChick/compare/v1.3.1...v1.3.2
[1.3.1]: https://github.com/QuickChick/QuickChick/compare/v1.3.0...v1.3.1
[1.3.0]: https://github.com/QuickChick/QuickChick/compare/v1.2.1...v1.3.0
[1.2.1]: https://github.com/QuickChick/QuickChick/compare/v1.2.0...v1.2.1
[1.2.0]: https://github.com/QuickChick/QuickChick/compare/v1.1.0...v1.2.0
[1.1.0]: https://github.com/QuickChick/QuickChick/compare/v1.0.2...v1.1.0
[1.0.2]: https://github.com/QuickChick/QuickChick/compare/v1.0.1...v1.0.2
[1.0.1]: https://github.com/QuickChick/QuickChick/compare/v1.0.0...v1.0.1
[1.0.0]: https://github.com/QuickChick/QuickChick/compare/itp-2015-final...v1.0.0