-
Notifications
You must be signed in to change notification settings - Fork 43
2024 02 09 Meeting
affeldt-aist edited this page Feb 12, 2024
·
3 revisions
Participants: Reynald, Quentin, Takafumi, Alessandro, Pierre, Zachary
-
Announcements:
- Mathcomp-Analysis 0.7.0 has been released
- btw, any clue about issue #1169 ?
- 0.7.0 seems to be not compatible with HB 1.6.0/Coq 8.17.1
- how did this escape our testings?
- might be broken with 1.6.0
- TODO(rei): try HB 1.6.0 with Coq 8.19.0 to confirm
- MathComp-Analysis 1.0.0 has been released
- feedback is welcome
- in particular about the https://github.com/math-comp/analysis/blob/master/README.md
- and the documentation generated by coq2html
- Pierre: let's think of a test suite to check the stability of coq2html and put in the CI
- TODO: check the status with Xavier
- Reynald: we have still bugs to fix
- Alessandro already found an issue: https://github.com/yoshihiro503/coq2html/issues/3
- Mathcomp-Analysis 0.7.0 has been released
-
issue triaging:
- about exports and
contra.v
issue #1157- Pierre wanted to remove canonicals to avoid us failing to add new ones when needed
- Pierre failed to use contra and didn't open the PR
- Quentin: Zorn to be PRed has a use-case
- it is a more general version that the already available one
- no problem if it is a duplicate for now because we will surely come back to it
- follow-up by Pierre just after the meeting: https://github.com/math-comp/analysis/pull/1172
- about the infamous monotonous issue #1133
- monotonic in US English
- monotonic with
mono
is strict- pbms: this is contrary to Zachary's intuition, the constant function is not monotonic
- => the definition should be
homo
- in some cases only should we need
mono
-
homo
would be large according to wikipedia - TODO: Reynald to try a PR
- move
nondecreasing*
, etc. inrealfun.v
earlier in the hierarchy of files - introduce
nondecreasing_on
,nonincreasing_on
, etc.- see also
order_morphism
andle_mono
inorder.v
- see also
- progress on issue #1126 ?
- Takafumi in charge
- idea: use https://mathscinet.ams.org/msnhtml/msc2020.pdf
- list the library of MathComp with links to the classification (next to the opam packages)
- TODO: PR to put them at the top of the headers?
- opam info should also display this information
- time to address the simplification of the filter layer from the long-standing issues?
- issues https://github.com/math-comp/analysis/pull/282 and https://github.com/math-comp/analysis/pull/300
- Zachary: the type class for filters are used in basically every lemma (ultrafiler is not often used), filters are used by near, most instances are in topology
- Pierre: similar mechanism in
derive.v
to prove derivability - test packed classes as a replacement?
- TODO: ping Cyril
- about exports and
-
PR triaging:
- splitting
topology.v
PR #1166- does it call for version 1.1.0?
- yes because it is a breaking change (new file and removal the canonical topology on functions)
-
mulr_rev
PR #1122- already discussed during the last meeting
- failed to figure out how to take advantage of
R^c
from MathComp- i.e., couldn't get rid of the identifier
mulr_rev
in favor ofGRing.mul R^c
- i.e., couldn't get rid of the identifier
- TODO(rei): try again with MathComp 2 and then discuss it again
- Pierre: ask Kazuhiko because it looks like the dual order experiment
- report on issue #965
- recently merged: total_variation PR #1118
- to be merged: LDT PR #1065
- Reynald asking for external input
- in particular, is it ok to use
locally_integrable
,integrable
w.r.t.setT
and not care about generic versions? - Zachary: yes for lemmas about integrability since we can always recast by multiplying with a characteristic function
- e.g.: FTC1 : patchable by multiplying
f
by a characteristic function - same for
locally_integrable
- for continuity it matters more
- splitting
-
Questions from issues:
-
sigma_finiteP
issue #1080- prove the reverse direction and then the suffix will make sense!
-
expRMm
issue #1094-
M
is multiplication - should it be
n
? maybe just a typo? - TODO: ask Laurent
-
- about
patch
issue #1100- Zachary: it depends on the lemma, this is case by case
- in a textbook specialized for the real it would be the same
- but
patch
is bit more general - to prove a bound `patchP might be nicer
-
+
vs.\+
issue #1077- the first one is useful to write from right to left
- the second one looks more generic
- TODO: Alessandro will try again
- looking like
caddE
for charges that we got rid of (but here the proof is less trivial)
-
-
Zachary: why do we need pointed on topology?
- Reynald referring to the experiment of removing pointed from
measurableType
see https://github.com/math-comp/analysis/issues/796 - Zachary to try to remove the hypothesis and introduce
npToplogy
- Reynald referring to the experiment of removing pointed from