Hierarchy builder merged #1161
Merged
Hierarchy builder merged #1161
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Co-authored-by: Cyril Cohen <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
* sumeN, renaming, generalization
* quotient topology * docs * trying to fix build * cleaning up proof * more general quotients * docs * trying to fix build * nitpicks * quotType alias * fix changelog * fixing changelog again --------- Co-authored-by: Reynald Affeldt <[email protected]>
* swapping machines * proof of open map * hausdorff accessible * weak products equivalent * changelog * strengthen join_product_weak * cleaning up proofs * typos * adding local notations for proof legibility * merging product stuff * fixing changelog * specialized conjunctions to use less brackets and splits * fixing grammar * fix changelog * fixing build * more build fixes --------- Co-authored-by: Reynald Affeldt <[email protected]>
- use cover in finSubCover - use [set: ] instead of @Sett - use shortcut notation for set comprehension
* proving sups preserve countable ent * proof going through * unused proofs * linting * metric implies countable uniformity * fixing changelog * linting * metric for products * linting * fixing docs * use %:pos * fixing changelog * fix changelog * nitpicking --------- Co-authored-by: Reynald Affeldt <[email protected]>
* simplifying clopen proofs * clopen separations * adding docs * linting. * nitpicks, trailing spaces, lint --------- Co-authored-by: Reynald Affeldt <[email protected]>
- fixes math-comp#846 - fixes math-comp#845
* cluster1 proof * updating changelog * Update theories/topology.v Co-authored-by: affeldt-aist <[email protected]> * Update theories/topology.v Co-authored-by: affeldt-aist <[email protected]> * change to signature of compact_near_coveringP * no need to name intermediate hypo --------- Co-authored-by: affeldt-aist <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
* fixes - fixes math-comp#828 - fixes math-comp#835 - fixes math-comp#838
* add a type for finite measures - s-finite measures from branch kernels - add subprobabilities - dirac instance of probability - rm finite_measure - renaming - minor fix
Co-authored-by: Quentin Vermande <[email protected]>
- a few pinfty/ninfty -> y/Ny renamings
* Add itv.v Taking inspiration on signed.v, replacing sign by intervals. * Add interval multiplication * Add hints to automatically solve _ <= 1 goals * Test to see if usable as a replacement for prob * use notation from mathcomp_extra.v * changelog and rm redundant code * prefix duplicated identifiers --------- Co-authored-by: Reynald Affeldt <[email protected]>
- fixes math-comp#866 - fixes math-comp#867 - fixes math-comp#868
* test a few files
* changelog for version 0.6.7 * upd README
* generalizations
* curry/uncurry of continuous functions * compact-open topology working * removing regular in favor of regular_space --------- Co-authored-by: Reynald Affeldt <[email protected]>
Co-authored-by: Georges Gonthier <[email protected]>
* total variation proofs - increasing implies BV - splitting partitions - right/left continuity of TV - define variation with path - adding monotone variation - variation using prev and next --------- Co-authored-by: Reynald Affeldt <[email protected]>
* changelog for version 0.7.0
|
NB:
|
|
I guess this is just to run CI and not intended to be merged? In which case it should be a draft PR, to avoid merging it inadvertently. |
You can probably squash it into the merge commit. |
|
We'll have to add 8.19 to the CI, but this can be done after merging #951 |
|
I have completed a changelog but you'd better take a look @proux01 @CohenCyril @zstone1 . It just remains to update the documentation which should be less boring and you're en route to the next release. |
|
Honestly, I trust you here. At first glance it looks reasonable but I don't have the patience to carefully review the changelog (the remaining is ok). So as far as I'm concerned, you can push this on master. |
|
The last commit contains an update of the doc. If you are ok with the changelog (@proux01 seems to be) and with the doc update (that may be a good timing to add things you care about), we can do a release of MathComp-Analysis 1.0 before friday. |
affeldt-aist
force-pushed
the
hierarchy-builder_merged
branch
from
9be4a7e to
bfcfe58
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Motivation for this change
This PR is the result of merging the branch
hierarchy-builderinto themastercorresponding to tag0.7.0.Things done/to do
CHANGELOG_UNRELEASED.mdCompatibility with MathComp 2.0
TODO: HB portto make sure someone ports this PR tothe
hierarchy-builderbranch or I already opened an issue or PR (please cross reference).Automatic note to reviewers
Read this Checklist and put a milestone if possible.