changelog for version 1.6.0 (#1364)

* changelog for version 1.6.0

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
 

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

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
 ```

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

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)