From f7cf59c65a057e8ec08ad0b248cb5c2d4dcb8dc2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 24 Jan 2022 23:08:05 +0900 Subject: [PATCH] changelog for version 0.3.13 --- CHANGELOG.md | 50 +++++++++++++++++++++++++++++++++++++- CHANGELOG_UNRELEASED.md | 40 ------------------------------ INSTALL.md | 4 +-- README.md | 2 +- coq-mathcomp-analysis.opam | 2 +- meta.yml | 16 ++++++------ 6 files changed, 61 insertions(+), 53 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7b9929e3b..048049e05 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,54 @@ # Changelog -Last releases: [[0.3.11] - 2021-11-14](#0311---2021-11-14) and [[0.3.12] - 2021-12-29](#0312---2021-12-29) +Last releases: [[0.3.12] - 2021-12-29](#0312---2021-12-29) and [[0.3.13] - 2022-01-24](#0313---2022-01-24) + +## [0.3.13] - 2022-01-24 + +### Added + +- in `topology.v`: + + definitions `kolmogorov_space`, `accessible_space` + + lemmas `accessible_closed_set1`, `accessible_kolmogorov` + + lemma `filter_pair_set` + + definition `prod_topo_apply` + + lemmas `prod_topo_applyE`, `prod_topo_apply_continuous`, `hausdorff_product` +- in `ereal.v`: + + lemmas `lee_pemull`, `lee_nemul`, `lee_pemulr`, `lee_nemulr` + + lemma `fin_numM` + + definition `mule_def`, notation `x *? y` + + lemma `mule_defC` + + notations `\*` in `ereal_scope`, and `ereal_dual_scope` + + lemmas `mule_def_fin`, `mule_def_neq0_infty`, `mule_def_infty_neq0`, `neq0_mule_def` + + notation `\-` in `ereal_scope` and `ereal_dual_scope` + + lemma `fin_numB` + + lemmas `mule_eq_pinfty`, `mule_eq_ninfty` + + lemmas `fine_eq0`, `abse_eq0` +- in `sequences.v`: + + lemmas `ereal_cvgM_gt0_pinfty`, `ereal_cvgM_lt0_pinfty`, `ereal_cvgM_gt0_ninfty`, + `ereal_cvgM_lt0_ninfty`, `ereal_cvgM` + +### Changed + +- in `topology.v`: + + renamed and generalized `setC_subset_set1C` implication to + equivalence `subsetC1` +- in `ereal.v`: + + lemmas `ereal_sup_gt`, `ereal_inf_lt` now use `exists2` +- notation `\*` moved from `realseq.v` to `topology.v` + +### Renamed + +- in `topology.v: + + `hausdorff` -> `hausdorff_space` + +### Removed + +- in `realseq.v`: + + notation `\-` + +### Infrastructure + +- add `.dir-locals.el` for company-coq symbols ## [0.3.12] - 2021-12-29 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 98c7bd921..c1ee5bdc8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,52 +4,12 @@ ### Added -- in `topology.v`: - + definitions `kolmogorov_space`, `accessible_space` - + lemmas `accessible_closed_set1`, `accessible_kolmogorov` -- in `ereal.v`: - + lemmas `lee_pemull`, `lee_nemul`, `lee_pemulr`, `lee_nemulr` -- in `sequences.v`: - + lemmas `ereal_cvgM_gt0_pinfty`, `ereal_cvgM_lt0_pinfty`, `ereal_cvgM_gt0_ninfty`, - `ereal_cvgM_lt0_ninfty`, `ereal_cvgM` -- in `ereal.v`: - + lemma `fin_numM` - + definition `mule_def`, notation `x *? y` - + lemma `mule_defC` - + notations `\*` in `ereal_scope`, and `ereal_dual_scope` -- in `ereal.v`: - + lemmas `mule_def_fin`, `mule_def_neq0_infty`, `mule_def_infty_neq0`, `neq0_mule_def` - + notation `\-` in `ereal_scope` and `ereal_dual_scope` - + lemma `fin_numB` - + lemmas `mule_eq_pinfty`, `mule_eq_ninfty` - + lemmas `fine_eq0`, `abse_eq0` -- in `topology.v`: - + lemma `filter_pair_set` -- in `topology.v`: - + definition `prod_topo_apply` - + lemmas `prod_topo_applyE`, `prod_topo_apply_continuous`, `hausdorff_product` - ### Changed -- in `topology.v`: - + renamed and generalized `setC_subset_set1C` implication to - equivalence `subsetC1` -- in `ereal.v`: - + lemmas `ereal_sup_gt`, `ereal_inf_lt` now use `exists2` -- notation `\*` moved from `realseq.v` to `topology.v` - ### Renamed -- in `topology.v: - + `hausdorff` -> `hausdorff_space` - ### Removed -- in `realseq.v`: - + notation `\-` - ### Infrastructure -- add `.dir-locals.el` for company-coq symbols - ### Misc diff --git a/INSTALL.md b/INSTALL.md index 3cfc98f47..d3e6f62e1 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -5,7 +5,7 @@ - [The Coq Proof Assistant version ≥ 8.12](https://coq.inria.fr) - [Mathematical Components version ≥ 1.12.0](https://github.com/math-comp/math-comp) - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap) -- [Hierarchy builder version >= 0.10.0](https://github.com/math-comp/hierarchy-builder) +- [Hierarchy builder version >= 1.0.0](https://github.com/math-comp/hierarchy-builder) These requirements can be installed in a custom way, or through [opam](https://opam.ocaml.org/) (the recommended way) using @@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.0.3.12 +$ opam install coq-mathcomp-analysis.0.3.13 ``` 4. Everytime you want to work in this same context, you need to type ``` diff --git a/README.md b/README.md index 3873e8510..f3c10555a 100644 --- a/README.md +++ b/README.md @@ -46,7 +46,7 @@ the Coq proof-assistant and using the Mathematical Components library. - [MathComp field 1.12 or later](https://math-comp.github.io) - [MathComp finmap 1.5.1](https://github.com/math-comp/finmap) - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough) - - [Hierarchy Builder >= 0.10.0](https://github.com/math-comp/hierarchy-builder) + - [Hierarchy Builder >= 1.0.0](https://github.com/math-comp/hierarchy-builder) - Coq namespace: `mathcomp.analysis` - Related publication(s): - [Formalization Techniques for Asymptotic Reasoning in Classical Analysis](https://jfr.unibo.it/article/view/8124) doi:[10.6092/issn.1972-5787/8124](https://doi.org/10.6092/issn.1972-5787/8124) diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index 5f56c46d6..4d67e78a8 100644 --- a/coq-mathcomp-analysis.opam +++ b/coq-mathcomp-analysis.opam @@ -26,7 +26,7 @@ depends: [ "coq-mathcomp-field" { (>= "1.12.0" & < "1.15~") | (= "dev") } "coq-mathcomp-finmap" { (>= "1.5.1" & < "1.6~") | (= "dev") } "coq-mathcomp-bigenough" { (>= "1.0.0") } - "coq-hierarchy-builder" { (>= "0.10.0") } + "coq-hierarchy-builder" { (>= "1.0.0") } ] tags: [ diff --git a/meta.yml b/meta.yml index 38d0a849a..1fdd5964d 100644 --- a/meta.yml +++ b/meta.yml @@ -63,7 +63,7 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '1.13.0-coq-8.15' repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-dev' +- version: '1.14.0-coq-dev' repo: 'mathcomp/mathcomp' - version: 'coq-8.13' repo: 'mathcomp/mathcomp-dev' @@ -75,27 +75,27 @@ tested_coq_opam_versions: dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "1.12.0" & < "1.14~") | (= "dev") }' + version: '{ (>= "1.12.0" & < "1.15~") | (= "dev") }' description: |- [MathComp ssreflect 1.12 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-fingroup - version: '{ (>= "1.12.0" & < "1.14~") | (= "dev") }' + version: '{ (>= "1.12.0" & < "1.15~") | (= "dev") }' description: |- [MathComp fingroup 1.12 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra - version: '{ (>= "1.12.0" & < "1.14~") | (= "dev") }' + version: '{ (>= "1.12.0" & < "1.15~") | (= "dev") }' description: |- [MathComp algebra 1.12 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-solvable - version: '{ (>= "1.12.0" & < "1.14~") | (= "dev") }' + version: '{ (>= "1.12.0" & < "1.15~") | (= "dev") }' description: |- [MathComp solvable 1.12 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-field - version: '{ (>= "1.12.0" & < "1.14~") | (= "dev") }' + version: '{ (>= "1.12.0" & < "1.15~") | (= "dev") }' description: |- [MathComp field 1.12 or later](https://math-comp.github.io) - opam: @@ -110,9 +110,9 @@ dependencies: [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough) - opam: name: coq-hierarchy-builder - version: '{ (>= "0.10.0") }' + version: '{ (>= "1.0.0") }' description: |- - [Hierarchy Builder >= 0.10.0](https://github.com/math-comp/hierarchy-builder) + [Hierarchy Builder >= 1.0.0](https://github.com/math-comp/hierarchy-builder) namespace: mathcomp.analysis keywords: