-
Notifications
You must be signed in to change notification settings - Fork 43
2020 12 17 Meeting
affeldt-aist edited this page Dec 18, 2020
·
2 revisions
Participants: Marie, Kazuhiko, Pierre-Yves, Cyril, Reynald
- PR 283
- still need to split lemmas in two
- add lemmas "interior of ball is open" and "interior of closed ball is ball"?
- for the time being, do not add any
open_ball
definition tonormedtype.v
- maybe later if needed
- should be done by next month
- TODO: put in the documentation
- NB: balls from pseudometric types are not necessarily open
- PR 305
- close but don't remove: keep as documentation
- PR 275
- TODO: add changelog entries
- drop support for versions before MathComp 1.12
- TODO: release mathcomp-analysis 0.3.5 once merged
- TODO: add changelog entries
- NB: hierarchy-builder requires Coq 8.11
- TODO: issue to add test with Coq 8.13
- summary of the new interval library
- bounds are now +oo and -oo, "left of x" and "right of x" (meaning open or closed depending on which extremity we are)
- NB: another order of intervals: by their middle point (x+1/x-1 for half-open intervals)
- PR 294
- no major issue, should be done by next month
- PR 309
-
predeqP
should be should be likepredeqE
but with<=>
instead of=
- what is
predeqP
right now should be calledseteqP
-
- PR 205
- could be merged by next month
-
^o
only used on intermediate structures (as in https://github.com/math-comp/analysis/blob/b3a67378443dc35cd788b02dc384a5f3a4949935/theories/normedtype.v#L1258)- topological structure defined on any numField as a clone of the regular structure on algebra
- NB: remaining
^o
insequences.v
- NB:
derive.v
still slow to compile, this is because of type classes- part of the solution could be to lock the definition mentioned in issue 118 with a module
- PR 302 New nix
- refactoring of nix files for analysis to work with the future version of Coq packages that is under refactoring (see this PR)
- using MathComp-Analysis as a benchmark
- PR 306 Generated nix CI test
- generated using PR 302
- to be put in draft mode but should be merged as some point
- meta discussion about simplification of filters
- this ultimately calls for an extension of hierarchy-builder
- alternative approach (besides the existing PRs): duplicate the hiearchy of algebraic predicates https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssralg.v#L3526-L3752
- TODO: try...