diff --git a/CHANGELOG.md b/CHANGELOG.md index 0a4027f90..9e7d99967 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,82 @@ # Changelog -Latest releases: [[1.5.0] - 2024-10-09](#131---2024-08-09) and [[1.4.0] - 2024-09-24](#140---2024-09-24) +Latest releases: [[1.6.0] - 2024-10-25](#160---2024-10-25) and [[1.5.0] - 2024-10-09](#150---2024-10-09) + +## [1.6.0] - 2024-10-25 + +### Added + +- new directory `theories/topology` with new files: + + `topology.v` + + `bool_topology.v` + + `compact.v` + + `connected.v` + + `matrix_topology.v` + + `nat_topology.v` + + `order_topology.v` + + `product_topology.v` + + `pseudometric_structure.v` + + `subspace_topology.v` + + `supremum_topology.v` + + `topology_structure.v` + + `uniform_structure.v` + + `weak_topology.v` + + `num_topology.v` + + `quotient_topology.v` + +- in `exp.v`: + + lemmas `cvgr_expR`, `cvgn_expR` + +- in `trigo.v`: + + lemmas `derive1_atan`, `lt_atan`, `le_atan`, `cvgy_atan` + +- in `lebesgue_measure.v`: + + lemmas `RintegralZl`, `RintegralZr`, `Rintegral_ge0` + +### Changed + +- The file `topology.v` has been split into several files in the directory + `topology_theory`. Unless stated otherwise, definitions, lemmas, etc. + have been moved without changes. The same import will work as before, + `Require Import topology.v`. + +- in `matrix_topology.v` (new file): + + lemmas `mx_ball_center`, `mx_ball_sym`, `mx_ball_triangle`, `mx_entourage` + are now `Local` + +- in `weak_topology.v` (new file): + + lemmas `wopT`, `wopI`, `wop_bigU` are now `Local` + +- in `supremum_topology.v` (new file): + + lemmas `sup_ent_filter`, `sup_ent_refl`, `sup_ent_inv`, `sup_ent_split`, + `sup_ent_nbhs` are now `Local` + +- The function `map_pair` was moved from `topology.v` to `mathcomp_extra.v`. + +- in `forms.v`: + + notation `'e_` + +- in `lebesgue_integral.v`: + + notation `\x` + +### Renamed + +- in `lebesgue_measure.v`: + + `EFin_measurable_fun` -> `measurable_EFinP` + +### Generalized + +- in `num_topology.v` (new file): + + lemma `nbhs0_lt` generalized from `realType` to `realFieldType` + +### Deprecated + +- in `pseudometric_structure.v` (new file): + + definition `cvg_toi_locally` (use `cvgi_ballP` instead) + +### Removed + +- file `topology.v` (contents now in directory `topology`) ## [1.5.0] - 2024-10-09 diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 460107a35..67bb43c3b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,76 +4,16 @@ ### Added -- new directory `theories/topology` with new files: - + `topology.v` - + `bool_topology.v` - + `compact.v` - + `connected.v` - + `matrix_topology.v` - + `nat_topology.v` - + `order_topology.v` - + `product_topology.v` - + `pseudometric_structure.v` - + `subspace_topology.v` - + `supremum_topology.v` - + `topology_structure.v` - + `uniform_structure.v` - + `weak_topology.v` - + `num_topology.v` - + `quotient_topology.v` -- in `lebesgue_measure.v`: - + lemmas `RintegralZl`, `RintegralZr`, `Rintegral_ge0` - -- in `trigo.v`: - + lemmas `derive1_atan`, `lt_atan`, `le_atan`, `cvgy_atan` - -- in `exp.v`: - + lemmas `cvgr_expR`, `cvgn_expR` - ### Changed -- The file `topology.v` has been split into several files in the directory - `topology_theory`. Unless stated otherwise, definitions, lemmas, etc. - have been moved without changes. The same import will work as before, - `Require Import topology.v`. - -- in `matrix_topology.v` (new file): - + lemmas `mx_ball_center`, `mx_ball_sym`, `mx_ball_triangle`, `mx_entourage` - are now `Local` - -- in `weak_topology.v` (new file): - + lemmas `wopT`, `wopI`, `wop_bigU` are now `Local` - -- in `supremum_topology.v` (new file): - + lemmas `sup_ent_filter`, `sup_ent_refl`, `sup_ent_inv`, `sup_ent_split`, - `sup_ent_nbhs` are now `Local` - -- The function `map_pair` was moved from `topology.v` to `mathcomp_extra.v`. -- in `forms.v`: - + notation `'e_` - -- in `lebesgue_integral.v`: - + notation `\x` - ### Renamed -- in `lebesgue_measure.v`: - + `EFin_measurable_fun` -> `measurable_EFinP` - ### Generalized -- in `num_topology.v` (new file): - + lemma `nbhs0_lt` generalized from `realType` to `realFieldType` - ### Deprecated -- in `pseudometric_structure.v` (new file): - + definition `cvg_toi_locally` (use `cvgi_ballP` instead) - ### Removed -- file `topology.v` (contents now in directory `topology`) - ### Infrastructure ### Misc diff --git a/INSTALL.md b/INSTALL.md index 6ed4a24d7..564c05560 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -48,7 +48,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.1.5.0 +$ opam install coq-mathcomp-analysis.1.6.0 ``` 4. Everytime you want to work in this same context, you need to type ``` diff --git a/Makefile.common b/Makefile.common index 2691bd4fa..0f3998513 100644 --- a/Makefile.common +++ b/Makefile.common @@ -128,14 +128,15 @@ doc-clean: rm -rf _build_doc/ coq2html: + ../coq2html/tools/generate-hierarchy-graph.sh ../coq2html/coq2html \ + -hierarchy-graph hierarchy-graph.dot \ -title "Mathcomp Analysis" \ -d html/ -base mathcomp -Q theories analysis \ -coqlib https://coq.inria.fr/doc/V8.19.2/stdlib/ \ -external https://math-comp.github.io/htmldoc/ mathcomp.ssreflect \ -external https://math-comp.github.io/htmldoc/ mathcomp.algebra \ - classical/*.v classical/*.glob \ - theories/*.v theories/*.glob + $(shell find . -not -path '*/.*' -name "*.v" -or -name "*.glob") coq2html-clean: rm -f */*.glob diff --git a/README.md b/README.md index 9a5d5b8db..b79d4bf46 100644 --- a/README.md +++ b/README.md @@ -84,7 +84,7 @@ We try to preserve backward compatibility as best as we can. Each file is documented in its header in ASCII. -[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_5_0/index.html) (using [`coq2html`](https://github.com/xavierleroy/coq2html)). +[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_6_0/index.html) (using a fork of [`coq2html`](https://github.com/xavierleroy/coq2html)). Overview presentations: - [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018)