Zulip Chat Archive

Stream: mathlib4

Topic: Technical Debt Counters

github mathlib4 bot (Jun 10 2024 at 04:08):

Number Type
7371 porting notes
51 backwards compatibility flags
77 adaptation notes
359 disabled simpNF lints
201 disabled deprecation lints
1930 erw
961 documentation nolint entries
30 missing module docstrings
93 large files
151 non-test files with autoImplicit true
41 Init files

5323 total LoC in 'Init' files

Michael Rothgang (Jun 10 2024 at 06:23):

For the statistic nerds (like me), let me note that the count of adaptation notes is too low --- as the master branch contains about 60 occurrences of the string "Adaptation note" (which should be the command #adaptation_note instead; only the latter is counted by this bot). A fix will merge soon.

Yaël Dillies (Jun 10 2024 at 07:10):

How is nolint simpNF "technical debt"? This is just that simpNF doesn't know about dsimp lemmas

Joël Riou (Jun 10 2024 at 07:25):

Yaël Dillies said:

How is nolint simpNF "technical debt"? This is just that simpNF doesn't know about dsimp lemmas

simpNF does know about dsimp lemmas, cf. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/attribute.20simp_NF_my_lemma.3F

Kim Morrison (Jun 10 2024 at 11:42):

Perhaps @Yaël Dillies intends to say that the simpNF linter should not pay any attention to dsimp lemmas. I would want to hear a persuasive argument there.

Yaël Dillies (Jun 10 2024 at 15:55):

I am saying that simping the LHS of dsimp lemmas is not fair game. One should be dsimping the LHS instead.

Yaël Dillies (Jun 10 2024 at 15:58):

The point of the linter (as I understand it) is to spot simp lemmas foo that never get to apply in simp because another simp lemma bar always applies (as in simp [-foo] simplifies the LHS of foo using bar). But if foo is a dsimp lemma and bar is not, then foo does get to apply in dsimp (as in dsimp [-foo] does not simplify the LHS of foo using bar)

Yaël Dillies (Jun 10 2024 at 16:02):

In practice, there is an order of magnitude less dsimp lemmas than there are simp lemmas, so one could simply disable simpNF on dsimp lemmas and everything would probably be fine. But the more principled approach would be to disable simpNF on dsimp lemmas AND run a new dsimpNF linter on them that tries to simplify the LHS of each dsimp lemma using dsimp (or make simpNF do that step too, doesn't really matter if it's one or two linters)

Johan Commelin (Jun 11 2024 at 03:56):

Agreed, but these nolints are still an artifact of the issue that you point out. So it is still some form of technical debt.

Johan Commelin (Jun 11 2024 at 07:21):

So I think this is basically a bug in the simpNF linter. The linter checks if the LHS of a simp-lemma is in simp normal form, by trying to reduce it with all available simp-lemmas in the standard simp set. But if a lemma is proven by rfl (et. al) then it is actually a dsimp-lemma. And so the linter should really be checking if the LHS is in dsimp normal form.
Lean determines whether a lemma is a dsimp-lemma using Lean.Meta.isRflTheorem (declName : Name) : CoreM Bool and so the simpNF linter should do the same thing.
The simpNF linter is in Batteries/Tactic/Lint/Simp.lean.

Does anyone feel like taking this on?

Yaël Dillies (Jun 11 2024 at 08:33):

Johan Commelin said:

Agreed, but these nolints are still an artifact of the issue that you point out. So it is still some form of technical debt.

Yes but the counter here makes it feel like the solution is to unsimp those lemmas. The debt is in the linter, not the lemmas

Johan Commelin (Jun 12 2024 at 06:09):

Fixed in

chore(Tactic/Lint/Simp): make simpNF linter dsimp-aware batteries#839

Eric Wieser (Jun 12 2024 at 10:35):

Note that without lean4#2679 (which restores some lean 3 community behavior), there are lemmas that should morally be dsimp (like docs#Set.mem_setOf) but currently are not considered so; and as such, we may still want @[nolint simpNF] -- will be dsimp after lean4#2679.

Johan Commelin (Jun 12 2024 at 11:56):

Sure, I'm not claiming that this linter-fix will allow us to remove all nolint simpNFs. But I hope we'll be able to remove a lot of them :smile:

Utensil Song (Jun 12 2024 at 12:05):

Could these Technical Debts contain links to a guide to fix them? Assuming these are simple to medium level tasks.

Johan Commelin (Jun 12 2024 at 13:28):

I think that varies a lot...

Ruben Van de Velde (Jun 12 2024 at 15:57):

We're missing a counter for deprecated declarations without a date, since those seem to keep popping up

Damiano Testa (Jun 12 2024 at 16:35):

How does this look for catching a bunch of deprecated but not since?

git grep "@\[.*deprecated" | grep -v 'deprecated .*(since := "'

Damiano Testa (Jun 12 2024 at 16:36):

(It reports that there are 225 such matches, though some are comments, others are actually legitimate uses.)

Damiano Testa (Jun 12 2024 at 16:38):

(note that deprecated can happen after more attributes in @[...] and it need not be contiguous to since -- nor in fact on the same line!)

Damiano Testa (Jun 12 2024 at 16:55):

#13778

Damiano Testa (Jun 12 2024 at 16:56):

Maybe the PR summary could also add a line in case the count is increased by a PR.

Johan Commelin (Jun 12 2024 at 19:57):

Can't we just have a Lean linter that rejects deprecated without since in mathlib?

Johan Commelin (Jun 12 2024 at 19:58):

That seems easier than keeping track of them afterwards. That would be "mopping while the tap is open" (pardon my Dutch)

Damiano Testa (Jun 12 2024 at 20:12):

Sure, that would be probably very easy to write. I will look into it!

Damiano Testa (Jun 12 2024 at 20:13):

However, the linter would not know which deprecate are new and which ones are old, unless it does quite a bit of git-digging.

Damiano Testa (Jun 12 2024 at 20:14):

So, together with the linter, there is also the need to remove the currently present "since-less" deprecate.

Damiano Testa (Jun 12 2024 at 20:15):

Would it be acceptable to put a blanket "today's date", where "today" refers to when they get updated?

Damiano Testa (Jun 12 2024 at 20:24):

There is also the solution of making since a mandatory part of the syntax.

Michael Rothgang (Jun 12 2024 at 20:36):

Isn't #13678 such a linter/how does this differ from what you had in mind?

Michael Rothgang (Jun 12 2024 at 20:36):

#13723 is the latest PR adding more dates/formatting existing ones.

Damiano Testa (Jun 12 2024 at 20:45):

Oh, I simply had not seen that PR! I had in mind a syntax linter, though, rather than an environment linter, so you would get a live warning.

Damiano Testa (Jun 12 2024 at 20:46):

The alternative, would be to elaborate the syntax for deprecated without the since to a logWarning (plus the actual deprecation).

Damiano Testa (Jun 12 2024 at 20:47):

But anyway this was before you mentioned Yury's linter.

Notification Bot (Jun 13 2024 at 06:56):

7 messages were moved from this topic to #mathlib4 > dsimpNF by Johan Commelin.

Michael Rothgang (Jun 13 2024 at 07:51):

Should this script also count occurrences of set_option tactic.skipAssignedInstances or set_option simprocs false, similarly to how it counts occurrences of any backward. option?

Damiano Testa (Jun 13 2024 at 07:56):

Btw, the syntax linter for "deprecated-no-since" reports 157 missing "no-since" in mathlib

Damiano Testa (Jun 13 2024 at 08:07):

In case someone wants to take a look, the command below takes you to the relevant position for each failure.

NoSinces

edklencl (Jun 13 2024 at 08:43):

https://lean4daydayup.zulipchat.com/#narrow/stream/435784-.E6.9C.89.E4.BB.B7.E5.80.BC.E7.9A.84.E5.AD.A6.E4.B9.A0.E8.B5.84.E6.BA.90.E5.90.88.E9.9B.86/topic/.E4.B8.80.E4.BA.9B.E6.B2.A1.E6.9C.89.E4.BB.B7.E5.80.BC.E7.9A.84.E5.B0.8F.E6.96.87.E7.AB.A0

Damiano Testa (Jun 13 2024 at 08:53):

#13793 is now testing the automatic addition of since: ideally, it builds mathlib, collects the linter warnings, performs all the substitutions and runs lake build again. The second time, lake build will fail on warnings.

Damiano Testa (Jun 13 2024 at 08:53):

Let's see where it gets stumped! :smile:

Damiano Testa (Jun 13 2024 at 10:21):

The sequence lake build, auto-add since, lake build was successful! After a first noisy build of mathlib, the second one was quiet.

CI failed due to long lines and the fact that I forgot to silence the test for the linter using #guard_msgs.

Damiano Testa (Jun 13 2024 at 10:22):

The auto-fix step reported 157 modifications across 54 files, all successful.

Mario Carneiro (Jun 14 2024 at 00:44):

Johan Commelin said:

Fixed in

chore(Tactic/Lint/Simp): make simpNF linter dsimp-aware batteries#839

@Johan Commelin @Kim Morrison did I miss some explanation for batteries#841 ? Why was this PR reverted?

Kim Morrison (Jun 14 2024 at 00:45):

I suggested reverting in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/dsimpNF/near/444369482, so that we can get the Mathlib fixes lined up ahead of time.

Kim Morrison (Jun 14 2024 at 00:46):

(I really needed to get nightly-testing working again, and this was going to become a blocker.)

Johan Commelin (Jun 14 2024 at 04:56):

It is certainly planned to re-revert it in the next few days (-;

Michael Rothgang (Jun 15 2024 at 10:29):

Michael Rothgang said:

tactic.skipAssignedInstances

Created #13851 to do this.

github mathlib4 bot (Jun 17 2024 at 04:08):

Number Type
7327 porting notes
51 backwards compatibility flags
90 skipAssignedInstances flags
141 adaptation notes
365 disabled simpNF lints
164 disabled deprecation lints
1935 erw
961 documentation nolint entries
30 missing module docstrings
95 large files
147 non-test files with autoImplicit true
11 deprecations without a date
41 Init files

5326 total LoC in 'Init' files

Kim Morrison (Jun 17 2024 at 05:13):

Next upgrade: show the diffs since last post!

Johan Commelin (Jun 17 2024 at 05:15):

:thumbs_up: but it requires maintaining some state :thinking:

Damiano Testa (Jun 17 2024 at 05:53):

Not necessarily: we can probably checkout the previous week's master and rerun the command.

Damiano Testa (Jun 17 2024 at 06:58):

With respect to last week, this is the only change:

| 7327  (-36)| porting notes |

Kim Morrison (Jun 17 2024 at 07:20):

Alternatively, scrape the last message from zulip?

Kim Morrison (Jun 17 2024 at 07:20):

(i.e. let Zulip maintain state)

Damiano Testa (Jun 17 2024 at 07:23):

If we do it with the git-history, then we can also do comparisons between different commits, not necessarily the lastest diff... Let me look into it!

Michael Rothgang (Jun 17 2024 at 08:06):

Damiano Testa said:

With respect to last week, this is the only change:

| 7327  (-36)| porting notes |

I also see differences in adaptation notes (some notes got labeled properly), disabled simpNF and deprecation lints, large files (no idea where that's coming from) and autoImplicit (four down)...

Damiano Testa (Jun 17 2024 at 08:20):

Michael, yes, I am not sure what happened there. I think that, like for the PR summaries, these posts should include the commit hashes: this would make the diff's reproducible more easily.

Damiano Testa (Jun 17 2024 at 09:01):

Let's see if this looks better!

Number Change Type
7330 -29 porting notes
52 0 backwards compatibility flags
91 1 skipAssignedInstances flags
142 -1 adaptation notes
366 6 disabled simpNF lints
165 -16 disabled deprecation lints
1935 5 erw
961 0 documentation nolint entries
30 0 missing module docstrings
95 2 large files
148 -4 non-test files with autoImplicit true
11 -318 deprecations without a date
41 0 Init files
5326 -3 total LoC in 'Init' files

'Init' file by file

Commits:
current 77e1ea0a339a4663eced9cacc3a46eb45f967b51
old f87721ad1ba9a6057d502b060a87778fb8186dbd

Michael Rothgang (Jun 17 2024 at 09:51):

I like the format! How about "current number" as the header?

Michael Rothgang (Jun 17 2024 at 09:52):

(In case others may wonder as well: the commits from this diff are not the ones the bot posted here - so the numbers don't match.)

Michael Rothgang (Jun 17 2024 at 09:57):

One more thought: I guess "deprecations without a date" can be removed now, since we have a linter against it - all remaining matches are false positives. Hoorah! :tada:

Damiano Testa (Jun 17 2024 at 10:59):

#13892, where I also removed the no since line, as suggested.

Damiano Testa (Jun 17 2024 at 11:57):

By the way, the default behaviour is that you run it and it compares master with "master from one week ago". However, if you provide two commits as reference, it will take the first as the commit where the numbers are computed and will report the difference with whatever numbers would come out of the second commit.

Michael Rothgang (Jun 17 2024 at 13:18):

Damiano Testa said:

#13892, where I also removed the no since line, as suggested.

I'm not an awk expert; a look on this would be helpful!

github mathlib4 bot (Jun 24 2024 at 04:05):

Current number Change Type
7007 0 porting notes
51 0 backwards compatibility flags
90 0 skipAssignedInstances flags
149 0 adaptation notes
278 0 disabled simpNF lints
162 0 disabled deprecation lints
1938 0 erw
961 0 documentation nolint entries
30 0 missing module docstrings
94 0 large files
147 0 non-test files with autoImplicit true
41 0 Init files
5326 0 total LoC in Init files

Changed 'Init' lines by file

Current commit 62fdad82b2
Reference commit 62fdad82b2

Kim Morrison (Jun 24 2024 at 05:11):

Could we please have maxHeartbeats in this table?

Kim Morrison (Jun 24 2024 at 05:24):

  • Remove about 75% of backward compatibility flags in #14064
  • Remove most set_option.skipAssignedInstances #14073

Damiano Testa (Jun 24 2024 at 06:06):

Also, the change column should be fixed...

Damiano Testa (Jun 24 2024 at 06:07):

I'm not sure that I can look into this quickly, though.

Damiano Testa (Jun 24 2024 at 06:15):

I just ran the code on my computer and the change column at least does not only have 0:

Current number Change Type
7007 -320 porting notes
51 0 backwards compatibility flags
90 0 skipAssignedInstances flags
149 8 adaptation notes
278 -87 disabled simpNF lints
162 -2 disabled deprecation lints
1938 7 erw
30 1 maxHeartBeats modifications
961 0 documentation nolint entries
30 0 missing module docstrings
94 -1 large files
147 0 non-test files with autoImplicit true
41 0 Init files
5326 0 total LoC in Init files

Changed 'Init' lines by file

Current commit 9d94f1d86c
Reference commit 9cbd6ff101

Damiano Testa (Jun 24 2024 at 06:23):

I edited the above to include the heartbeats: #14075.

Damiano Testa (Jun 24 2024 at 06:44):

I also think that the Change issue is that CI was using a shallow clone: #14076.

Michael Rothgang (Jun 24 2024 at 08:30):

Kim Morrison said:

  • Remove about 75% of backward compatibility flags in #14064
  • Remove most set_option.skipAssignedInstances #14073

Did you see #13704, which does very similar things to #14073? I benchmarked that one and removed the changes which were actively slowing things down.

Kim Morrison (Jun 24 2024 at 08:32):

Sigh, I didn't see this, the #queue is impossibly long and I don't look at it anymore. :-(

Kim Morrison (Jun 24 2024 at 08:32):

I hit :merge: on #13704. Shall I just close #14073?

Jeremy Tan (Jun 24 2024 at 08:32):

Yes

Kim Morrison (Jun 24 2024 at 08:34):

@Jeremy Tan, your answer is not helpful to me.

Kim Morrison (Jun 24 2024 at 08:35):

Matthew has hit merge on #14073 in the meantime ...

Matthew Ballard (Jun 24 2024 at 08:36):

I've called off bors and delegated

Kim Morrison (Jun 24 2024 at 08:36):

For "technical debt" type PRs, I will very happily merge them quickly if notified about them (but I won't see them if they aren't mentioned on zulip, tbh). Two weeks is far too long for something like this is wait.

Michael Rothgang (Jun 24 2024 at 08:36):

I was about to write: I can check if #14073 has any changes left after the other one is merged. (Certainly this week; no promises on a quicker response - I don't have much Lean time right now.)

Michael Rothgang (Jun 24 2024 at 08:37):

Kim Morrison said:

For "technical debt" type PRs, I will very happily merge them quickly if notified about them (but I won't see them if they aren't mentioned on zulip, tbh). Two weeks is far too long for something like this is wait.

I was about to ask: is there something I can change about this - thanks for anticipating my question! So I will aggressively mention tech debt PRs in there, from now on; that works for me.

Michael Rothgang (Jun 24 2024 at 08:40):

So... do the following PRs count as technical debt? If no, feel free to ignore these :-)

  • #13869 re-distributes fun_prop tags; @Tomas Skrivan already approved
  • #14059 rewrites another Python style linter in Lean

Jeremy Tan (Jun 24 2024 at 08:41):

I'll approve #14059

Kim Morrison (Jun 24 2024 at 08:43):

Merged both now.

Michael Rothgang (Jun 24 2024 at 08:43):

Thanks for the fast reviews! :heart:

Michael Rothgang (Jun 24 2024 at 12:55):

I wonder if there are further unnessary set_options left (unless Kim looked at them all). @Damiano Testa Would you like to run the most recent incarnation of #13653 to check? (Presumably, the number of hits will be small, so even just the linter would suffice.)

Michael Rothgang (Jun 24 2024 at 12:57):

Kim Morrison said:

Sigh, I didn't see this, the #queue is impossibly long and I don't look at it anymore. :-(

Another thought (perhaps this should move to a different thread, such as "avoiding duplicate work cleaning up technical debt"..) There is a "tech debt" label: is checking all PRs labelled such an option, instead of the queue?

Michael Rothgang (Jun 24 2024 at 12:57):

I'm happy to help ensure that PRs are labelled such as appropriate.

Shreyas Srinivas (Jun 24 2024 at 13:50):

are unnamespaced defs and theorems "technical debt"?

Michael Rothgang (Jun 24 2024 at 15:02):

#14094 regenerates the list of style exceptions: includes a reordering as a by-product of the rewrite in Lean. As we're measuring tech debt using this, we may as well keep it up to date.

Jireh Loreaux (Jun 24 2024 at 19:04):

Shreyas Srinivas said:

are unnamespaced defs and theorems "technical debt"?

We don't currently consider those as such (We = most maintainers, with some exceptions). This constitutes most of Mathlib.

Damiano Testa (Jun 24 2024 at 20:36):

Michael Rothgang said:

I wonder if there are further unnessary set_options left (unless Kim looked at them all). Damiano Testa Would you like to run the most recent incarnation of #13653 to check? (Presumably, the number of hits will be small, so even just the linter would suffice.)

Michael, I merged master and re-ran the linter: there are a couple of set_options that are flagged as unnecessary, but some (especially the maxHeartbeats ones) may be false positives.

Damiano Testa (Jun 24 2024 at 20:57):

#14103

I think that the other flags are false positives.

Michael Rothgang (Jun 30 2024 at 16:52):

#14298, #14299, #14300 and #14301 each are short PRs removing autoImplicit from a few files. Each PR deals with a single directory.

Michael Rothgang (Jun 30 2024 at 21:27):

#14304 removes almost all occurences from Order

Eric Wieser (Jun 30 2024 at 22:40):

I merged most of those (before seeing this message)

github mathlib4 bot (Jul 01 2024 at 04:06):

Current number Change Type
6928 -79 porting notes
10 -41 backwards compatibility flags
40 -50 skipAssignedInstances flags
153 4 adaptation notes
290 12 disabled simpNF lints
169 7 disabled deprecation lints
1947 9 erw
26 -4 maxHeartBeats modifications
958 -3 documentation nolint entries
29 -1 missing module docstrings
95 1 large files
134 -13 non-test files with autoImplicit true
41 0 Init files
5310 -16 total LoC in Init files

Changed 'Init' lines by file

Current commit f5c3f06aa7
Reference commit b1a314186f

Damiano Testa (Jul 01 2024 at 06:28):

The Change fix worked!

Damiano Testa (Jul 01 2024 at 06:42):

A small wrinkle is that the current reference commit does not match the past current commit. If I remember the script, they should be commits from the day, though.

Michael Rothgang (Jul 03 2024 at 12:28):

Eric Wieser said:

I merged most of those (before seeing this message)

Thanks for the reviews; the above PRs are all merged. #14354 (FieldTheory) and #14355 (Mathlib/Init) clean two more folders.

github mathlib4 bot (Jul 08 2024 at 04:06):

Current number Change Type
6853 -75 porting notes
10 0 backwards compatibility flags
40 0 skipAssignedInstances flags
137 -16 adaptation notes
287 -3 disabled simpNF lints
167 -2 disabled deprecation lints
1939 -8 erw
26 0 maxHeartBeats modifications
958 0 documentation nolint entries
29 0 missing module docstrings
95 0 large files
102 -32 non-test files with autoImplicit true
41 0 Init files
5772 462 total LoC in Init files

Changed 'Init' lines by file

Current commit b8b8c3dbb9
Reference commit 58d07ea11e

Damiano Testa (Jul 08 2024 at 08:29):

The apparent regression in Init is actually due to #14383, adding a comment to all Init files of the intention to remove them! :upside_down:

Michael Rothgang (Jul 09 2024 at 09:44):

#14560 and #14362 remove further uses of autoImplicit

Michael Rothgang (Jul 10 2024 at 10:53):

#14607 updates the style exceptions, removing a handful of now-stale entries: very easy to review

Michael Rothgang (Jul 10 2024 at 10:54):

Does #13871 (replace manual measurability calls by fun_prop) count as technical debt? Three-week review ping on this one.

Ruben Van de Velde (Jul 10 2024 at 12:26):

Michael Rothgang said:

#14607 updates the style exceptions, removing a handful of now-stale entries: very easy to review

merge conflict

Ruben Van de Velde (Jul 10 2024 at 12:28):

Michael Rothgang said:

Does #13871 (replace manual measurability calls by fun_prop) count as technical debt? Three-week review ping on this one.

I'd be happy to improve the replacements, but I'm less confident about which lemmas should be tagged (and I guess you need all those additions to do the replacements)

Michael Rothgang (Jul 10 2024 at 12:41):

Ruben Van de Velde said:

Michael Rothgang said:

#14607 updates the style exceptions, removing a handful of now-stale entries: very easy to review

merge conflict

Indeed, fixed now.

Johan Commelin (Jul 10 2024 at 15:36):

Concerning technical debt reductions: I'm working on removing bit0/1 from mathlib.

Ruben Van de Velde (Jul 10 2024 at 15:41):

Speaking of, feel free to review #14168 :)

Jireh Loreaux (Jul 10 2024 at 22:33):

I'll look at #13871 tonight since I'm developing a better understanding of fun_prop

Miyahara Kō (Jul 11 2024 at 06:17):

#14642 removes 3 1 Init files.

Johan Commelin (Jul 11 2024 at 13:18):

chore: remove bit0 and bit1 #14644

Johan Commelin (Jul 11 2024 at 17:10):

This PR is now failing because many simp lemmas are no longer good simp lemmas.

I am wondering what will be the most helpful step forward for reviewers.

  • Should I just delete all lemmas about bit0 and bit1 in this PR
  • Or in a follow-up PR?
  • Should I leave open #14644 as is, for review purposes
  • Or should I at least remove a whole bunch of simp attributes in this PR

Riccardo Brasca (Jul 11 2024 at 17:15):

What do you think is the easiest for you? If the end result is the same I don't think it is very important.

Yaël Dillies (Jul 11 2024 at 17:15):

If that helps (not sure it helps, haven't looked at the PR), I'm of the opinion that unsimping deprecated lemmas is fair game(/encouraged)

Ruben Van de Velde (Jul 11 2024 at 18:23):

I'll be glad to see them go, but I'm not sure this is the best approach when we want to remove/rename most if not all of the lemmas you touch. I'm wondering if it might be better to work in smaller batches that can get us where we want to do in one step

Johan Commelin (Jul 11 2024 at 20:31):

Riccardo Brasca said:

What do you think is the easiest for you? If the end result is the same I don't think it is very important.

I think what I would prefer is if this PR is reviewed as is. And then I stack another PR on top of this that fixes CI. And then that one is also reviewed (with #14644 as base). And when we are happy with that, then we merge the total result.

Riccardo Brasca (Jul 12 2024 at 10:15):

Is there another PR that passes CI? (You unfortunately already have quite a lot of merge conflicts in #14644).

Ruben Van de Velde (Jul 12 2024 at 11:01):

Probably all mine, I can fix after #14672 lands

Johan Commelin (Jul 12 2024 at 11:12):

I fixed the current conflicts

Johan Commelin (Jul 12 2024 at 12:06):

And the others.

Michael Rothgang (Jul 13 2024 at 03:19):

A few more easy autoImplicits: #14694

Johan Commelin (Jul 13 2024 at 17:06):

I'm sorry for dropping the ball on #14644. I've got a nasty cold, and I'm out for the weekend. Feel free to adopt the PR.

Michael Rothgang (Jul 14 2024 at 11:30):

Two more PRs removing autoImplicit: #14725 and #14726
(#14709, depending on these, has another batch of files.)

github mathlib4 bot (Jul 15 2024 at 04:06):

Current number Change Type
6802 -50 porting notes
10 0 backwards compatibility flags
40 0 skipAssignedInstances flags
137 0 adaptation notes
287 0 disabled simpNF lints
151 -16 disabled deprecation lints
1923 -16 erw
25 -1 maxHeartBeats modifications
932 -26 documentation nolint entries
22 -7 missing module docstrings
93 -2 large files
83 -19 non-test files with autoImplicit true
41 0 Init files
5769 -3 total LoC in Init files

Changed 'Init' lines by file

Current commit af10129053
Reference commit 8b3a9507ac

Johan Commelin (Jul 15 2024 at 04:32):

#14743 removes all but one porting notes from SetTheory/Lists.

Johan Commelin (Jul 15 2024 at 05:55):

#14744 is a PR on top of #14644 that removes many deprecated lemmas and simp attributes. And #14745 is a PR that combines the two.

Johan Commelin (Jul 15 2024 at 10:55):

chore: remove bit0/bit1 and associated lemmas #14745

now passes CI

Riccardo Brasca (Jul 15 2024 at 11:03):

Is the idea to remove stuff like natDegree_bit1 in a later PR?

Riccardo Brasca (Jul 15 2024 at 11:06):

If this is the plan #14745 LGTM, we can live with meaningless name for a bit.

Johan Commelin (Jul 15 2024 at 11:08):

Yeah, I definitely want to have a follow-up PR

Johan Commelin (Jul 15 2024 at 11:09):

But I'm trying to keep this PR in a reviewable size.

Michael Rothgang (Jul 17 2024 at 11:47):

#14828 adds module docstrings to all missing tactics: after that, only Data/ByteArray remains.

github mathlib4 bot (Jul 22 2024 at 04:06):

Current number Change Type
6675 -127 porting notes
10 0 backwards compatibility flags
40 0 skipAssignedInstances flags
137 0 adaptation notes
289 2 disabled simpNF lints
106 -45 disabled deprecation lints
1938 15 erw
25 0 maxHeartBeats modifications
882 -50 documentation nolint entries
0 -22 missing module docstrings
93 0 large files
17 -66 non-test files with autoImplicit true
18 -23 Init files
2395 -3374 total LoC in Init files

Changed 'Init' lines by file

Current commit e41e510215
Reference commit ce90d3589f

Johan Commelin (Jul 22 2024 at 06:49):

No more missing module docstrings :tada: :octopus:

#15002 removes the entry from the table.

Michael Rothgang (Jul 23 2024 at 10:39):

#15052 updates the list of style exceptions: the number of large files is falling rapidly :tada:

github mathlib4 bot (Jul 29 2024 at 04:06):

Current number Change Type
6598 -76 porting notes
10 0 backwards compatibility flags
40 0 skipAssignedInstances flags
136 -1 adaptation notes
289 0 disabled simpNF lints
107 1 disabled deprecation lints
1937 -1 erw
23 -2 maxHeartBeats modifications
882 0 documentation nolint entries
66 -27 large files
17 0 non-test files with autoImplicit true
18 0 Init files
2395 0 total LoC in Init files

Changed 'Init' lines by file

Current commit 2159435a6c
Reference commit 0a67e5a4cc

Jon Eugster (Jul 30 2024 at 08:08):

I've just found myself searching mathlib to find there are 1848 occurences of the string TODO. Is this something that could be tracked here, too?

Damiano Testa (Jul 30 2024 at 08:17):

Tracking occurrences of the string TODO is just a matter of adding one line to the script that reports these "debts".

Damiano Testa (Jul 30 2024 at 08:19):

I often wonder, though, whether some of these "in-code notes" should be more than just comments and whether it would be useful to have more commands like #adaptation_note that are actually parse by Lean (and probably do nothing). If that were available, besides being able to track them via grep, they would also be addressable in bulk via metaprogramming.

Yaël Dillies (Jul 30 2024 at 08:33):

@Eric Rodriguez has made an issue with short comments about every todo

Damiano Testa (Jul 30 2024 at 08:36):

Right, I forgot about it! #7987

Michael Rothgang (Jul 30 2024 at 08:45):

There are currently about 230 references to lean4#2644 in mathlib - which were created prior to the #adaptation_note command. I propose using that for this case.

Eric Rodriguez (Jul 30 2024 at 10:36):

just to note that it's super out of date and haven't been able to maintain it - I'm desperately busy at my day job :(

Michael Rothgang (Aug 04 2024 at 14:26):

#15490 proposes including open (scoped) Classical statements that are not open (scoped) Classical in

github mathlib4 bot (Aug 05 2024 at 04:06):

Current number Change Type
6581 -17 porting notes
10 0 backwards compatibility flags
40 0 skipAssignedInstances flags
136 0 adaptation notes
289 0 disabled simpNF lints
107 0 disabled deprecation lints
1917 -20 erw
22 -1 maxHeartBeats modifications
882 0 documentation nolint entries
66 0 large files
17 0 non-test files with autoImplicit true
17 -1 Init files
1984 -411 total LoC in Init files

Changed 'Init' lines by file

Current commit 39adedf118
Reference commit 188a24253a

github mathlib4 bot (Aug 12 2024 at 04:06):

Current number Change Type
6547 -34 porting notes
10 0 backwards compatibility flags
32 -8 skipAssignedInstances flags
137 1 adaptation notes
289 0 disabled simpNF lints
135 28 disabled deprecation lints
1914 -3 erw
20 -2 maxHeartBeats modifications
882 0 documentation nolint entries
66 0 large files
273 -60 bare open (scoped) Classical
17 0 non-test files with autoImplicit true
16 -1 Init files
1936 -48 total LoC in Init files

Changed 'Init' lines by file

Current commit e5d297f011
Reference commit 94a5464783

Jireh Loreaux (Aug 15 2024 at 18:43):

Can we add something to these counters? How about Deprecated files, or total LoC in Deprecated files?

Jireh Loreaux (Aug 15 2024 at 18:44):

Also, should we add actual @[deprecated] tags to everything in the Deprecated folder so that we can eventually get rid of it? Some of it has been chilling in there for at least 3-4 years.

Damiano Testa (Aug 15 2024 at 18:48):

Just like what is done for Init, but for Deprecated? This should be really quick!

Damiano Testa (Aug 15 2024 at 18:54):

Here is what it would look like today:

Current number Change Type
6507 -46 porting notes
10 0 backwards compatibility flags
32 -7 skipAssignedInstances flags
138 -3 adaptation notes
287 -2 disabled simpNF lints
138 29 disabled deprecation lints
1925 11 erw
20 -3 maxHeartBeats modifications
782 -100 documentation nolint entries
65 -1 large files
239 -38 bare open (scoped) Classical
17 0 non-test files with autoImplicit true
9 3 Deprecated files
1980 100 total LoC in Deprecated files
9 -7 Init files
1577 -374 total LoC in Init files

Changed 'Init' lines by file

Current commit 46a3ce0bc2
Reference commit ec7748d19a

Damiano Testa (Aug 15 2024 at 18:56):

#15853

Notification Bot (Aug 16 2024 at 11:16):

8 messages were moved from this topic to #PR reviews > #15371 Remove some uses of open Classical by Johan Commelin.

github mathlib4 bot (Aug 19 2024 at 04:06):

Current number Change Type
6496 -51 porting notes
10 0 backwards compatibility flags
32 0 skipAssignedInstances flags
138 1 adaptation notes
287 -2 disabled simpNF lints
143 8 disabled deprecation lints
1925 11 erw
20 0 maxHeartBeats modifications
781 -101 documentation nolint entries
66 0 large files
222 -51 bare open (scoped) Classical
17 0 non-test files with autoImplicit true
9 1 Deprecated files
1980 26 total LoC in Deprecated files
9 -7 Init files
1627 -309 total LoC in Init files

Changed 'Init' lines by file

Current commit 74ed769345
Reference commit 267c64bef5

Johan Commelin (Aug 19 2024 at 06:30):

#15964 moves Data/Set/Defs.lean to Data/Set/Operations.lean so that we can move Init/Set.lean out of Init/ and to Data/Set/Defs.lean.

Johan Commelin (Aug 19 2024 at 09:20):

#15967 is the follow-up that moves Set out of Init.

Johan Commelin (Aug 22 2024 at 12:00):

There are 8 files left in Init/. Can we get rid of them before next Monday?

Yaël Dillies (Aug 22 2024 at 12:01):

Please no!

Yaël Dillies (Aug 22 2024 at 12:02):

I already had to make #15228 go through a traumatic rebase. I would now like Init.Algebra.Classes to not be touched until it is merged

Kim Morrison (Aug 22 2024 at 12:04):

Let's see if we can get #15228 in, then. :-)

Kim Morrison (Aug 22 2024 at 12:05):

I just hit merge on its dependency.

Matthew Ballard (Aug 22 2024 at 12:10):

#15152 touched one so I moved it.

Johan Commelin (Aug 22 2024 at 12:11):

@Matthew Ballard Could you please remove the Init header comment from that file?

Matthew Ballard (Aug 22 2024 at 12:13):

Not at a computer. Please feel free to push to it

Yaël Dillies (Aug 23 2024 at 09:18):

#15228 is now awaiting review

Johan Commelin (Aug 23 2024 at 09:27):

@Yaël Dillies transitive imports seem to be mostly going up...

Yaël Dillies (Aug 23 2024 at 09:28):

That's expected, right? I'm incorporating Init files (which have close to zero imports) into non-Init files (which have a small but non-zero number of imports).

Yaël Dillies (Aug 23 2024 at 09:30):

The alternative would be to have Init-like files outside of Init, but that's explicitly the kind of design decisions that would make those files hard to work with.

Johan Commelin (Aug 23 2024 at 09:31):

I guess that's fair...

Yaël Dillies (Aug 23 2024 at 09:33):

I haven't checked but I also believe that Init.Algebra.Classes is now transferring some imports around when it is almost entirely deprecated.

Yaël Dillies (Aug 23 2024 at 09:34):

Separately, there is an argument to be made that Order.Defs shouldn't contain unbundled relation classes. I am somewhat sympathetic to that, but would like to hear a stronger argument than "basic files have gained a handful of even more basic imports".

Dagur Asgeirsson (Aug 23 2024 at 12:06):

I've been cleaning up a bit in CategoryTheory/Adjunction and CategoryTheory/Sites, removing a bunch of porting notes. The following types of porting notes can just be removed, right?

  • Those about clear improvements from lean 3 to lean 4, like for example Porting note: Lean 3 proof continued with a rewrite but we're done here
  • Those of the form "this is now a syntactic tautology and hence commented out"

The PRs in question are #16071, #16086, #16089, #16091 and #16092 if someone wants to take a look

Yaël Dillies (Aug 23 2024 at 12:11):

Dagur Asgeirsson said:

  • Those of the form "this is now a syntactic tautology and hence commented out"

Barely anything actually became a syntactic tautology when going from Lean 3 to Lean 4. Most likely, those commentd out lemmas were misported.

Dagur Asgeirsson (Aug 23 2024 at 12:36):

Ok, I had removed two of those, one was indeed misported (coe_fun_coe in Sites/Grothendieck.lean) and I changed it to an explanation of that, the other one is AFAICT exactly the same as in mathlib 3, but I added the porting note back. It's mem_sieves_iff_coe in the same file.

Yaël Dillies (Aug 23 2024 at 12:38):

docs3#category_theory.grothendieck_topology.mem_sieves_iff_coe

Dagur Asgeirsson (Aug 23 2024 at 12:39):

That link doesn't work, but here it is
category_theory.grothendieck_topology.mem_sieves_iff_coe

Yaël Dillies (Aug 23 2024 at 12:39):

(it does work for me)

Dagur Asgeirsson (Aug 23 2024 at 12:40):

Sorry, it works now

Yaël Dillies (Aug 23 2024 at 12:40):

It is a syntactic tautology because GrothendieckTopology C was ported to use CoeFun instead of FunLike. Any reason why?

Dagur Asgeirsson (Aug 23 2024 at 12:43):

I don't understand, it uses CoeFun in mathlib 3 as well

Yaël Dillies (Aug 23 2024 at 12:44):

Yes, but docs3#has_coe_to_fun.coe is not reducible in Lean 3, as opposed to docs#CoeFun.coe

Yaël Dillies (Aug 23 2024 at 12:44):

So yes the lemma statement has changed, and the way to fix it is to make GrothendieckTopology use FunLike

Matthew Ballard (Aug 23 2024 at 12:46):

Where is docs#CoeFun.coe registered as reducible?

Yaël Dillies (Aug 23 2024 at 12:47):

Unclear, but it is, as you can check by uncommenting GrothendieckTopology.mem_sieves_iff_coe

Dagur Asgeirsson (Aug 23 2024 at 13:32):

#16092 now builds with a DFunLike instance for GrothendieckTopology instead of CoeFun

Jeremy Tan (Aug 23 2024 at 16:32):

Johan Commelin said:

There are 8 files left in Init/. Can we get rid of them before next Monday?

#16096 deprecates everything in Init.Data.Nat.Lemmas

Matthew Ballard (Aug 23 2024 at 16:39):

I am not sure we want deprecate docs#Nat.strong_induction_on but admittedly haven't been paying attention

Yaël Dillies (Aug 23 2024 at 16:41):

Certainly we don't want to deprecate docs#Nat.twoStepInduction !

Jeremy Tan (Aug 23 2024 at 17:04):

Yaël Dillies said:

Certainly we don't want to deprecate docs#Nat.twoStepInduction !

It was only used once in mathlib

Yaël Dillies (Aug 23 2024 at 17:07):

Someone used it on Xena just last week. That's good evidence it is useful

Jeremy Tan (Aug 23 2024 at 17:07):

Who and for what?

Ruben Van de Velde (Aug 23 2024 at 17:28):

I just used it in a proof of CharP here on zulip.

Ruben Van de Velde (Aug 23 2024 at 17:29):

I don't think we need to continue arguing about this. Someone can move these results to a better place if you don't want to

Mario Carneiro (Aug 23 2024 at 18:16):

Matthew Ballard said:

Where is docs#CoeFun.coe registered as reducible?

it's not, it's a magic function with the coercion internals attribute which means that it is unfolded after TC resolution (this is not the same as being reducible, it is removed at parse time)

Jeremy Tan (Aug 24 2024 at 06:43):

Yaël Dillies said:

Certainly we don't want to deprecate docs#Nat.twoStepInduction !

I have moved it to Data.Nat.Defs in the PR

Violeta Hernández (Aug 24 2024 at 06:49):

Matthew Ballard said:

I am not sure we want deprecate docs#Nat.strong_induction_on but admittedly haven't been paying attention

I find having the induction principles written out like this very useful even with the termination checker. It can be really finicky at times - sometimes it won't complain about a faulty induction until you've written our the rest of your long argument, or it won't be able to prove a decreasing argument automatically. Having a concrete type signature solves these issues.

Violeta Hernández (Aug 24 2024 at 06:50):

So yeah, don't deprecate these!

Violeta Hernández (Aug 24 2024 at 07:05):

Wait, Nat.strong_induction_on is just an alias of Nat.strongRecOn?

Violeta Hernández (Aug 24 2024 at 07:05):

If so then actually I'm all for deprecating that one

Violeta Hernández (Aug 24 2024 at 07:05):

Do keep the two step induction though

Jeremy Tan (Aug 24 2024 at 07:07):

Violeta Hernández said:

Wait, Nat.strong_induction_on is just an alias of Nat.strongRecOn?

Actually Nat.strongInductionOn, and similarly for Nat.cases_strong_induction_on being an alias of Nat.casesStrongInductionOn

Yaël Dillies (Aug 24 2024 at 07:08):

It's an alias for discoverability, since people looking for a theorem are looking for a snake_case lemma, not a lowerCamelCase def. I am however in favor of deleting/renaming docs#Nat.strongInductionOn, docs#Nat.caseStrongInductionOn which are lemma-named definitions

Yaël Dillies (Aug 24 2024 at 07:09):

... sadly, they are in core

Jeremy Tan (Aug 24 2024 at 07:13):

Yaël Dillies said:

I am however in favor of deleting/renaming docs#Nat.strongInductionOn, docs#Nat.caseStrongInductionOn which are lemma-named definitions

What would you like to rename them to?

Jeremy Tan (Aug 24 2024 at 07:24):

The problem is that if you try something like this in core

@[elab_as_elim] protected theorem strong_induction_on
    {motive : Nat → Sort u}
    (n : Nat)
    (ind : ∀ n, (∀ m, m < n → motive m) → motive n) : motive n :=
  Nat.lt_wfRel.wf.fix ind n

you get type of theorem 'Nat.strong_induction_on' is not a proposition

Yaël Dillies (Aug 24 2024 at 07:25):

...RecOn instead of ...InductionOn, just like every other recursor

Jeremy Tan (Aug 24 2024 at 07:25):

So like this?

@[elab_as_elim] protected noncomputable def strongRecOn
    {motive : Nat → Sort u}
    (n : Nat)
    (ind : ∀ n, (∀ m, m < n → motive m) → motive n) : motive n :=
  Nat.lt_wfRel.wf.fix ind n

@[elab_as_elim] protected noncomputable def caseStrongRecOn
    {motive : Nat → Sort u}
    (a : Nat)
    (zero : motive 0)
    (ind : ∀ n, (∀ m, m ≤ n → motive m) → motive (succ n)) : motive a :=
  Nat.strongRecOn a fun n =>
    match n with
    | 0   => fun _  => zero
    | n+1 => fun h₁ => ind n (λ _ h₂ => h₁ _ (lt_succ_of_le h₂))

Jeremy Tan (Aug 24 2024 at 07:34):

But Nat.strongRecOn is in Batteries

Jeremy Tan (Aug 24 2024 at 08:33):

I've made lean4#5147 to make the above changes in core

Kim Morrison (Aug 26 2024 at 02:00):

@Jeremy Tan, please fix branch#lean-pr-testing-5147. Once you have a builds-mathlib label on #5147, ping me and I'll merge.

Jeremy Tan (Aug 26 2024 at 02:02):

@Kim Morrison but how can I fix the mathlib branch when an error is in Batteries?

Kim Morrison (Aug 26 2024 at 02:08):

There is a lean-pr-testing-5147 branch of batteries too.

Kim Morrison (Aug 26 2024 at 02:08):

You can make a PR to that branch, ping me and I'll merge it.

Kim Morrison (Aug 26 2024 at 02:08):

Then in the mathlib branch, change the batteries dependency to point to lean-pr-testing-5147 and push that.

Jeremy Tan (Aug 26 2024 at 02:49):

@Kim Morrison batteries adaptation PR is at https://github.com/leanprover-community/batteries/pull/933

Kim Morrison (Aug 26 2024 at 03:03):

@Jeremy Tan, I removed the comment, which isn't necessary when things are upstreamed directly, and merged.

github mathlib4 bot (Aug 26 2024 at 04:06):

Current number Change Type
6407 -87 porting notes
10 0 backwards compatibility flags
32 0 skipAssignedInstances flags
138 0 adaptation notes
285 -2 disabled simpNF lints
89 -54 disabled deprecation lints
1929 4 erw
20 0 maxHeartBeats modifications
781 0 documentation nolint entries
66 0 large files
218 -4 bare open (scoped) Classical
17 0 non-test files with autoImplicit true
9 0 Deprecated files
1980 0 total LoC in Deprecated files
6 -3 Init files
1056 -573 total LoC in Init files

Changed 'Init' lines by file

Current commit 8e8377ed25
Reference commit 6dfa77d6cd

Jeremy Tan (Aug 26 2024 at 05:14):

@Kim Morrison lean-pr-testing-5147 has built successfully
image.png

Violeta Hernández (Aug 26 2024 at 09:13):

Quick question, what's this erw thing and why are we trying to get rid of it?

Johan Commelin (Aug 26 2024 at 09:15):

erw is like rw but angrier :very_angry: . And it's Expensive :dollar_bills: :money_with_wings: , hence the e.

It tries to do more unfolding then rw, so it succeeds more often.

But it is a code smell, hinting at missing simp-lemmas. And using it means that downstream in the proof other automation can grind to a halt. We are seeing this particularly in category theory (with concrete categories) and in algebraic geometry.

Jeremy Tan (Aug 26 2024 at 12:58):

#16154: all uses of autoImplicit are removed, outside tests

Jeremy Tan (Aug 26 2024 at 13:49):

(btw #16149 deletes Init.Quot)

Jeremy Tan (Sep 01 2024 at 07:13):

#16378 moves Init.Data.Quot to Logic.Relation

Johan Commelin (Sep 02 2024 at 16:10):

I guess the bot celebrates US holidays?

Bryan Gin-ge Chen (Sep 02 2024 at 16:13):

I don't understand the error message from the failed run, but I've re-triggered it: https://github.com/leanprover-community/mathlib4/actions/runs/10660569226/job/29544746099

Julian Berman (Sep 02 2024 at 16:22):

I think possibly it's tripping the content limit, and not showing that in a helpful way?

Julian Berman (Sep 02 2024 at 16:22):

Specifically this says:

The content of the message. Maximum message size of 10000 bytes.

But what's being passed is clearly longer than 10000 bytes.

Damiano Testa (Sep 02 2024 at 16:23):

It looks like something that was supposed to count the number of files, actually printed the files, maybe?

Julian Berman (Sep 02 2024 at 16:23):

Yeah last run is way way way shorter and doesn't have all those filenames in it.

Damiano Testa (Sep 02 2024 at 16:26):

The output of

grep -c '^set_option linter.style.longFile [0-9]*' $(git ls-files '*.lean')

looks like what the bot printed, but I think that this was tallied in the previous runs.

Julian Berman (Sep 02 2024 at 16:34):

I am not 100% sure what's happening without debugging closer, but I am slightly worried that some things are lying because the shell script doesn't have set -e and pipefail

Julian Berman (Sep 02 2024 at 16:35):

So it's possible some stuff is failing and then the script is continuing on with life

Damiano Testa (Sep 02 2024 at 16:35):

Here is what changed:

# before
printf '%s|%s\n' "$(
    { grep 'ERR_NUM_LIN' scripts/style-exceptions.txt
      grep '^set_option linter.style.longFile [0-9]*' $(git ls-files '*.lean') ; } | wc -l
  )" "large files"
# after
printf '%s|%s\n' "$(grep -c '^set_option linter.style.longFile [0-9]*' $(git ls-files '*.lean'))" "large files"

Damiano Testa (Sep 02 2024 at 16:35):

I think that there was a wc missing.

Damiano Testa (Sep 02 2024 at 16:36):

I propose

printf '%s|%s\n' "$(
    grep '^set_option linter.style.longFile [0-9]*' $(git ls-files '*.lean') | wc -l
  )" "large files"

Damiano Testa (Sep 02 2024 at 16:37):

That reports 74, instead of a really long list of filenames.

Damiano Testa (Sep 02 2024 at 16:39):

#16418

Damiano Testa (Sep 02 2024 at 20:13):

By the way, this is (more or less) what the bot did not post earlier today:

Current number Change Type
6357 -26 porting notes
10 0 backwards compatibility flags
30 -2 skipAssignedInstances flags
136 -1 adaptation notes
275 0 disabled simpNF lints
89 0 disabled deprecation lints
1899 -20 erw
21 1 maxHeartBeats modifications
764 -17 documentation nolint entries
74 74 large files
218 0 bare open (scoped) Classical
5 -12 non-test files with autoImplicit true
9 0 Deprecated files
1981 1 total LoC in Deprecated files
5 0 Init files
1017 4 total LoC in Init files

Changed 'Init' lines by file

Current commit b951101186
Reference commit cbe86e0d47

Damiano Testa (Sep 02 2024 at 20:14):

The "large files" line is "wrong", since the measure for it changed: it went from measuring lines in an exception file, to counting set_options in the long files. So it is not really indicative of a regression.

Jeremy Tan (Sep 03 2024 at 05:55):

#16434 moves Init.Data.List.Lemmas to Data.List.Defs. After this, the only remaining declarations in Init files still to upstream/move out/deprecate should be IsLeft(Right)Cancel, IsSymmOp and IsTotalPreorder in Init.Algebra.Classes – and Init.Logic

Jeremy Tan (Sep 03 2024 at 05:56):

I'd like assistance in determining what to do with the rest of the Init.Logic declarations

Jeremy Tan (Sep 03 2024 at 08:25):

…well I've deprecated most of Init.Logic at #16438

Johan Commelin (Sep 03 2024 at 09:21):

#16444 removes 4 backcomp flags. But we should bench it before merging

Jeremy Tan (Sep 03 2024 at 09:23):

I have opened lean4#5243, which upstreams some classes from the two outstanding Mathlib.Init files. This core PR should allow all declarations in Mathlib.Init.Algebra.Classes to be deprecated

Michael Rothgang (Sep 03 2024 at 10:04):

Damiano Testa said:

#16418

Sorry for the mess and thanks for cleaning it up! I took a look and have a refinement to suggest - hence would prefer to not merge my own code. :-)

Kim Morrison (Sep 04 2024 at 05:31):

Jeremy Tan said:

I have opened lean4#5243, which upstreams some classes from the two outstanding Mathlib.Init files. This core PR should allow all declarations in Mathlib.Init.Algebra.Classes to be deprecated

As I replied on that PR, PRs like this to Lean need to be preceeded either by an RFC, and even that should probably be preceeded by a discussion on zulip.

Yaël Dillies (Sep 04 2024 at 06:35):

Yes it's not very clear to me that we want to make almost unused typeclasses be part of core Lean because:

  1. They are not clearly useful
  2. It will be much harder to edit them later

Jireh Loreaux (Sep 04 2024 at 23:52):

  1. They cause maintenance debt for the FRO.

github mathlib4 bot (Sep 09 2024 at 04:06):

Current number Change Type
6317 -41 porting notes
10 0 backwards compatibility flags
30 0 skipAssignedInstances flags
160 23 adaptation notes
277 2 disabled simpNF lints
106 17 disabled deprecation lints
1896 -3 erw
25 4 maxHeartBeats modifications
764 0 documentation nolint entries
68 0 large files
218 -1 bare open (scoped) Classical
5 0 non-test files with autoImplicit true
9 0 Deprecated files
1981 0 total LoC in Deprecated files
3 -2 Init files
818 -199 total LoC in Init files

Changed 'Init' lines by file

Current commit 8c811c94af
Reference commit f43d6924ff

Jeremy Tan (Sep 12 2024 at 05:16):

According to my calculations this is about all that's left of Init.Logic

/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-/
import Mathlib.Tactic.Lemma
import Mathlib.Tactic.Relation.Trans

/-!
# Note about `Mathlib/Init/`
The files in `Mathlib/Init` are leftovers from the port from Mathlib3.
(They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)

We intend to move all the content of these files out into the main `Mathlib` directory structure.
Contributions assisting with this are appreciated.
-/

universe u v
variable {α : Sort u}

/- HEq, Iff -/

-- FIXME This is still rejected after #857
-- attribute [refl] HEq.refl
attribute [trans] HEq.trans
attribute [trans] heq_of_eq_of_heq
attribute [refl] Iff.refl
attribute [trans] Iff.trans

section Relation

variable {α : Sort u} {β : Sort v} (r : β → β → Prop)

/-- Local notation for an arbitrary binary relation `r`. -/
local infix:50 " ≺ " => r

/-- A reflexive relation relates every element to itself. -/
def Reflexive := ∀ x, x ≺ x

/-- A relation is symmetric if `x ≺ y` implies `y ≺ x`. -/
def Symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x

/-- A relation is transitive if `x ≺ y` and `y ≺ z` together imply `x ≺ z`. -/
def Transitive := ∀ ⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z

lemma Equivalence.reflexive {r : β → β → Prop} (h : Equivalence r) : Reflexive r := h.refl

lemma Equivalence.symmetric {r : β → β → Prop} (h : Equivalence r) : Symmetric r := fun _ _ ↦ h.symm

lemma Equivalence.transitive {r : β → β → Prop} (h : Equivalence r) : Transitive r :=
  fun _ _ _ ↦ h.trans

/-- A relation is total if for all `x` and `y`, either `x ≺ y` or `y ≺ x`. -/
def Total := ∀ x y, x ≺ y ∨ y ≺ x

/-- Irreflexive means "not reflexive". -/
def Irreflexive := ∀ x, ¬ x ≺ x

/-- A relation is antisymmetric if `x ≺ y` and `y ≺ x` together imply that `x = y`. -/
def AntiSymmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x → x = y

/-- An empty relation does not relate any elements. -/
@[nolint unusedArguments]
def EmptyRelation := fun _ _ : α ↦ False

theorem InvImage.trans (f : α → β) (h : Transitive r) : Transitive (InvImage r f) :=
  fun (a₁ a₂ a₃ : α) (h₁ : InvImage r f a₁ a₂) (h₂ : InvImage r f a₂ a₃) ↦ h h₁ h₂

theorem InvImage.irreflexive (f : α → β) (h : Irreflexive r) : Irreflexive (InvImage r f) :=
  fun (a : α) (h₁ : InvImage r f a a) ↦ h (f a) h₁

end Relation

section Binary

variable {α : Type u} {β : Type v} (f : α → α → α)

/-- `LeftCommutative op` says that `op` is a left-commutative operation,
i.e. `a₁ ∘ (a₂ ∘ b) = a₂ ∘ (a₁ ∘ b)`. -/
class LeftCommutative (op : α → β → β) : Prop where
  /-- A left-commutative operation satisfies `a₁ ∘ (a₂ ∘ b) = a₂ ∘ (a₁ ∘ b)`. -/
  left_comm : (a₁ a₂ : α) → (b : β) → op a₁ (op a₂ b) = op a₂ (op a₁ b)

/-- `RightCommutative op` says that `op` is a right-commutative operation,
i.e. `(b ∘ a₁) ∘ a₂ = (b ∘ a₂) ∘ a₁`. -/
class RightCommutative (op : β → α → β) : Prop where
  /-- A right-commutative operation satisfies `(b ∘ a₁) ∘ a₂ = (b ∘ a₂) ∘ a₁`. -/
  right_comm : (b : β) → (a₁ a₂ : α) → op (op b a₁) a₂ = op (op b a₂) a₁

instance left_comm [hc : Std.Commutative f] [ha : Std.Associative f] : LeftCommutative f :=
  ⟨fun a _ _ ↦ by rw [← ha.assoc, hc.comm a, ha.assoc]⟩

instance right_comm [hc : Std.Commutative f] [ha : Std.Associative f] : RightCommutative f :=
  ⟨fun _ b _ ↦ by rw [ha.assoc, hc.comm b, ha.assoc]⟩

end Binary

Johan Commelin (Sep 12 2024 at 05:33):

Great work!

Jeremy Tan (Sep 12 2024 at 05:35):

I have to deprecate 14 iff lemmas first though (this is in branch#fourteen)

Violeta Hernández (Sep 13 2024 at 00:51):

Where are Reflexive, Symmetric, and Transitive being used? What happens if we go to those places and use IsRefl, etc. instead?

Johan Commelin (Sep 13 2024 at 03:35):

Good questions, I dunno the answer, someone should find out :wink:

Jeremy Tan (Sep 14 2024 at 03:35):

To review and merge, please:

  • #16751 (turn LeftCommutative, RightCommutative into typeclasses, preparing for #16748)
  • #16757 (easy deprecations, a move and changing IsSymmOp to be like other typeclasses)

Jeremy Tan (Sep 14 2024 at 04:52):

Violeta Hernández said:

Where are Reflexive, Symmetric, and Transitive being used? What happens if we go to those places and use IsRefl, etc. instead?

Well for a start I am anticipating obstacles in SimpleGraph because its definition uses Symmetric and Irreflexive. If I change them to IsSymm and IsIrrefl then aesop cannot automatically fill in proofs of the symmetric and loopless (irreflexive) properties anymore

Jeremy Tan (Sep 14 2024 at 05:53):

@Violeta Hernández I have created branch#test-deprecate-irrefl to demonstrate the effects of deprecating just Irreflexive, AntiSymmetric and Total. As you can see, model theory is particularly affected

Jeremy Tan (Sep 14 2024 at 07:51):

Based on this I am now of the opinion that the six relational definitions in Init.Logic that aren't deprecated should be kept and moved to Order.Defs

Jeremy Tan (Sep 14 2024 at 07:54):

The declarations without Is live in theorem space, those with Is live in instance space, and the two should not mingle

Jeremy Tan (Sep 15 2024 at 02:01):

So #16748 and #16796 conclude the cleanup of Mathlib.Init!

Jeremy Tan (Sep 16 2024 at 04:14):

#16836 deletes six Deprecated files

Kim Morrison (Sep 16 2024 at 04:34):

I'm in favour.

While these haven't had a @[deprecated] attribute, they've been sitting unchanged in the Deprecated directory for a long time.

If someone shows up saying they were still using them, we can consider restoring them / putting them in a separate repo / asking them to adopt into their project.

Jeremy Tan (Sep 16 2024 at 04:36):

@Kim Morrison reverted the tech debt counter update

Jeremy Tan (Sep 16 2024 at 04:51):

(and updated the description…)

Johan Commelin (Sep 16 2024 at 11:14):

But somehow the bot didn't post...

Edward van de Meent (Sep 16 2024 at 12:15):

it seems to be due to changes @Michael Rothgang made, robustifying scripts in this commit

Edward van de Meent (Sep 16 2024 at 12:15):

there are missing optional arguments, which now makes the script fail

Bryan Gin-ge Chen (Sep 16 2024 at 12:25):

Looks like the "unofficial bash strict mode" URL that was referenced in the change suggests using "parameter default values".

Bryan Gin-ge Chen (Sep 16 2024 at 12:26):

Seems like a quick fix, I'll make a PR now.

Bryan Gin-ge Chen (Sep 16 2024 at 12:59):

Thanks Edward for identifying the issue! PR at #16854

Michael Rothgang (Sep 16 2024 at 14:10):

Sorry for the inconvenience, thanks for fixing this quickly.
Indeed, I had made a similar change in #15996, and inadvertedly cherry-picked only half the changes to the technical debt metrics.

Michael Rothgang (Sep 16 2024 at 14:10):

(If anybody would like to review #15996, be my guest.)

Edward van de Meent (Sep 16 2024 at 14:20):

for now, i've hit re-run on the workflow

Edward van de Meent (Sep 16 2024 at 14:20):

(which apparently doesn't check out the current master branch?)

Bryan Gin-ge Chen (Sep 16 2024 at 14:31):

It looks like it's possible to allow workflows to be manually triggered if we add a workflow_dispatch trigger, which seems convenient for our other scheduled workflows as well.

I don't have time to do this right now but I'll try and take care of it tonight unless someone else beats me to it.

Johan Commelin (Sep 16 2024 at 15:25):

Current number Change Type
6294 -22 porting notes
10 0 backwards compatibility flags
30 0 skipAssignedInstances flags
160 0 adaptation notes
277 0 disabled simpNF lints
121 15 disabled deprecation lints
1888 -10 erw
24 -1 maxHeartBeats modifications
759 -5 documentation nolint entries
66 -2 large files
218 0 bare open (scoped) Classical
4 -1 non-test files with autoImplicit true
9 0 Deprecated files
1980 0 total LoC in Deprecated files
3 0 Init files
544 -274 total LoC in Init files

Changed 'Init' lines by file

Current commit a03152ba78
Reference commit 8079b7f17f

Johan Commelin (Sep 16 2024 at 15:25):

/me trying to impersonate the bot :up:

Bryan Gin-ge Chen (Sep 16 2024 at 18:30):

#16862 should let us manually trigger our scheduled workflows when it's merged.

Edward van de Meent (Sep 16 2024 at 18:48):

i'd like to point out that this will allow any user with write access to trigger those workflows (including the ones that post to zulip).

Edward van de Meent (Sep 16 2024 at 18:50):

(which may be of some kind of security concern)

Bryan Gin-ge Chen (Sep 16 2024 at 19:12):

Good point. I suppose we could add some kind of user check if we wanted to, but at a first glance, I don't see any major security issues here. We will be able to see who ran the workflows so if there's some kind of strange abuse then it should be fine to take away permissions. (Someone with write perms can do much greater damage with just git!)

Looking over the workflows briefly:

  • dependent-issues.yml and merge_conflicts.yml just run checks on our github repo, so they should be fine to run manually (though running too frequently will hit the API limit)
  • nolints.yml and update_dependencies.yml both create PRs when they are run, but they have logic preventing them from opening duplicate PRs, so they should also be fine.
  • lean4checker.yml and technical_debt_metrics.yml will post to Zulip each time they are run, but I can't imagine any of our contributors using them to spam.
  • nightly_bump_toolchain.yml and nightly_merge_master.yml will push commits to the nightly-testing branch, so I suppose someone could annoy people working on that branch if they wanted, but nightly_bump_toolchain.yml already had the workflow_dispatch event so I assume the convenience outweighs the risk in that case, and the other workflow seems similar enough to me (with the caveat that I don't know the etiquette / rules around nightly-testing). Again, anyone with write access can already do much worse from the command line.

Edward van de Meent (Sep 16 2024 at 19:25):

i do agree that the security issues are minimal. if it is too risky, perhaps making the runs try again automatically in logarithmic fashion (when they failed/continue to fail) is a good mechanism too?

Bryan Gin-ge Chen (Sep 16 2024 at 19:33):

I think most of the failures are due to bugs in our workflows and scripts rather than temporary issues / flakiness, but yeah, that could be something to look into in the future, particularly for the jobs which frequently hit the GitHub API limit.

Jeremy Tan (Sep 17 2024 at 02:44):

I would have expected #16836 to have been merged by now

Kim Morrison (Sep 17 2024 at 03:12):

It is a slightly complicated one because of potential downstream users. I don't think any such exist, however, as these files are unused since the port..

Kim Morrison (Sep 17 2024 at 03:12):

I'll merge given a +1 from a reviewer!

Violeta Hernández (Sep 17 2024 at 06:12):

Jeremy Tan said:

I would have expected #16836 to have been merged by now

You guys are getting your PRs approved within a day? Lucky!

Ruben Van de Velde (Sep 17 2024 at 06:29):

I wish!

Notification Bot (Sep 17 2024 at 06:39):

A message was moved from this topic to #mathlib4 > deprecated sub{monoid,group} predicates by Johan Commelin.

github mathlib4 bot (Sep 23 2024 at 04:06):

Current number Change Type
6285 -19 porting notes
10 0 backwards compatibility flags
30 0 skipAssignedInstances flags
160 0 adaptation notes
277 0 disabled simpNF lints
163 51 disabled deprecation lints
1896 7 erw
24 0 maxHeartBeats modifications
752 -7 documentation nolint entries
65 -2 large files
219 1 bare open (scoped) Classical
3 -1 non-test files with autoImplicit true
9 0 Deprecated files
1980 0 total LoC in Deprecated files
3 0 Init files
544 0 total LoC in Init files

Changed 'Init' lines by file

Current commit 9890065b5f
Reference commit 2a811d0dea

Kim Morrison (Sep 23 2024 at 04:31):

Ugh, what happened with going backwards on disabling deprecation lints and erw?

Kim Morrison (Sep 23 2024 at 04:34):

Can anyone think of a cheap way to find additions of erw in the last week?

Kim Morrison (Sep 23 2024 at 04:35):

Ideally any PR adding new erw would also have had a zulip discussion trying to avoid it.

Violeta Hernández (Sep 23 2024 at 04:47):

I think I've disabled a few deprecation lints myself, but that's only because large swaths of API are being deprecated. So the number should go down again once those are deleted.

Violeta Hernández (Sep 23 2024 at 04:47):

I definitely didn't add 50 though...

Damiano Testa (Sep 23 2024 at 04:53):

Indeed, a few deprecations are in #15820. Others seem to come from #16220.

Daniel Weber (Sep 23 2024 at 04:59):

Kim Morrison said:

Can anyone think of a cheap way to find additions of erw in the last week?

git log 2a811d0dea^.. -S"erw " returns #9417, #16727, #16718, #16853, #16891, #15716, #16531, #16819 as PRs touching erw

Violeta Hernández (Sep 23 2024 at 05:00):

Damiano Testa said:

Indeed, a few deprecations are in #15820. Others seem to come from #16220.

Oh damn maybe this is my fault :sweat_smile:

Violeta Hernández (Sep 23 2024 at 05:01):

But of course, the idea is for these deprecation notices and their associated theorems to be deleted a few months from now.

Violeta Hernández (Sep 23 2024 at 05:02):

It'd be nice if we could omit deprecated theorems from the deprecation linter count. That way none of this would be flagged.

Damiano Testa (Sep 23 2024 at 05:02):

I think that most of the erw are in #9417.

Violeta Hernández (Sep 23 2024 at 05:02):

As in, if we disable the linter in Y because it's a deprecated theorem about the deprecated definition X, then Y shouldn't add to the count

Daniel Weber (Sep 23 2024 at 05:03):

Daniel Weber said:

Kim Morrison said:

Can anyone think of a cheap way to find additions of erw in the last week?

git log 2a811d0dea^.. -S"erw " returns #9417, #16727, #16718, #16853, #16891, #15716, #16531, #16819 as PRs touching erw

Looking at it:

Damiano Testa (Sep 23 2024 at 05:05):

If we are seriously tracking these debt counters, maybe it would be better to actually lint against adding more to these counters.

Damiano Testa (Sep 23 2024 at 05:06):

As is, now it almost feels like we are blaming people who increased these counts, but there was no way that this could be known at the moment of the PR.

Violeta Hernández (Sep 23 2024 at 05:13):

That'd be nice. My suggestion would have to be implemented first though, since I've got a lot more PRs in the works that will keep adding to this count otherwise.

Violeta Hernández (Sep 23 2024 at 05:13):

(see #17033 for anyone curious)

Damiano Testa (Sep 23 2024 at 05:22):

This seems to be an example of what is happening with the deprecation nolints:

@[deprecated]
def depr := 0

@[deprecated]
theorem depr_zero : depr = 0 := rfl  -- `depr` has been deprecated

I think that it is valuable to know that depr is deprecated, maybe there should be a @[deprecated!] variant of the deprecated attribute that silences deprecations in the declaration?

Yaël Dillies (Sep 23 2024 at 06:25):

Is there a good use case for deprecated declarations mentioning other deprecated declarations to be flagged with a warning?

Yaël Dillies (Sep 23 2024 at 06:26):

I would think not, so the behaviour you describe for deprecated! should become the new behaviour of deprecated

Yaël Dillies (Sep 23 2024 at 06:26):

(I am pretty sure I already suggested this somewhere and there was some disagreement?)

Kim Morrison (Sep 23 2024 at 06:33):

I think the "use case" is to make it annoying to deal with deprecated declarations, so they get deleted. :-)

Yaël Dillies (Sep 23 2024 at 09:30):

Well, the more annoying deprecations are, the less of them you will get :wink:

Mario Carneiro (Sep 24 2024 at 13:42):

I originally wanted to implement @[deprecated] to work like this, but the current implementation approach makes it difficult. (@[deprecated] isn't actually a linter, it just pretends to be one while running during elaboration.) This should probably be a lean4 issue

Michael Rothgang (Sep 24 2024 at 19:14):

#17017 removes the autoImplicit files metric from the tech debt list, as this has served its purpose :tada:

Michael Rothgang (Sep 24 2024 at 19:16):

#17109 proposes warning against autoImplicit true in mathlib (outside of tests).

Kim Morrison (Sep 25 2024 at 00:06):

Michael Rothgang said:

#17017 removes the autoImplicit files metric from the tech debt list, as this has served its purpose :tada:

#17107 (digit-swap!)

Mario Carneiro (Sep 25 2024 at 00:23):

Michael Rothgang said:

#17109 proposes warning against autoImplicit true in mathlib (outside of tests).

Isn't this just going to cause lints on top of lints? autoImplicit is already a lint which is already being suppressed

Mario Carneiro (Sep 25 2024 at 00:24):

I think it would make more sense to just keep track of the number of set_option autoImplicit true as a tech debt counter

Mario Carneiro (Sep 25 2024 at 00:37):

Michael Rothgang said:

#17017 removes the autoImplicit files metric from the tech debt list, as this has served its purpose :tada:

I don't think we should remove tech debt metrics. Instead they should be silently elided if they have value 0, and we should fix things so that the answer is actually 0 and not 3. This is the whole idea behind @[nolint] and nolints.json being different - you want to differentiate deliberate uses of a restricted technique from tech debt uses

Johan Commelin (Sep 25 2024 at 03:43):

Good point! I agree that eliding metrics with value 0 is better.

Michael Rothgang (Sep 25 2024 at 07:17):

I agree with this, in general --- but in this special case, I am not so sure:
to me, the reasoning behind including autoImplicit always was "the great majority of these are technical debt, so let's track this" - with the understanding that using it in very restricted cases could actually be fine. (Perhaps I'm missing nuance here; my understanding is that not all maintainers believe "all autoImplicit is bad".) The two remaining files in mathlib using it are such cases, in my opinion.

If you disagree, feel free to file a PR removing it! But that has been proposed, and imho the diff is less readable.

Michael Rothgang (Sep 25 2024 at 07:19):

Mario Carneiro said:

Michael Rothgang said:

#17109 proposes warning against autoImplicit true in mathlib (outside of tests).

Isn't this just going to cause lints on top of lints? autoImplicit is already a lint which is already being suppressed

There should be ~no exceptions (indeed, the PR adds one exception overall). The point of the warning, for me, is to prevent accidentally re-introducing this. Yes, a reviewer could catch this, but if automation can catch this already, that's even better.

Mario Carneiro (Sep 25 2024 at 15:50):

What I mean is, this is like having a dialog saying "are you sure you want to press Yes on the 'are you sure you want to quit' dialog?"

github mathlib4 bot (Sep 30 2024 at 04:07):

Current number Change Type
6272 -13 porting notes
9 -1 backwards compatibility flags
30 0 skipAssignedInstances flags
147 -13 adaptation notes
277 0 disabled simpNF lints
164 1 disabled deprecation lints
1901 5 erw
25 1 maxHeartBeats modifications
750 -2 documentation nolint entries
65 0 large files
219 0 bare open (scoped) Classical
9 0 Deprecated files
1982 2 total LoC in Deprecated files
3 0 Init files
544 0 total LoC in Init files

Changed 'Init' lines by file

Current commit 07a48737b7
Reference commit 6fd58d5c79

github mathlib4 bot (Oct 07 2024 at 04:07):

Current number Change Type
6252 -20 porting notes
9 0 backwards compatibility flags
30 0 skipAssignedInstances flags
201 54 adaptation notes
279 2 disabled simpNF lints
164 0 disabled deprecation lints
1894 -7 erw
25 0 maxHeartBeats modifications
748 -2 documentation nolint entries
63 -2 large files
219 0 bare open (scoped) Classical
9 0 Deprecated files
1982 0 total LoC in Deprecated files
3 0 Init files
544 0 total LoC in Init files

Changed 'Init' lines by file

Current commit 3d637cea4a
Reference commit 39b61a6aaa

Johan Commelin (Oct 07 2024 at 06:37):

That's a lot of new adaptation notes :sad:

Violeta Hernández (Oct 07 2024 at 06:38):

where do they come from?

Damiano Testa (Oct 07 2024 at 06:43):

#17377 maybe?

Damiano Testa (Oct 07 2024 at 06:45):

A good number of them say

#adaptation_note
/--
After nightly-2024-09-06 we can remove the `_root_` prefix below.
-/

Yaël Dillies (Oct 07 2024 at 07:15):

At this rate, all porting notes will be gone by 2030 (:tada:)

Johan Commelin (Oct 07 2024 at 11:34):

Damiano Testa said:

A good number of them say

#adaptation_note
/--
After nightly-2024-09-06 we can remove the `_root_` prefix below.
-/

Sounds like it is telling us to do something (-;

Johan Commelin (Oct 07 2024 at 11:34):

When I'm back at my desktop, I will create a PR removing them, unless someone beats me :racecar:

Johan Commelin (Oct 07 2024 at 14:05):

Working on this now :working_on_it:

Johan Commelin (Oct 07 2024 at 14:25):

#17498

Jireh Loreaux (Oct 07 2024 at 14:45):

I'm wondering if things like this:

 -- TODO: this instance was found automatically before #6045
have := @AlgebraicGeometry.LocallyRingedSpace.isLocalRingHomStalkMap X Y

should be recorded as adaptation_notes. As is, there is no way to track them because they are just TODOs. I realize that it's not an adaptation_note in the way that was originally designed (i.e., for adaptations from upstream changes), but perhaps we could still use it as such?

Jireh Loreaux (Oct 07 2024 at 14:47):

#6045 has several changes of that nature.

Jireh Loreaux (Oct 07 2024 at 14:48):

Another option is just to duplicate the code for adaptation_note into a new kind of note. Or else pass a String to adaptation note that contains the url of the relevant change.

Johan Commelin (Oct 07 2024 at 14:49):

I agree that it would be good to have a more structure way to track these.
Should we rename the current #adaptation_note to #core_adaptation_note?

Johan Commelin (Oct 07 2024 at 14:49):

Or at least: I would prefer if we can distinguish easily between adaptations because of changes in core and adaptations that are "mathlib internal".

Matthew Ballard (Oct 07 2024 at 14:59):

Should adaptation notes take a github id / repo id and number?

Johan Commelin (Oct 07 2024 at 15:01):

number = issue number?

Matthew Ballard (Oct 07 2024 at 15:01):

Does Github keep separate numbers for issues/PRs or the counter counts both?

Johan Commelin (Oct 07 2024 at 15:02):

It's a shared counter

Matthew Ballard (Oct 07 2024 at 15:02):

That would be the target for the number. There could be optional syntax for Issue/PR also.

Matthew Ballard (Oct 07 2024 at 15:24):

#17508 removes some adaptation_notes from lean#5376

Damiano Testa (Oct 07 2024 at 19:34):

I strongly approve going from the current #adaptation_notes to more dependently type ones! :smile:

That would help also with systematically removing one issue, like the case above, where you could then make sure that all issues were resolved.

Johan Commelin (Oct 08 2024 at 04:03):

We can of course grep for the pr number already, in the case above

github mathlib4 bot (Oct 14 2024 at 04:07):

Current number Change Type
6164 -88 porting notes
9 0 backwards compatibility flags
29 -1 skipAssignedInstances flags
159 -42 adaptation notes
279 0 disabled simpNF lints
174 10 disabled deprecation lints
1503 -391 erw
29 4 maxHeartBeats modifications
744 -4 documentation nolint entries
64 1 large files
219 0 bare open (scoped) Classical
4879 0 exceptions for the docPrime linter
9 0 Deprecated files
1982 0 total LoC in Deprecated files
3 0 Init files
544 0 total LoC in Init files

Changed 'Init' lines by file

Current commit cfdf6e790c
Reference commit e7484e60ae

github mathlib4 bot (Oct 21 2024 at 04:07):

Current number Change Type
5934 -230 porting notes
9 0 backwards compatibility flags
29 0 skipAssignedInstances flags
178 19 adaptation notes
282 3 disabled simpNF lints
177 3 disabled deprecation lints
1521 18 erw
29 0 maxHeartBeats modifications
743 -1 documentation nolint entries
65 1 large files
211 -8 bare open (scoped) Classical
4881 2 exceptions for the docPrime linter
16 7 Deprecated files
2718 736 total LoC in Deprecated files
0 -3 Init files
total LoC in Init files

Changed 'Init' lines by file

Current commit 4d87f692a5
Reference commit da6abacefb

Violeta Hernández (Oct 21 2024 at 04:33):

I think we might be going backwards somewhat

Johan Commelin (Oct 21 2024 at 06:26):

Why do you say that? Because of the LoC in Deprecated files?

Kim Morrison (Oct 21 2024 at 06:27):

Well, notably erw went up as well. :-(

Damiano Testa (Oct 21 2024 at 06:31):

I agree that it does not look like an improvement on every front, but it looks like the Init files counter can now be ignored!

Damiano Testa (Oct 21 2024 at 06:32):

Maybe Deprecated is the new Init.

Damiano Testa (Oct 21 2024 at 07:03):

I updated the script in #17993, replacing Init with Deprecated.

Below is what the new script would show now.

Deprecated instead of Init

Anne Baanen (Oct 21 2024 at 08:32):

Damiano Testa said:

64 -1918 Mathlib/Deprecated/NatLemmas.lean

That doesn't seem right: the file wasn't there last week and has 64 lines now. Do you know how it came up with this number?

Daniel Weber (Oct 21 2024 at 08:49):

Also weird is that the total LoC is equal to the total change

Damiano Testa (Oct 21 2024 at 09:00):

I'll look into this: I simply copied over the script from the Init check, but likely there was an implicit assumption that those files existed in an earlier version, which is not necessarily the case with Deprecated.

Damiano Testa (Oct 21 2024 at 09:46):

Ok, the script actually assumes that the Init/Deprecated filenames never change and are the same in the reference commit and in the current one. This was actually wrong already for the old version of the script, but "good enough", since those files got rarely deleted and even more rarely added.

Damiano Testa (Oct 21 2024 at 09:47):

It will take a little change in the script to update "properly" the Deprecated files: I'll get to it soon!

github mathlib4 bot (Oct 28 2024 at 04:07):

Current number Change Type
5303 -631 porting notes
9 0 backwards compatibility flags
29 0 skipAssignedInstances flags
173 -5 adaptation notes
279 -3 disabled simpNF lints
174 -3 disabled deprecation lints
1531 10 erw
29 0 maxHeartBeats modifications
743 0 documentation nolint entries
66 1 large files
212 1 bare open (scoped) Classical
4880 -1 exceptions for the docPrime linter
16 0 Deprecated files
2716 -2 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 132344bd66
Reference commit c8f7de855a

Kim Morrison (Oct 28 2024 at 05:41):

#18319 makes significant progress on backwards compatibility flags

Kim Morrison (Oct 28 2024 at 05:41):

and #18320 on skipAssignedInstances flags

Johan Commelin (Oct 28 2024 at 05:44):

Thanks! Let's bench both of them.

Damiano Testa (Oct 28 2024 at 08:09):

Also note that Init files are no longer a thing!

Johan Commelin (Oct 29 2024 at 06:19):

#18369 excludes counting maxHeartbeats in test/. We are down to 8!

Michael Rothgang (Nov 02 2024 at 14:22):

Mario Carneiro said:

What I mean is, this is like having a dialog saying "are you sure you want to press Yes on the 'are you sure you want to quit' dialog?"

From a Lean core perspective, this makes sense. autoImplicit is enabled there, so mathlib's configuration is the odd one out, and having to jump through hoops on re-enabling it in mathlib feels like the warning fatigue above.
Let me propose a different phrasing, coming from the perspective of a math user in mathlib, I claim that using autoImplicit is either unknown or surprising. (Indeed, common advice when teaching Lean in some form is to turn off that option, as the first thing you're doing.) Living just in math-land, autoImplicit is always off, and having a warning on activating it makes sense.

From a pragmatic view-point: I claim that mathlib reviewers would usually reject PRs adding that option. The linter in #17109 just codifies this internal convention, saving reviewer time.

Michael Rothgang (Nov 02 2024 at 14:23):

That said: if there's consensus that not having this linter is preferred, I can certainly close that PR.

Violeta Hernández (Nov 02 2024 at 19:45):

I only recently learned about autoImplicit. Turns out I used it this whole time on my Rubik's cube project!

Violeta Hernández (Nov 02 2024 at 19:45):

What's the setting to disable it on an entire project?

Edward van de Meent (Nov 02 2024 at 19:51):

make sure something along the lines of the following is in your lakefile.lean:

package «Test» where
  -- Settings applied to both builds and interactive editing
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`pp.proofs.withType, false⟩,
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩
  ]

copied from one of my own projects, adjust as needed...

Michael Rothgang (Nov 02 2024 at 22:14):

Or: take a look at mathlib's lakefile.lean, and copy from the mathlibOption array what you want to apply. :-)

github mathlib4 bot (Nov 04 2024 at 04:07):

Current number Change Type
5201 -102 porting notes
7 -2 backwards compatibility flags
14 -15 skipAssignedInstances flags
167 -6 adaptation notes
279 0 disabled simpNF lints
175 1 disabled deprecation lints
1531 0 erw
0 -13 maxHeartBeats modifications
719 -24 documentation nolint entries
67 1 large files
213 1 bare open (scoped) Classical
4881 1 exceptions for the docPrime linter
16 0 Deprecated files
2719 3 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit fef6aa3e68
Reference commit bafdce7177

Johan Commelin (Nov 04 2024 at 05:23):

It looks like the remaining 8 maxHeartbeats modifications were also removed! I didn't realize that. Cool!

Kim Morrison (Nov 04 2024 at 06:32):

No, that is a false hope, they are still there in master.

Damiano Testa (Nov 04 2024 at 07:10):

Has it been the case that every run of the technical debt counter had at least one bug? :face_palm:

Damiano Testa (Nov 04 2024 at 07:53):

In the script, I think that there is a : that is confusing git grep in some path specification that only occurs for the maxHeartbeats.

Johan Commelin (Nov 04 2024 at 07:56):

  "maxHeartBeats modifications"    ":^test" "^ *set_option .*maxHeartbeats"

I thought that this : meant "omit".

Johan Commelin (Nov 04 2024 at 07:56):

Because we want to grep everything except the tests.

Johan Commelin (Nov 04 2024 at 07:56):

That's how it works locally

Damiano Testa (Nov 04 2024 at 07:59):

I think that there is a missing -- before the path specification to "escape" it.

Damiano Testa (Nov 04 2024 at 07:59):

For me, this works:

git grep '--' '^ *set_option .*maxHeartbeats' -- ':^test'

Damiano Testa (Nov 04 2024 at 07:59):

(note the two -- to separate various parts)

Damiano Testa (Nov 04 2024 at 08:02):

This is the "new" diff:

Current number Change Type
5201 -102 porting notes
7 -2 backwards compatibility flags
14 -15 skipAssignedInstances flags
167 -6 adaptation notes
279 0 disabled simpNF lints
191 17 disabled deprecation lints
1531 0 erw
8 -21 maxHeartBeats modifications
719 -24 documentation nolint entries
67 1 large files
213 1 bare open (scoped) Classical
4881 1 exceptions for the docPrime linter
16 0 Deprecated files
2718 2 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 85f90384c2
Reference commit a9ecf75bdf

Damiano Testa (Nov 04 2024 at 08:02):

#18602

Johan Commelin (Nov 04 2024 at 08:12):

@Damiano Testa Well.... something else changed as well in the last week :rofl: We need to use MathlibTest now.

Damiano Testa (Nov 04 2024 at 08:19):

I update the PR and the above message with the "new" run: now it uses MathlibTest as path for the tests for both the current and reference hash: the results may still be off slightly, since last week it was test.

Damiano Testa (Nov 04 2024 at 08:20):

However, I guarantee that next week's report will be perfect.

Update: the fix was merged into master.

Notification Bot (Nov 04 2024 at 08:45):

9 messages were moved from this topic to #mathlib4 > late imports by Johan Commelin.

github mathlib4 bot (Nov 11 2024 at 04:07):

Current number Change Type
5155 -46 porting notes
5 -2 backwards compatibility flags
14 0 skipAssignedInstances flags
164 -3 adaptation notes
270 -9 disabled simpNF lints
197 22 disabled deprecation lints
1548 17 erw
9 1 maxHeartBeats modifications
719 0 documentation nolint entries
67 0 large files
216 3 bare open (scoped) Classical
4884 3 exceptions for the docPrime linter
16 0 Deprecated files
2718 -1 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 006c0fc200
Reference commit 5f90ccdd9e

Johan Commelin (Nov 11 2024 at 06:49):

Hmm erw is going up again

Markus Himmel (Nov 11 2024 at 06:55):

Did we introduce a "no new erws" policy that I missed? I have bors r+ed a few erws recently where I looked at the goal before and after, decided that it was not "malicious" abuse of defeq (whatever that means), and let it slide (https://github.com/leanprover-community/mathlib4/blob/8fa662232f9bac9afad1064b6807f885ecb42a6b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean#L102 comes to mind for example). I'd be very happy with a "no new erws" policy though (supported by a linter).

Johan Commelin (Nov 11 2024 at 07:00):

There is no policy at the moment. It's just a signal that we should investigate sooner rather than later.

Johan Commelin (Nov 11 2024 at 07:00):

And we should have good alternatives, before enacting a policy

Damiano Testa (Nov 11 2024 at 07:05):

Also, a linter would either start with a lot of nolints or with a lot of fixing.

Markus Himmel (Nov 11 2024 at 07:32):

Yes, I had the "a lot of nolints" option in mind.

Damiano Testa (Nov 11 2024 at 07:35):

The linter (with the nolints file) would be very easy to write, but I also think that Johan's point is more pressing: there is no clear path for avoiding an erw...

Anne Baanen (Nov 11 2024 at 08:36):

I think erw in itself is not an issue, but places where rw fails to apply are often places where other tactics, or typeclass instance synthesis, might also fail. So encountering a lot of erws can suggest that we might want to change our design. Unfortunately, technical reasons sometimes make it hard to change designs (such as the duplication around concrete category coercions).

Anne Baanen (Nov 11 2024 at 08:36):

Also, sometimes erws stick around where cheap rws also work. So every so often I run the linter of #17638 and replace some erw with rw for free :)

Damiano Testa (Nov 11 2024 at 08:38):

Maybe we could run the automatic replacement in a cron job that creates a PR with the replacements that can be inspected before being merged.

Anne Baanen (Nov 11 2024 at 09:04):

Anne Baanen said:

Also, sometimes erws stick around where cheap rws also work. So every so often I run the linter of #17638 and replace some erw with rw for free :)

Every so often happens to include today, so: #18847 reduces the erw count by 5 :)

Damiano Testa (Nov 11 2024 at 09:53):

I am also very happy that no one pointed out any issues with the report this week! :smile:

Kim Morrison (Nov 11 2024 at 14:32):

#18864 deals with about 10% of the simpNF nolints. I think at this point the majority of our simpNF nolints are either spurious, or we should remove the @[simp] itself, it's just a matter of ploughing through them.

Violeta Hernández (Nov 11 2024 at 21:03):

#17602 gets rid of a handful of simpNFs

Kim Morrison (Nov 13 2024 at 00:20):

More simpNFs at #18943

Violeta Hernández (Nov 13 2024 at 23:54):

#18200 also takes care of some simpNFs

Damiano Testa (Nov 13 2024 at 23:56):

If you merge current master in your PR, the PR summary comment will have a new section containing the change that your PR has on technical debts!

Damiano Testa (Nov 13 2024 at 23:57):

(I am mentioning this, since it is relatively rare to have a PR that has some change to technical debt and I am curious to test the script... :smile: )

Damiano Testa (Nov 13 2024 at 23:58):

It worked! 3 fewer porting notes and 3 fewer nolint simpNF!

Ruben Van de Velde (Nov 14 2024 at 00:06):

#19001 has some porting notes too :)

Damiano Testa (Nov 14 2024 at 00:09):

If porting notes continue being decreased in multiples of 3, removing the last one will be hard...

github mathlib4 bot (Nov 18 2024 at 04:07):

Current number Change Type
5096 -59 porting notes
5 0 backwards compatibility flags
14 0 skipAssignedInstances flags
185 21 adaptation notes
220 -50 disabled simpNF lints
206 9 disabled deprecation lints
1556 8 erw
9 0 maxHeartBeats modifications
716 -3 documentation nolint entries
65 -2 large files
220 4 bare open (scoped) Classical
4879 -5 exceptions for the docPrime linter
16 0 Deprecated files
2718 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 25f427c356
Reference commit 04897dfe99

Kim Morrison (Nov 18 2024 at 04:25):

Does "disabled deprecation lints" count turning off linter.deprecated for a declaration that is itself deprecated? It should not. These will naturally disappear as time passes.

Kim Morrison (Nov 18 2024 at 04:25):

I think it is also counting occurrences in Mathlib/Deprecated/, which I think it should not.

Kim Morrison (Nov 18 2024 at 06:37):

@Violeta Hernández, would you mind taking a looking at section bsup in Mathlib.SetTheory.Ordinal.Arithmetic: there is a set_option linter.deprecated false in that section, but the following declarations are not themselves deprecated.

Kim Morrison (Nov 18 2024 at 06:40):

Besides that file, and the overcounting mentioned above, #19181 comes pretty close to cleaning up set_option linter.deprecated false.

Violeta Hernández (Nov 18 2024 at 06:44):

Kim Morrison said:

Violeta Hernández, would you mind taking a looking at section bsup in Mathlib.SetTheory.Ordinal.Arithmetic: there is a set_option linter.deprecated false in that section, but the following declarations are not themselves deprecated.

I'm working on it! bsup is unfortunately still used in a few places, but it shouldn't be used in any new theorems and will be deprecated soon.

Violeta Hernández (Nov 18 2024 at 06:45):

#19145 gets rid of one of its usages

Damiano Testa (Nov 18 2024 at 08:00):

Kim Morrison said:

Does "disabled deprecation lints" count turning off linter.deprecated for a declaration that is itself deprecated? It should not. These will naturally disappear as time passes.

Yes, the script simply counts how many times the string set_option linter.deprecated false appears in mathlib. Making it aware of what is being deprecated and cross-referencing it with that being deprecated would be a substantial upgrade of this report and would likely be better suited for a script in Lean, rather than a shell script.

Damiano Testa (Nov 18 2024 at 08:01):

Kim Morrison said:

I think it is also counting occurrences in Mathlib/Deprecated/, which I think it should not.

Here again the answer is "yes, it is looking everywhere", but now making it not search inside Mathlib/Deprecated is in scope!

Damiano Testa (Nov 18 2024 at 08:10):

#19184 for not looking for deprecations in Deprecated.

Damiano Testa (Nov 18 2024 at 08:11):

Although, there seem to be only 8 linter.deprecated false in that dir.

Kim Morrison (Nov 18 2024 at 09:53):

Damiano Testa said:

Yes, the script simply counts how many times the string set_option linter.deprecated false appears in mathlib. Making it aware of what is being deprecated and cross-referencing it with that being deprecated would be a substantial upgrade of this report and would likely be better suited for a script in Lean, rather than a shell script.

Could we just ignore any set_option linter.deprecated false for which the following line contains @[deprecated (or some slightly more robust regex?

Yaël Dillies (Nov 18 2024 at 09:54):

Why can't we allow deprecated declarations to refer to deprecated declarations?

Yaël Dillies (Nov 18 2024 at 09:54):

(I remember Mario explained something at some point, but I don't remember it exactly and I exactly remember not being super convinced by his argument)

Damiano Testa (Nov 18 2024 at 10:02):

Kim Morrison said:

Could we just ignore any set_option linter.deprecated false for which the following line contains @[deprecated (or some slightly more robust regex?

Bypassing the deprecated refactor mentioned above, yes, this would indeed be easy to implement. It involves extracting set_option linter.deprecated false into its own custom (very short) script, but there are already other counters that are special-cased.

Damiano Testa (Nov 18 2024 at 10:02):

I'll try to get to this later today.

Damiano Testa (Nov 18 2024 at 10:17):

Btw, with a very quick script, there seem to be 130 deprecated linter options followed by @[deprecated...]. So, likely, a more correct number for the deprecated entry above is 206 - 8 - 130 = 68.

Kim Morrison (Nov 18 2024 at 10:24):

Yaël Dillies said:

Why can't we allow deprecated declarations to refer to deprecated declarations?

It's tricky, I did have a look at this, but currently there's not an easy hook to change options after the attributes have been processed, but before the rest of the declaration has been elaborated.

Damiano Testa (Nov 18 2024 at 11:16):

I updated the #19184 with Kim's suggestion as well: the current version omits all Mathlib/Deprecated paths and counts set_options linter.deprecated false that are not followed by @[deprecated...] on the following line.

This is what the script reports right now:

Current number Change Type
5096 -56 porting notes
5 0 backwards compatibility flags
14 0 skipAssignedInstances flags
185 21 adaptation notes
220 -50 disabled simpNF lints
1553 8 erw
9 0 maxHeartBeats modifications
71 4 disabled deprecation lints
716 -3 documentation nolint entries
65 -2 large files
220 4 bare open (scoped) Classical
4879 -5 exceptions for the docPrime linter
16 0 Deprecated files
2718 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 035c73548d
Reference commit 0465f40a73

Mario Carneiro (Nov 18 2024 at 12:09):

Yaël Dillies said:

Why can't we allow deprecated declarations to refer to deprecated declarations?

(I remember Mario explained something at some point, but I don't remember it exactly and I exactly remember not being super convinced by his argument)

I don't remember what I said, but my reconstruction is that I would have said that this is desirable but currently difficult to implement due to the way deprecations are reported (it's not actually a linter, it runs at elaboration time and this has a few drawbacks)

github mathlib4 bot (Nov 25 2024 at 04:07):

Current number Change Type
5041 -55 porting notes
5 0 backwards compatibility flags
14 0 skipAssignedInstances flags
183 -2 adaptation notes
201 -19 disabled simpNF lints
1558 2 erw
9 0 maxHeartBeats modifications
54 -16 disabled deprecation lints
705 -11 documentation nolint entries
61 -4 large files
220 0 bare open (scoped) Classical
4879 4879 exceptions for the docPrime linter
17 1 Deprecated files
2830 112 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 386ab515e2
Reference commit 5750078e99

Kim Morrison (Nov 25 2024 at 04:23):

Decent!

Damiano Testa (Nov 25 2024 at 06:42):

The weirdness in the docPrime linter should be due to the fact that the exception file changed names and the bot got confused.

Damiano Testa (Nov 25 2024 at 06:43):

Also, besides manually removing lemmas with a prime that no longer exist, there is no automated mechanism to update the list of exceptions.

github mathlib4 bot (Dec 02 2024 at 04:07):

Current number Change Type
5022 -19 porting notes
5 0 backwards compatibility flags
14 0 skipAssignedInstances flags
184 1 adaptation notes
200 -1 disabled simpNF lints
1527 -31 erw
9 0 maxHeartBeats modifications
56 2 disabled deprecation lints
704 -1 documentation nolint entries
62 1 large files
218 -2 bare open (scoped) Classical
4882 3 exceptions for the docPrime linter
18 1 Deprecated files
2857 27 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit dde4f2ecae
Reference commit aa050b47ff

Johan Commelin (Dec 02 2024 at 05:01):

That seems to be mostly progress

Jireh Loreaux (Dec 02 2024 at 11:37):

I went on a porting note killing spree in #19685. I just hunted randomly and looked for easy ones to kill while I procrastinated doing other things.

Anne Baanen (Dec 02 2024 at 16:11):

Tiny improvement in erw count (-3): #19689

Kim Morrison (Dec 03 2024 at 01:29):

#19701 deals with all disabled deprecation lints except in Mathlib.SetTheory.Ordinal.Arithmetic.

Kim Morrison (Dec 03 2024 at 01:29):

(@Violeta Hernández, perhaps you could prioritize that? The Ordinal files have seen too much churn already ...)

Kim Morrison (Dec 03 2024 at 01:31):

@Damiano Testa, would you mind changing the technical debt counter script? Currently it does a subtraction to count set_option linter.deprecated false not followed by deprecated. Better to do it with this regex:

set_option linter\.deprecated false.*(?:(?:\n/--.*?-/\n(?!.*deprecated))|\n(?!.*deprecated|/--))

which also acccounts for intervening doc-strings.

Kim Morrison (Dec 03 2024 at 01:31):

If we can have that measurement also exclude Mathlib/Data/MLList, that would be great, as everything there is deprecated by now.

Violeta Hernández (Dec 03 2024 at 01:42):

Ordinal arithmetic is in fact somewhat of a mess since I'm in the middle of trying to deprecate half of the API defined in that file

Violeta Hernández (Dec 03 2024 at 01:47):

My main blocker right now is the cofinality file, which has a very long section of theorems relating cofinality to docs#Ordinal.lsub, docs#Ordinal.bsup, and all of the other special cases of iSup I'm trying to get rid of. I'm currently working on a complete rewrite of said file which aims to (among other things) reprove these theorems in terms of iSup instead. Once that's done, I'll be able to deprecate all of the "morally deprecated" declarations we currently have.

Violeta Hernández (Dec 03 2024 at 01:49):

If we really really need to get rid of these non-deprecated theorems using deprecated theorems right this instant, something I can do is to first redefine bsup, lsub, and blsub in terms of iSup, instead of keeping them defined in terms of the deprecated docs#Ordinal.sup. But do consider this is extra work on declarations that are ultimately going to be deleted.

Violeta Hernández (Dec 03 2024 at 01:50):

(For context on my ongoing ordinal refactors, see #17033)

Kim Morrison (Dec 03 2024 at 01:51):

No, it's not urgent.

Kim Morrison (Dec 03 2024 at 01:51):

But just a heads up that this is now the last part of the library where we need linter.deprecated false for non-deprecated declarations! :-)

github mathlib4 bot (Dec 09 2024 at 04:07):

Current number Change Type
4977 -34 porting notes
5 0 backwards compatibility flags
14 0 skipAssignedInstances flags
207 0 adaptation notes
202 -2 disabled simpNF lints
1499 -26 erw
16 0 maxHeartBeats modifications
87 31 disabled deprecation lints
703 -1 documentation nolint entries
62 0 large files
223 5 bare open (scoped) Classical
4882 0 exceptions for the docPrime linter
21 3 Deprecated files
3103 246 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 65c00859d0
Reference commit 41ff1f7899

Johan Commelin (Dec 09 2024 at 05:40):

< 5k porting notes
< 1.5k erw

:octopus:

Kim Morrison (Dec 09 2024 at 07:55):

The increase in disabled deprecation lints was me converting all the bare set_options to set_option ... in.

github mathlib4 bot (Dec 16 2024 at 04:07):

Current number Change Type
4861 -116 porting notes
5 0 backwards compatibility flags
14 0 skipAssignedInstances flags
207 0 adaptation notes
201 -1 disabled simpNF lints
1489 -10 erw
17 1 maxHeartBeats modifications
87 0 disabled deprecation lints
701 -2 documentation nolint entries
62 0 large files
222 -1 bare open (scoped) Classical
4882 0 exceptions for the docPrime linter
21 0 Deprecated files
3103 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 3f813de52d
Reference commit bd9aea4b24

David Loeffler (Dec 18 2024 at 10:27):

#20031 splits up Topology/Separation/Basic, which is currently one of the largest single files in the library.

Miyahara Kō (Dec 18 2024 at 10:29):

#19989 splits Tactic/CC/Addition.

github mathlib4 bot (Dec 23 2024 at 04:07):

Current number Change Type
4850 -11 porting notes
5 0 backwards compatibility flags
14 0 skipAssignedInstances flags
207 0 adaptation notes
201 0 disabled simpNF lints
1515 26 erw
17 0 maxHeartBeats modifications
88 1 disabled deprecation lints
700 -1 documentation nolint entries
58 -4 large files
224 2 bare open (scoped) Classical
4882 0 exceptions for the docPrime linter
21 0 Deprecated files
3103 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit e820917259
Reference commit aee9be2beb

github mathlib4 bot (Dec 30 2024 at 04:07):

Current number Change Type
4835 -6 porting notes
5 0 backwards compatibility flags
14 0 skipAssignedInstances flags
207 0 adaptation notes
201 0 disabled simpNF lints
1516 1 erw
17 0 maxHeartBeats modifications
88 0 disabled deprecation lints
700 0 documentation nolint entries
58 0 large files
224 0 bare open (scoped) Classical
4882 0 exceptions for the docPrime linter
21 0 Deprecated files
3103 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit b4e6697e70
Reference commit 38b244b718

Miyahara Kō (Jan 04 2025 at 03:59):

#20376 reduces doc nolints in notations by inherit_doc.

Miyahara Kō (Jan 04 2025 at 06:41):

#20467 removes unnecesarry adaptation notes.

Kim Morrison (Jan 05 2025 at 04:50):

#20484 removes around 60 or 70 erw, thanks to @David Renshaw's tryAtEachStep tool.

Ruben Van de Velde (Jan 05 2025 at 07:42):

Sadly it doesn't compile

Kim Morrison (Jan 05 2025 at 09:52):

Fixed now.

Kevin Buzzard (Jan 05 2025 at 14:45):

There's a 16% slowdown in Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated and it's picked up a merge conflict :-/

Kim Morrison (Jan 05 2025 at 22:07):

I've fixed the merge conflict, and replaced the change in Pretriangulated with a smaller change that I'll benchmark again.

(To be honest, however, I don't care at all about minor slowdowns relative to removing erw...)

Ruben Van de Velde (Jan 05 2025 at 22:13):

Is the goal to remove erw entirely?

Kim Morrison (Jan 06 2025 at 00:47):

I don't mind if a few uses remain, but they should all come with explanations of what is going on to require them.

Kim Morrison (Jan 06 2025 at 00:47):

Relying on erw seems to be a pretty reliable sign that things are not set up properly! :-)

github mathlib4 bot (Jan 06 2025 at 04:07):

Current number Change Type
4824 -11 porting notes
5 0 backwards compatibility flags
14 0 skipAssignedInstances flags
199 -8 adaptation notes
201 0 disabled simpNF lints
1513 -3 erw
79 -80 ofNat
17 0 maxHeartBeats modifications
94 6 disabled deprecation lints
673 -27 documentation nolint entries
58 0 large files
105 -119 bare open (scoped) Classical
4882 0 exceptions for the docPrime linter
21 0 Deprecated files
3106 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 95cdc7a6ab
Reference commit c4263a50a3

Ruben Van de Velde (Jan 06 2025 at 06:50):

Kim Morrison said:

Relying on erw seems to be a pretty reliable sign that things are not set up properly! :-)

Agree - but I've occasionally used it while developing to check that the proof works before spending time on adding API lemmas

Yaël Dillies (Jan 06 2025 at 08:28):

Kim Morrison said:

Relying on erw seems to be a pretty reliable sign that things are not set up properly! :-)

I just used erw yesterday in the following situation:
Rewriting an expression, a subexpression Finset.sup complicatedThing fun a => a appears. I have a lemma proving Finset.sup complicatedThing id = simplerThing, but I can't use it because no lemma that I could find states id = fun a => a. Both the equational lemma and docs#id.def state id a = a...

Kevin Buzzard (Jan 06 2025 at 08:30):

I doubt anyone would object if you added this lemma, I'm quite surprised we don't have it.

Yaël Dillies (Jan 06 2025 at 08:32):

The issue is that I would call it id.def, but it's already taken

Kevin Buzzard (Jan 06 2025 at 08:37):

How about id.def'?

Edward van de Meent (Jan 06 2025 at 08:37):

Perhaps a more general f = fun x => f x lemma?

Anne Baanen (Jan 06 2025 at 16:21):

#20521 replaces all occurrences of no_index (ofNat _) that grep could find with the new ofNat() macro.

github mathlib4 bot (Jan 13 2025 at 04:07):

Current number Change Type
4799 -25 porting notes
5 0 backwards compatibility flags
14 0 skipAssignedInstances flags
198 -1 adaptation notes
203 2 disabled simpNF lints
1419 -94 erw
17 0 maxHeartBeats modifications
96 2 disabled deprecation lints
672 -1 documentation nolint entries
59 1 large files
106 1 bare open (scoped) Classical
4878 -4 exceptions for the docPrime linter
21 0 Deprecated files
3101 -5 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 039d0c7642
Reference commit 10a421547e

Michael Rothgang (Jan 13 2025 at 14:12):

#20684 and #20683 remove some nolint entries using inherit_doc

Anne Baanen (Jan 13 2025 at 15:31):

#20714 deals with a few porting notes about function coercions.

Kent Van Vels (Jan 14 2025 at 21:16):

#20501 removes some technical debt and is awaiting a review/merge.

Kent Van Vels (Jan 14 2025 at 21:18):

It removes bare "classicals".

Jovan Gerbscheid (Jan 15 2025 at 14:58):

#20193 removed the remaining skipAssignedInstances flags.
#20214 removes all backwards compatibility flags, and some maxHeartBeats modification, which gives quite a bit of speedup.

github mathlib4 bot (Jan 20 2025 at 04:06):

Current number Change Type
4572 -227 porting notes
1 -4 backwards compatibility flags
1 -13 skipAssignedInstances flags
198 0 adaptation notes
201 -2 disabled simpNF lints
1414 -5 erw
11 -6 maxHeartBeats modifications
100 4 disabled deprecation lints
665 -7 documentation nolint entries
58 -1 large files
106 0 bare open (scoped) Classical
4878 0 exceptions for the docPrime linter
21 0 Deprecated files
3101 -1 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 14f0a13820
Reference commit 666dd63743

Kim Morrison (Jan 20 2025 at 10:58):

As far as I can see, the "backwards compatibility flags" and "skipAssignedInstances" counts are actually at zero.

  • Would anyone like to create a mathlib-only linter that forbids skipAssignedInstances?
  • We should not forbid set_option.*backward for now, as more may be introduced in future.
  • Could we remove these two lines from the technical debt report?
  • Thanks @Jovan Gerbscheid for killing these ones off!!

Johan Commelin (Jan 20 2025 at 11:14):

Haha, the tech debt counter is counting the script that counts the tech debt :rofl:

Johan Commelin (Jan 20 2025 at 11:16):

Could we remove these two lines from the technical debt report?

Let's not remove the backward compat counter. Since those might return, and it would be good to be automatically reminded then.

Johan Commelin (Jan 20 2025 at 11:16):

But we can certainly change the way entries are styled when their "Current number" is 0.

Yaël Dillies (Jan 20 2025 at 11:18):

Should entries be sorted in decreasing order of their "Current number"?

Kim Morrison (Jan 20 2025 at 11:56):

#20867 is a top-to-bottom review of nolint simpNF.

Michael Rothgang (Jan 20 2025 at 13:00):

#20872 is adding a linter against skipAssignedInstances. It's not as exhaustive as I'd like, but perhaps useful already.

github mathlib4 bot (Jan 27 2025 at 04:06):

Current number Change Type
4306 -266 porting notes
1 0 backwards compatibility flags
1 0 skipAssignedInstances flags
196 -2 adaptation notes
114 -87 disabled simpNF lints
1417 3 erw
11 0 maxHeartBeats modifications
101 1 disabled deprecation lints
646 -19 documentation nolint entries
57 -1 large files
63 -43 bare open (scoped) Classical
4877 -1 exceptions for the docPrime linter
21 0 Deprecated files
3101 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit a02b5327b9
Reference commit 510fdca8a0

Kent Van Vels (Jan 27 2025 at 14:34):

#20898 continues removing bare open (scoped) classicals. I have two more pull requests ready to go once this is approved. There is a question in #20898 about the proper way to remove a classical in a non-tactic proof. Any fresh eyes will be appreciated.

Kent Van Vels (Jan 29 2025 at 05:49):

#20898 has been reviewed and patched and (probably) ready to be merged.

Johan Commelin (Jan 29 2025 at 06:53):

The report should be running

$ git grep adaptation_note -- :^Mathlib/Tactic/Linter :^Mathlib/Tactic/AdaptationNote.lean | wc -l
179

instead of

$ git grep adaptation_note -- * | wc -l
194

Johan Commelin (Jan 29 2025 at 06:54):

But I don't know immediately how to accomplish that with our current setup

Kent Van Vels (Jan 29 2025 at 13:58):

#21217 continues removing bare open (scoped) classicals. I had a misunderstanding before about a review that has since been cleared up. I have one more pull request in this spirit after #21217.

Johan Commelin (Jan 29 2025 at 14:03):

Thanks! Great work

Johan Commelin (Jan 29 2025 at 14:28):

#21221 fixes some edge cases with the counters. They should be more accurate now. Especially the ones that had a count of 1 now end up being 0 :octopus:

Kent Van Vels (Jan 29 2025 at 15:34):

#21220 removes more bare open classicals.

Kent Van Vels (Jan 29 2025 at 16:50):

#21228 removes the last of the bare open classicals. There is one file that should be inspected: Mathlib/Order/DirectedInverseSystem.lean. I resorted to using the classical namespace in two function calls.

Damiano Testa (Jan 29 2025 at 21:22):

#21241 is another PR "fixing" the script: it allows parsing a string of paths that contains spaces by actually parsing each space-separated-path separately. If you know something about bash, you probably know what I am talking about!

Damiano Testa (Jan 29 2025 at 21:23):

In particular, the modification in the PR above avoid counting references to adaptation_note inside the file that defines them, so measuring only the ones "in the wild".

Damiano Testa (Jan 30 2025 at 07:52):

Since there have been a couple changes to the script that reports the technical debts, I will run it again now to make sure that it still works!

github mathlib4 bot (Jan 30 2025 at 07:57):

Current number Change Type
4278 -30 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
121 -48 adaptation notes
114 1 disabled simpNF lints
1413 -5 erw
12 1 maxHeartBeats modifications
101 1 disabled deprecation lints
646 -19 documentation nolint entries
55 -2 large files
0 -63 bare open (scoped) Classical
4877 -1 exceptions for the docPrime linter
15 -6 Deprecated files
1215 -1886 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 132efc702f
Reference commit 3abd04bf8d

Damiano Testa (Jan 30 2025 at 07:59):

Looks like the script still works!

github mathlib4 bot (Feb 03 2025 at 04:07):

Current number Change Type
4258 -43 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
121 -48 adaptation notes
113 0 disabled simpNF lints
1403 -14 erw
12 1 maxHeartBeats modifications
88 -13 disabled deprecation lints
640 -6 documentation nolint entries
50 -7 large files
1 -62 bare open (scoped) Classical
4877 0 exceptions for the docPrime linter
11 -10 Deprecated files
771 -2330 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 8926633ff2
Reference commit ff6124cf63

Michael Rothgang (Feb 03 2025 at 15:29):

From github:

Too bad we don't track attribute [local instance] as technical debt!

Should we do this? It should be easy to add.

Jireh Loreaux (Feb 03 2025 at 16:06):

Is that actually technical debt? I think in many cases it is not. E.g., consider the construction of norms on spaces which already have a topology. It is frequently the case that you construct a metric / norm structure with a "bad" topology, make a def and then immediately use attribute [local instance] to work with it while you prove things about it (like the fact that the "bad" topology is equal to the "good" topology). Then you end the section and you build the real instance with docs#MetricSpace.replaceTopology or whatever.

Jireh Loreaux (Feb 03 2025 at 16:08):

There are other examples. For instance, there are many norms available on matrices, and we don't want to activate any of them globally. The reasonable approach is to just provide the defs and then activate them locally when you want to use them. You might claim that we should make type synonyms, and my response is: no, you really don't unless you absolutely have to, see the work involved in #15277.

Johan Commelin (Feb 03 2025 at 16:12):

Hmm, those are good points.

Matthew Ballard (Feb 03 2025 at 16:13):

I also agree with @Jireh Loreaux 's points which is why I stated my opinion on PR review and not here :)

There are provocative things I can ask about that design pattern but there are already enough devolving topics at the moment.

My main complaint is that this can and is abused to paper over other issues.

Matthew Ballard (Feb 03 2025 at 16:14):

But I have no strong opinions on whether it deserves to go in here

Kevin Buzzard (Feb 03 2025 at 18:18):

I definitely need local instances. For example A⊗RBA\otimes_RB is not a BB-algebra if A,B,R are commutative rings and I'm not allowed to make the algebra structure a global instance because it will give a diamond if A=B but I absolutely cannot avoid wanting L⊗KAKL\otimes_K\mathbb{A}_K to be an algebra for both LL and AK\mathbb{A}_K in the Adele miniproject in FLT

Kevin Buzzard (Feb 03 2025 at 18:19):

I've tried switching the order of the tensor but at the end of the day we unsurprisingly need both algebra structures

Kevin Buzzard (Feb 03 2025 at 18:21):

By 'absolutely cannot avoid' I mean things like "module topology only works for modules, tensor product only works for modules, so ring homs aren't enough"

github mathlib4 bot (Feb 10 2025 at 04:06):

Current number Change Type
3993 -265 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
108 -13 adaptation notes
109 -4 disabled simpNF lints
1355 -48 erw
12 0 maxHeartBeats modifications
91 3 disabled deprecation lints
636 -4 documentation nolint entries
46 -4 large files
1 0 bare open (scoped) Classical
4877 0 exceptions for the docPrime linter
11 0 Deprecated files
771 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit ec3a82fc3c
Reference commit b76b14cff6

Kim Morrison (Feb 10 2025 at 04:35):

chore: remove/improve several set_option maxHeartbeats #21627

gets rid of most of the remaining maxHeartbeats.

Johan Commelin (Feb 10 2025 at 06:59):

Should CI prevent merging new open (scoped) Classical?

Michael Rothgang (Feb 10 2025 at 07:17):

(This would be easy to lint for, if desired.)

Johan Commelin (Feb 10 2025 at 07:29):

If we really consider it technical debt, then we should imho

Jovan Gerbscheid (Feb 10 2025 at 15:56):

@Kim Morrison , I think #21627 removed two docstring accidentally

Johan Commelin (Feb 10 2025 at 16:01):

Good catch!

Johan Commelin (Feb 10 2025 at 16:04):

Restored in #21669

github mathlib4 bot (Feb 17 2025 at 04:07):

Current number Change Type
3384 -609 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
106 -2 adaptation notes
109 0 disabled simpNF lints
1333 -22 erw
2 -10 maxHeartBeats modifications
91 0 disabled deprecation lints
625 -11 documentation nolint entries
43 -3 large files
1 0 bare open (scoped) Classical
4876 -1 exceptions for the docPrime linter
11 0 Deprecated files
771 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit c6a7350729
Reference commit 770d057c43

Michael Rothgang (Feb 17 2025 at 08:23):

#21977 and #21978 remove the last occurrences of bare open Classical; it seems the tech debt script misses them. The first PR should be straightforward; the second one may merit more discussion.

Michael Rothgang (Feb 17 2025 at 08:24):

#21947 resurrects an old PR of mine, linting against bare open classical: if we think that is always technical debt, imho we should lint against it.

Kim Morrison (Feb 18 2025 at 03:48):

I've been chipping away at erw this morning, using the new erw? tool.

Kim Morrison (Feb 18 2025 at 03:48):

#22019 fixes some erw to do with AlgEquiv.

Kim Morrison (Feb 18 2025 at 03:48):

#22024 deals with many erw in Lie theory. Perhaps @Oliver Nash would be interested in reviewing and/or looking at the remaining ones! :-)

Kim Morrison (Feb 18 2025 at 03:48):

#22025 is just a grab bag from several files

Kim Morrison (Feb 18 2025 at 03:49):

#22026 deals with most of the erw in Polynomial. @Damiano Testa, there's one remaining erw in the Laurent file that you wrote, which I can't work out yet.

Kim Morrison (Feb 18 2025 at 03:52):

But it's really the ones in AlgebraicGeometry/ and AlgebraicTopology/ that I'm worried about, and want to make progress on.

Kim Morrison (Feb 18 2025 at 05:38):

#22028 makes epsilon progress in AlgebraicGeometry.

Damiano Testa (Feb 18 2025 at 07:35):

Kim Morrison said:

#22026 deals with most of the erw in Polynomial. Damiano Testa, there's one remaining erw in the Laurent file that you wrote, which I can't work out yet.

Using

  apply (comapDomain.addMonoidHom_apply Int.ofNat_injective ..).trans

instead of

  erw [comapDomain.addMonoidHom_apply Int.ofNat_injective]

is not good, right?

Ruben Van de Velde (Feb 18 2025 at 08:12):

Yeah, that's worse :)

Ruben Van de Velde (Feb 18 2025 at 08:13):

There's also -4 erw in #22016

github mathlib4 bot (Feb 24 2025 at 04:07):

Current number Change Type
3355 -29 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
104 -2 adaptation notes
109 0 disabled simpNF lints
1306 -27 erw
2 0 maxHeartBeats modifications
91 0 disabled deprecation lints
625 0 documentation nolint entries
43 0 large files
0 -1 bare open (scoped) Classical
4876 0 exceptions for the docPrime linter
11 0 Deprecated files
771 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 5e2e7342a4
Reference commit 6b0da400f1

Anne Baanen (Feb 24 2025 at 15:36):

Some tech debt cleanup in Algebra/Category: #22249

Anne Baanen (Feb 24 2025 at 16:08):

I am now looking at algebraic geometry, and found we can get rid of some erws if we turn docs#AlgebraicGeometry.LocallyRingedSpace.toRingedSpace into an abbrev. Is there an objection to doing so?

Johan Commelin (Feb 25 2025 at 13:23):

I'm not clear on the tradeoffs. Maybe we should just try and learn.

Yury G. Kudryashov (Feb 27 2025 at 00:43):

Is there a guide on debugging why a certain line needs an erw? I'm writing a new code, rw fails, erw works, but I don't understand why.

Floris van Doorn (Feb 27 2025 at 00:55):

erw? landed in core recently, and should be there in the next Mathlib update (I believe), and does exactly that.

Kim Morrison (Feb 27 2025 at 02:22):

Floris van Doorn said:

erw? landed in core recently, and should be there in the next Mathlib update (I believe), and does exactly that.

Actually erw? is just implemented in Mathlib, and is available now.

Kim Morrison (Feb 27 2025 at 02:22):

It will likely later move to Lean.

Kim Morrison (Feb 27 2025 at 11:13):

I've also just made

check_equalities tactic for diagnosing defeq problems #22366

which I'm finding useful when diagnosing defeq problems.

Really we should just make the general purpose tactic that re-infers the type of every function argument, and compares that to the expect type according to the function, and reporting all discrepancies. But for now check_equalities and check_compositions for category theory are useful special cases. I'm a bit worried the UX for the general purpose one might be bad, but we can just try.

github mathlib4 bot (Mar 03 2025 at 04:07):

Current number Change Type
3169 -186 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
104 0 adaptation notes
103 -6 disabled simpNF lints
1265 -41 erw
2 0 maxHeartBeats modifications
104 13 disabled deprecation lints
522 -103 documentation nolint entries
36 -7 large files
0 0 bare open (scoped) Classical
4875 -1 exceptions for the docPrime linter
11 0 Deprecated files
771 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 45a9aacac4
Reference commit 8c8ef3cd84

Damiano Testa (Mar 03 2025 at 08:09):

The docPrime linter is disabled, but an exception was removed?

Ruben Van de Velde (Mar 03 2025 at 08:29):

A previous rename caused a name without a prime to end up in the list of exceptions, which I removed

Damiano Testa (Mar 03 2025 at 08:32):

Manual self-linting: amazing!

github mathlib4 bot (Mar 10 2025 at 04:06):

Current number Change Type
3148 -21 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
96 -8 adaptation notes
103 0 disabled simpNF lints
1219 -46 erw
4 2 maxHeartBeats modifications
95 -9 disabled deprecation lints
510 -12 documentation nolint entries
32 -3 large files
0 0 bare open (scoped) Classical
4875 0 exceptions for the docPrime linter
9 -2 Deprecated files
632 -139 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 63a7be57d4
Reference commit 95c78f355f

Jeremy Tan (Mar 10 2025 at 04:32):

#22754 clears even more docBlame nolints

Jeremy Tan (Mar 10 2025 at 10:06):

#22762 deletes a file which says it has been deprecated since May 2024, but has not been marked with the deprecation tag

Kim Morrison (Mar 10 2025 at 23:50):

#22813 clears the remaining uses of erw from NumberTheory/, with the exception of one in file#NumberTheory/PellMatiyasevic. (@Mario Carneiro, any interest in cleaning up that file, either a complete overhaul or dealing with erw?)

Mario Carneiro (Mar 10 2025 at 23:59):

maybe after the ITP deadline :)

Kim Morrison (Mar 17 2025 at 03:35):

Has there been any progress on all of the -- FIXME There is undeprecated material below still depending on this?! in SetTheory/Ordinal/Arithmetic?

(It seems implausible to me that a CGT repo would be viable if we can't even get things like this cleaned up.)

Kim Morrison (Mar 17 2025 at 03:37):

We discussed this in December, and these deprecations are now otherwise ready for removal (>6 months old).

Violeta Hernández (Mar 17 2025 at 03:39):

Sorry! The CGT repo has been taking away my allocated Lean time.

Violeta Hernández (Mar 17 2025 at 03:40):

As mentioned here, there's essentially only one PR missing before we can remove these definitions. I'll get it working ASAP.

Violeta Hernández (Mar 17 2025 at 03:40):

(We do still need to decide what happens with the game material within Mathlib)

Violeta Hernández (Mar 17 2025 at 03:51):

Dammit! I lied, #19698 is not really ready for review at all. There's a few other dependent PRs I've got to get working first.

Violeta Hernández (Mar 17 2025 at 03:52):

I've got a somewhat extreme solution: what about just deprecating everything that depends on these deprecated functions?

Violeta Hernández (Mar 17 2025 at 03:58):

These are all lemmas and definitions that will have to go at some point anyways. (And if we're being honest, I'm probably the only user for a lot of them)

Violeta Hernández (Mar 17 2025 at 04:00):

The biggest file which is affected is the cofinality file, but once again, I'm trying to refactor this anyways since the current API is missing a lot of important results and is very difficult to work with.

github mathlib4 bot (Mar 17 2025 at 04:07):

Current number Change Type
1814 -1334 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
96 0 adaptation notes
98 -5 disabled simpNF lints
1180 -39 erw
4 0 maxHeartBeats modifications
95 0 disabled deprecation lints
510 0 documentation nolint entries
30 -2 large files
0 0 bare open (scoped) Classical
4874 -1 exceptions for the docPrime linter
9 0 Deprecated files
632 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit d27bbbade6
Reference commit 0d1fc21822

Violeta Hernández (Mar 17 2025 at 04:08):

I realize part of why progress has been so slow is that a bunch of the PRs I've opened over the past two months have rotted. I'll start by fixing that up.

Johan Commelin (Mar 17 2025 at 05:41):

PSA: Big drop in porting notes. Get yours now, before they're gone! While supplies last!

Michael Rothgang (Mar 18 2025 at 10:21):

The openClassicalLinter #21947 ensures bare open Classical statements don't re-occur. It has been on the queue for 29 days overall. Is there any reason not to merge it? @Damiano Testa @Kim Morrison since you both like reviewing linter resp. tech debt PRs.
(This linter itself is not urgent, it would just be nice to land it eventually.)

Michael Rothgang (Mar 18 2025 at 10:22):

(Though it probably makes sense to merge #23019 before 21947.)

Jeremy Tan (Mar 19 2025 at 03:01):

#23082 clears docBlame nolints in category theory (including two related files in Topology)

Jeremy Tan (Mar 19 2025 at 12:45):

Jeremy Tan said:

#22754 clears even more docBlame nolints

(spun off from this)

github mathlib4 bot (Mar 24 2025 at 04:07):

Current number Change Type
1802 -12 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
92 -4 adaptation notes
78 -20 disabled simpNF lints
1138 -37 erw
4 0 maxHeartBeats modifications
82 -13 disabled deprecation lints
492 -18 documentation nolint entries
19 -11 large files
4874 0 exceptions for the docPrime linter
5 -4 Deprecated files
271 -361 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 524e5aa6c2
Reference commit 13a84ccec8

Patrick Massot (Mar 24 2025 at 07:25):

What happened to the porting notes count? Do we really have all those zombie porting notes?

Ruben Van de Velde (Mar 24 2025 at 07:47):

Yeah - we made a lot of progress two weeks ago, but there's a lot left. Often not actionable, but still worth checking them

Patrick Massot (Mar 24 2025 at 07:59):

Oh I understand, I was misreading the table. Please ignore my question.

Patrick Massot (Mar 24 2025 at 08:00):

I thought the 1814 in the table last week was the count before removing 1334 of them. But it was the count after removing.

Johan Commelin (Mar 24 2025 at 08:09):

It was 4824 at the start of the year :sweat_smile:

github mathlib4 bot (Mar 31 2025 at 04:07):

Current number Change Type
1788 -14 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
92 0 adaptation notes
63 -15 disabled simpNF lints
973 -154 erw
4 0 maxHeartBeats modifications
82 0 disabled deprecation lints
415 -77 documentation nolint entries
13 -6 large files
4874 0 exceptions for the docPrime linter
5 0 Deprecated files
271 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit f8f8d42d40
Reference commit 4d2f8ba7d8

Jeremy Tan (Mar 31 2025 at 04:48):

A sizeable number of the 415 remaining documentation nolints are in Mathlib.Control, but I have next to no knowledge of monads. Would someone with that knowledge add the documentation in there?

Jeremy Tan (Mar 31 2025 at 05:36):

Meanwhile, #23474 clears docBlame in Computability and ModelTheory (close enough relation).

Kim Morrison (Mar 31 2025 at 09:49):

Are there files under Mathlib/Control/ which are leaf files (i.e. not transitively imported by anything outside Mathlib/Control/)? We may be able to do some pruning here!

Patrick Massot (Mar 31 2025 at 11:06):

There may be some, but there are definitely import from that folder in mathematical files.

Patrick Massot (Mar 31 2025 at 11:07):

If someone wants to work on those docstrings, I guess there are lots of them we could simply take from the Haskell documentation.

Kim Morrison (Mar 31 2025 at 12:32):

As it's the end of the quarter, I thought I'd post a quick update on technical debt work by the FRO (i.e. @Anne Baanen, @Johan Commelin, and me). In the past three months, we've been working on processing a bunch of technical debt. The result is:

Name Start Current
porting notes 5000 1798
adaptation notes 200 121
disabled simpNF lints 200 65
erw 1500 973
maxHeartBeats modifications 16 4
large files 60 12

All the remaining simpNF nolints have been triaged and checked that they are harmless. We've also worked on import reductions, extending the spine of Defs files. Anne Baanen valiantly refactored concrete categories. Finally, we had a queueboard survey that led to many useful suggestions from the community.

We also thank all the community members that worked on these projects alongside us: reducing technical debt, adding documentation, implementing queueboard features, experimenting with redesigns and reviewing refactors. You know who you are: big kudos!

Kim Morrison (Mar 31 2025 at 12:32):

By my count we've had about 140 PRs labelled tech debt this quarter!

Kim Morrison (Mar 31 2025 at 12:33):

There's still a long way to go here, of course. Particularly for the porting notes and erws, we've been picking the low hanging fruit so far, and the remaining ones are on average probably harder than the ones dealt with so far!

Kim Morrison (Mar 31 2025 at 12:33):

We're planning on continuing on these projects, albeit at a slightly slower pace as there are also other priorities for this quarter.

Jeremy Tan (Mar 31 2025 at 17:37):

Patrick Massot said:

There may be some, but there are definitely import from that folder in mathematical files.

grep gives

Mathlib/Algebra/Free.lean:import Mathlib.Control.Applicative
Mathlib/Algebra/Free.lean:import Mathlib.Control.Traversable.Basic
Mathlib/CategoryTheory/Core.lean:import Mathlib.Control.EquivFunctor
Mathlib/CategoryTheory/Monad/Types.lean:import Mathlib.Control.Basic -- Porting note: Needed for `joinM_map_map`, etc.
Mathlib/Data/DList/Instances.lean:import Mathlib.Control.Traversable.Equiv
Mathlib/Data/DList/Instances.lean:import Mathlib.Control.Traversable.Instances
Mathlib/Data/List/Basic.lean:import Mathlib.Control.Basic
Mathlib/Data/List/Defs.lean:import Mathlib.Control.Functor
Mathlib/Data/Multiset/Functor.lean:import Mathlib.Control.Traversable.Lemmas
Mathlib/Data/Multiset/Functor.lean:import Mathlib.Control.Traversable.Instances
Mathlib/Data/Option/Basic.lean:import Mathlib.Control.Combinators
Mathlib/Data/PFunctor/Multivariate/Basic.lean:import Mathlib.Control.Functor.Multivariate
Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean:import Mathlib.Control.Functor.Multivariate
Mathlib/Data/QPF/Multivariate/Constructions/Const.lean:import Mathlib.Control.Functor.Multivariate
Mathlib/Data/QPF/Multivariate/Constructions/Prj.lean:import Mathlib.Control.Functor.Multivariate
Mathlib/Data/Set/Functor.lean:import Mathlib.Control.Basic
Mathlib/Data/Tree/Traversable.lean:import Mathlib.Control.Applicative
Mathlib/Data/Tree/Traversable.lean:import Mathlib.Control.Traversable.Basic
Mathlib/Data/ULift.lean:import Mathlib.Control.ULift
Mathlib/Data/Vector/Basic.lean:import Mathlib.Control.Applicative
Mathlib/Data/Vector/Basic.lean:import Mathlib.Control.Traversable.Basic
Mathlib/Logic/Equiv/Functor.lean:import Mathlib.Control.Bifunctor
Mathlib/Logic/Equiv/Option.lean:import Mathlib.Control.EquivFunctor
Mathlib/Order/Filter/ListTraverse.lean:import Mathlib.Control.Traversable.Instances
Mathlib/Order/Filter/Map.lean:import Mathlib.Control.Basic
Mathlib/Order/OmegaCompletePartialOrder.lean:import Mathlib.Control.Monad.Basic
Mathlib/Probability/ProbabilityMassFunction/Constructions.lean:import Mathlib.Control.ULiftable
Mathlib/Tactic/DeriveTraversable.lean:import Mathlib.Control.Traversable.Lemmas
Mathlib/Tactic/IntervalCases.lean:import Mathlib.Control.Basic
Mathlib/Tactic/Linarith/Frontend.lean:import Mathlib.Control.Basic
Mathlib/Tactic/Linarith/Preprocessing.lean:import Mathlib.Control.Basic
Mathlib/Tactic/Positivity/Core.lean:import Mathlib.Control.Basic

Johan Commelin (Apr 01 2025 at 05:46):

  • chore(LinearAlgebra/AffineSpace): process porting notes #23505

Johan Commelin (Apr 01 2025 at 07:25):

  • chore(LinearAlgebra/Matrix): process porting notes #23524

13 files changed, 30 insertions(+), 60 deletions(-)

Johan Commelin (Apr 01 2025 at 08:06):

  • chore(LinearAlgebra/CliffordAlgebra): process some porting notes #23526

4 files changed, 15 insertions(+), 42 deletions(-)

Johan Commelin (Apr 01 2025 at 12:54):

  • chore(LinearAlgebra/LinearPMap): process porting notes #23538

1 file changed, 27 insertions(+), 41 deletions(-)

Johan Commelin (Apr 01 2025 at 15:02):

  • chore(LinearAlgebra/*): process misc porting notes #23551

12 files changed, 73 insertions(+), 99 deletions(-)

Johan Commelin (Apr 04 2025 at 10:52):

  • chore(LinearAlgebra/Alternating): process porting notes #23664

3 files changed, 43 insertions(+), 73 deletions(-)

Robin Carlier (Apr 06 2025 at 12:16):

  • chore(CategoryTheory/Equivalence): simp lemmas for co/unit naturality #23724

There are 7 erw left in file#CategoryTheory/Equivalence, but I have to admit I don’t understand well enough what are considered "good" ways to remove erws: for instance

@[reassoc (attr := simp)]
theorem counitInv_functor_comp (e : C ≌ D) (X : C) :
    e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X) := by
  erw [Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X))
      (Iso.refl _)]
  exact e.functor_unit_comp X

can be replaced by 

@[reassoc (attr := simp)]
theorem counitInv_functor_comp (e : C ≌ D) (X : C) :
    e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X) :=
  Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X))
      (Iso.refl _)|>.mpr <| e.functor_unit_comp X

but is that acually better in any way? In both cases, I feel like this is forcing unification of
(e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)).inv and e.functor.map (e.unitInv.app X) ≫ e.counitInv.app (e.functor.obj X), and I remember reading that we don’t want to replace erws by things that "blast through unification" the same way.

Eric Wieser (Apr 07 2025 at 00:16):

Michael Rothgang said:

The openClassicalLinter #21947 ensures bare open Classical statements don't re-occur.

It looks like attribute [local instance] Classical.propDecidable has now been occuring instead! I removed a few of these in #23750

Kim Morrison (Apr 07 2025 at 01:31):

Robin Carlier said:

  • chore(CategoryTheory/Equivalence): simp lemmas for co/unit naturality #23724

There are 7 erw left in file#CategoryTheory/Equivalence, but I have to admit I don’t understand well enough what are considered "good" ways to remove erws: for instance

@[reassoc (attr := simp)]
theorem counitInv_functor_comp (e : C ≌ D) (X : C) :
    e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X) := by
  erw [Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X))
      (Iso.refl _)]
  exact e.functor_unit_comp X

can be replaced by 

@[reassoc (attr := simp)]
theorem counitInv_functor_comp (e : C ≌ D) (X : C) :
    e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X) :=
  Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X))
      (Iso.refl _)|>.mpr <| e.functor_unit_comp X

but is that acually better in any way? In both cases, I feel like this is forcing unification of
(e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)).inv and e.functor.map (e.unitInv.app X) ≫ e.counitInv.app (e.functor.obj X), and I remember reading that we don’t want to replace erws by things that "blast through unification" the same way.

What does erw? say?

github mathlib4 bot (Apr 07 2025 at 04:07):

Current number Change Type
1676 -111 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
129 37 adaptation notes
38 -25 disabled simpNF lints
959 -14 erw
7 3 maxHeartBeats modifications
69 -13 disabled deprecation lints
366 -49 documentation nolint entries
8 -4 large files
4873 -1 exceptions for the docPrime linter
5 0 Deprecated files
557 286 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit bdd987365c
Reference commit 01dba5e821

Robin Carlier (Apr 07 2025 at 06:15):

Kim Morrison said:

What does erw? say?

❌️ at reducible transparency,
  𝟙 (e.functor.obj X)
and
  Iso.inv (Iso.refl (e.functor.obj (Prefunctor.obj.{v₁ + 1, v₁ + 1, u₁, u₁} (toPrefunctor (𝟭 C)) X)))
are not defeq, but they are at default transparency.

Not what I thought it would. Does that mean that what is needed is actually lemmas about Iso.inv (Iso.refl _)?

Kim Morrison (Apr 07 2025 at 07:05):

(Those lemmas presumably exist: they just need to be used here.)

Kim Morrison (Apr 07 2025 at 07:06):

Most of the new adaptation notes in this week's technical debt report are consequences of @Kyle Miller's substantial structure refactor. He's going to think further about these notes, still.

Yaël Dillies (Apr 07 2025 at 07:07):

Eric Wieser said:

Michael Rothgang said:

The openClassicalLinter #21947 ensures bare open Classical statements don't re-occur.

It looks like attribute [local instance] Classical.propDecidable has now been occuring instead! I removed a few of these in #23750

Where there's a decl there's a way

Yaël Dillies (Apr 07 2025 at 07:08):

Kim Morrison said:

Most of the new adaptation notes in this week's technical debt report are consequences of Kyle Miller's substantial structure refactor. He's going to think further about these notes, still.

What about the maxHeartbeats changes?

Kim Morrison (Apr 07 2025 at 07:20):

Those I don't recall, sorry!

Michael Rothgang (Apr 07 2025 at 07:49):

Yaël Dillies said:

Eric Wieser said:

Michael Rothgang said:

The openClassicalLinter #21947 ensures bare open Classical statements don't re-occur.

It looks like attribute [local instance] Classical.propDecidable has now been occuring instead! I removed a few of these in #23750

Where there's a decl there's a way

#23763 extends the openClassical linter accordingly. (I've scoped it narrowly; if further lemmas (or, e.g., anything in the Classical namespace) should be linted, that'll be easy to change.)

Johan Commelin (Apr 07 2025 at 08:11):

Yaël Dillies said:

What about the maxHeartbeats changes?

Kim Morrison said:

Those I don't recall, sorry!

Can we enforce in linting/type-checking that every set_option maxHeartbeats comes with a comment or adaptation note?

Damiano Testa (Apr 07 2025 at 08:12):

It would probably be easier to have a separate command that under the hood sets the option and takes a mandatory string as argument.

Damiano Testa (Apr 07 2025 at 08:12):

After that, you can lint for set_option maxHeartbeats not existing.

Damiano Testa (Apr 07 2025 at 08:13):

something like maxHeartbeats 0 "Because otherwise it times out" in ....

Robin Carlier (Apr 07 2025 at 08:15):

Robin Carlier said:

Kim Morrison said:

What does erw? say?

❌️ at reducible transparency,
  𝟙 (e.functor.obj X)
and
  Iso.inv (Iso.refl (e.functor.obj (Prefunctor.obj.{v₁ + 1, v₁ + 1, u₁, u₁} (toPrefunctor (𝟭 C)) X)))
are not defeq, but they are at default transparency.

Not what I thought it would. Does that mean that what is needed is actually lemmas about Iso.inv (Iso.refl _)?

Re this: it seems that following the erw? trail leads to a proof like 

@[reassoc (attr := simp)]
theorem counitInv_functor_comp (e : C ≌ D) (X : C) :
    e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X) := by
  haveI := Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X))
      (Iso.refl _)
  dsimp only [id_obj, comp_obj, Iso.trans_inv, Iso.app_inv, mapIso_inv, Iso.refl_inv, Iso.trans_hom,
    mapIso_hom, Iso.app_hom, Iso.refl_hom] at this
  exact this.mpr <| e.functor_unit_comp X

Is that considered an "acceptable" replacement for the erw above? Sorry to clutter the discussion a bit, but I’d like to make sure I don’t PR something that ends up replacing erws by something worse in terms of perfs (I’m mainly asking because of the use of haveI here, which I have no idea about its perfs).

Johan Commelin (Apr 07 2025 at 08:20):

Untested, but I would try to write the proof something like this:

theorem counitInv_functor_comp (e : C ≌ D) (X : C) :
    e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X) := by
  suffices /- the type of `this` between your `dsimp` and `exact` lines -/ from
    this.mpr <| e.functor_unit_comp X
  simpa using Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X))
      (Iso.refl _)

Robin Carlier (Apr 07 2025 at 08:25):

Actually, simpa even works directly here.

Damiano Testa (Apr 07 2025 at 08:26):

Something like this?

import Lean

macro "maxHeartbeats " n:num ppSpace _descr:str &" in " cmd:command : command =>
  `(command| set_option maxHeartbeats $n in $cmd)

maxHeartbeats 1 "hello" in
example : True := trivial

Damiano Testa (Apr 07 2025 at 08:26):

It is suboptimal that it would suggest to use set_option maxHeartbeats, since that one would then be linted against, but the linter message would suggest using maxHeartbeats instead.

Damiano Testa (Apr 07 2025 at 08:33):

Or

macro _d:docComment " maxHeartbeats " n:num &" in " cmd:command : command =>
  `(command| set_option maxHeartbeats $n in $cmd)

/-- hello -/
maxHeartbeats 1 in
example : True := trivial

if a doc-string is preferred.

Robin Carlier (Apr 07 2025 at 09:08):

  • chore(CategoryTeory/Equivalence): remove some erws #23764

Robin Carlier (Apr 07 2025 at 09:59):

  • chore(CategoryTheory/ChosenFiniteProducts/FunctorCategory): simp lemmas and erw #23766 (+21/−14)

Kim Morrison (Apr 08 2025 at 05:16):

Damiano Testa said:

something like maxHeartbeats 0 "Because otherwise it times out" in ....

I'd really prefer not to introduce new commands like this. It fractures the ecosystem and makes things harder to learn. Better that the linter writers jump through the hoops, instead of the users!

Damiano Testa (Apr 08 2025 at 06:01):

Ok, so I think that if the comment comes "inside" the set_option ..., then linting it is easy.

Damiano Testa (Apr 08 2025 at 06:03):

So, without having tried it, I suspect that a linter can easily pick up if the comment below is present or not:

set_option maxHeartbeats in
-- I can be linted
....

Damiano Testa (Apr 08 2025 at 06:04):

Putting the comment before the command, means that it gets embedded in the syntax of the previous command and then linting is hard.

Damiano Testa (Apr 08 2025 at 09:59):

#23816 adds linting for uncommented set_option maxHeartbeats n in ....

Damiano Testa (Apr 08 2025 at 11:03):

Damiano Testa said:

#23816 adds linting for uncommented set_option maxHeartbeats n in ....

Should also synthInstance.maxHeartbeats be similarly linted?

Damiano Testa (Apr 08 2025 at 12:29):

In the current iteration, if there are (possibly nested) set_options whose option name contains maxHeartbeats as a component, then the linter will emit a warning unless the outermost set_option has a comment.

Damiano Testa (Apr 08 2025 at 12:29):

This seems better than requiring all set_options to have their own comment, although the linter does not prevent more comments, if so desired.

Damiano Testa (Apr 08 2025 at 12:31):

I also preferred this to the alternative of having at least one comment, though possibly not on the first one. This is probably a matter of personal taste, but the implementation was easier with the current choice and I went for it.

Michael Rothgang (Apr 12 2025 at 10:39):

#23902 adds a linter for bare set_option maxHeartsbeats (or synthInstance.maxHeartbeats) - on the grounds that we presumably prefer set_option ... in instead. The implementation is straightforward and was already approved. Do you think this is a good idea?

Michael Rothgang (Apr 13 2025 at 07:35):

Extending the openClassical linter at #23763 pointed out an interesting case: Topology/MetricSpace/GromovHausdorffRealised uses a attribute [local instance 10] Classical.inhabited_of_nonempty' pervasively in its proof; using open scoped Classical does not work as a fix. Is that a case of "technical debt, please fix" or "actually, this pattern is fine"?

Michael Rothgang (Apr 13 2025 at 07:36):

(All other occurrences of attribute [{local,scoped} instance Classical.something] in mathlib are easily removable.)

Kyle Miller (Apr 13 2025 at 18:34):

Relevant thread about open scoped Classical: #mathlib4 > `by classical exact foo` vs `open scoped Classical in foo` @ 💬.

Eric was suggesting changing the classical ... tactic to do open scoped Classical in ... here. I'm wondering if the priority of the classical decidable instances should be lowered, given your evidence.

Eric Wieser (Apr 13 2025 at 18:48):

It almost certainly should be 10 not 100; it seems very unlikely you would ever want something lower priority than it

Eric Wieser (Apr 13 2025 at 21:32):

I opened lean4#7948

Kim Morrison (Apr 14 2025 at 02:12):

Please ping me if/when this is working.

github mathlib4 bot (Apr 14 2025 at 04:07):

Current number Change Type
1588 -85 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
122 -7 adaptation notes
38 0 disabled simpNF lints
920 -38 erw
7 0 maxHeartBeats modifications
96 27 disabled deprecation lints
366 0 documentation nolint entries
3 -5 large files
4873 0 exceptions for the docPrime linter
5 0 Deprecated files
557 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit 2ccecc0e99
Reference commit e1a7a7f3aa

Kim Morrison (Apr 14 2025 at 06:04):

Still looking good, pity about the regression in disabled deprecation lints. Do we know where that came from?

Yaël Dillies (Apr 14 2025 at 06:08):

Are these not the set_option linter.deprecated false in coming from #20676 ?

Kim Morrison (Apr 14 2025 at 06:12):

Ah, we never fixed this counter to ignore setting the option on something that is deprecated anyway. That's what we really want.

Johan Commelin (Apr 14 2025 at 09:55):

#24031 tries to fix this. We were already looking ahead 1 line. Now we look ahead 2 lines.
Since this is al regex based, there will always be false positives, if you have a longer docstring in-between.

Johan Commelin (Apr 14 2025 at 09:55):

Maybe this is good enough for now.

Damiano Testa (Apr 14 2025 at 10:10):

I am going to re-trigger the summary to test the effect of the change.

github mathlib4 bot (Apr 14 2025 at 10:11):

Current number Change Type
1588 -70 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
122 -7 adaptation notes
38 0 disabled simpNF lints
920 -27 erw
7 0 maxHeartBeats modifications
73 27 disabled deprecation lints
366 0 documentation nolint entries
3 -5 large files
4873 0 exceptions for the docPrime linter
5 0 Deprecated files
557 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit dcefb86ae9
Reference commit 11f405a5d1

Yaël Dillies (Apr 14 2025 at 10:13):

Nope, that's not it then

Damiano Testa (Apr 14 2025 at 10:15):

The current number did decrease by 23 which may be compatible with the 27 difference: maybe there is a sign error on one "subtraction"?

Damiano Testa (Apr 14 2025 at 10:16):

(Note that the mechanism for counting the excess is a little hacky, so I am viewing 23 as approximately equal to 27, modulo the hack.)

Kevin Buzzard (Apr 15 2025 at 08:27):

Michael Rothgang said:

Extending the openClassical linter at #23763 pointed out an interesting case: Topology/MetricSpace/GromovHausdorffRealised uses a attribute [local instance 10] Classical.inhabited_of_nonempty' pervasively in its proof; using open scoped Classical does not work as a fix. Is that a case of "technical debt, please fix" or "actually, this pattern is fine"?

The problem seems to be this definition (metric space structure on the disjoint union of two metric spaces):

/-- Distance on a disjoint union. There are many (noncanonical) ways to put a distance compatible
with each factor.
If the two spaces are bounded, one can say for instance that each point in the first is at distance
`diam X + diam Y + 1` of each point in the second.
Instead, we choose a construction that works for unbounded spaces, but requires basepoints,
chosen arbitrarily.
We embed isometrically each factor, set the basepoints at distance 1,
arbitrarily, and say that the distance from `a` to `b` is the sum of the distances of `a` and `b` to
their respective basepoints, plus the distance 1 between the basepoints.
Since there is an arbitrary choice in this construction, it is not an instance by default. -/
protected def Sum.dist : X ⊕ Y → X ⊕ Y → ℝ
  | .inl a, .inl a' => dist a a'
  | .inr b, .inr b' => dist b b'
  | .inl a, .inr b => dist a (Nonempty.some ⟨a⟩) + 1 + dist (Nonempty.some ⟨b⟩) b
  | .inr b, .inl a => dist b (Nonempty.some ⟨b⟩) + 1 + dist (Nonempty.some ⟨a⟩) a

which crucially uses Classical.some. It's not an instance by default but the line attribute [local instance] metricSpaceSum switches it on in the file. (It's Topology/MetricSpace/GromovHausdorffRealized with a z by the way)

Kevin Buzzard (Apr 15 2025 at 08:42):

You can fix the proofs by just putting lines like

  letI : Inhabited S := Classical.inhabited_of_nonempty inferInstance

in them. Do people understand why classical is not doing this?

Yaël Dillies (Apr 15 2025 at 08:46):

Kevin, your line is equivalent to inhabit S

Edward van de Meent (Apr 15 2025 at 08:49):

that's an unusually specific tactic

Johan Commelin (Apr 15 2025 at 08:50):

I wish that tactic would take a name as argument. So that you can write inhabit S with s.

Johan Commelin (Apr 15 2025 at 08:50):

Where s would be notation/abbrev/let for default

Yaël Dillies (Apr 15 2025 at 08:50):

We also have nontriviality along these lines

Edward van de Meent (Apr 15 2025 at 08:50):

isn't that just like choose s : S or something then?

Yaël Dillies (Apr 15 2025 at 08:52):

choose doesn't work if you want a single thing out of it. Arguably, that's an oversight

Kevin Buzzard (Apr 15 2025 at 08:55):

Yaël Dillies said:

Kevin, your line is equivalent to inhabit S

Sure, but that's not my question. My question is why classical doesn't work.

Michael Rothgang (Apr 15 2025 at 09:42):

Using inhabit indeed allows removing some uses of that instance --- but not all.

Michael Rothgang (Apr 15 2025 at 09:43):

Here is a not-quite-minimal version of the error: the version with Classical.inhabited_of_nonempty' a local instance works, but merely omitting that an asking for Inhabited spaces fails. (Asking for Nonempty and using inhabit also fails.) Details:

-- Minimised from GromovHausdorffRealised.lean
import Mathlib.Topology.ContinuousMap.Bounded.Normed
import Mathlib.Topology.MetricSpace.Gluing

open NNReal Set Metric
open Sum (inl inr)

attribute [local instance] metricSpaceSum

variable (X Y : Type*) [MetricSpace X] [MetricSpace Y]

private noncomputable def maxVar : ℝ≥0 :=
  2 * ⟨diam (univ : Set X), diam_nonneg⟩ + 1 + 2 * ⟨diam (univ : Set Y), diam_nonneg⟩

private theorem one_le_maxVar : 1 ≤ maxVar X Y := sorry -- omitted

variable {X : Type*} {Y : Type*} [MetricSpace X] [MetricSpace Y] [CompactSpace X] [CompactSpace Y]
  {x y z t : X ⊕ Y}

-- This version works.
attribute [local instance 10] Classical.inhabited_of_nonempty' in
private theorem maxVar_bound [Nonempty X] [Nonempty Y] : dist x y ≤ maxVar X Y := by
  calc
    dist x y ≤ diam (univ : Set (X ⊕ Y)) :=
      dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)
    _ = diam (range inl ∪ range inr : Set (X ⊕ Y)) := by rw [range_inl_union_range_inr]
    _ ≤ diam (range inl : Set (X ⊕ Y)) + dist (inl default) (inr default) +
        diam (range inr : Set (X ⊕ Y)) :=
      (diam_union (mem_range_self _) (mem_range_self _))
    _ = diam (univ : Set X) + (dist (α := X) default default + 1 + dist (α := Y) default default) +
        diam (univ : Set Y) := by
      rw [isometry_inl.diam_range, isometry_inr.diam_range]
      rfl
    _ = 1 * diam (univ : Set X) + 1 + 1 * diam (univ : Set Y) := by simp
    _ ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by gcongr <;> norm_num

-- Removing the local instance, but asking for Inhabited fails. Why?
private theorem maxVar_bound_fails [Inhabited X] [Inhabited Y] : dist x y ≤ maxVar X Y := by calc
    dist x y ≤ diam (univ : Set (X ⊕ Y)) :=
      dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)
    _ = diam (range inl ∪ range inr : Set (X ⊕ Y)) := by rw [range_inl_union_range_inr]
    _ ≤ diam (range inl : Set (X ⊕ Y)) + dist (inl default) (inr default) +
        diam (range inr : Set (X ⊕ Y)) :=
      (diam_union (mem_range_self _) (mem_range_self _))
    _ = diam (univ : Set X) + (dist (α := X) default default + 1 + dist (α := Y) default default) +
        diam (univ : Set Y) := by
      rw [isometry_inl.diam_range, isometry_inr.diam_range]
      /- This line errors with:
      tactic 'rfl' failed, the left-hand side
        diam univ + dist (inl default) (inr default) + diam univ
      is not definitionally equal to the right-hand side
        diam univ + (dist default default + 1 + dist default default) + diam univ -/
      sorry -- rfl
    _ = 1 * diam (univ : Set X) + 1 + 1 * diam (univ : Set Y) := by simp
    _ ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by gcongr <;> norm_num

-- Using the inhabit tactic shows the same error.
private theorem maxVar_bound_fails2 [Nonempty X] [Nonempty Y] : dist x y ≤ maxVar X Y := by
  inhabit X; inhabit Y
  calc
    dist x y ≤ diam (univ : Set (X ⊕ Y)) :=
      dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)
    _ = diam (range inl ∪ range inr : Set (X ⊕ Y)) := by rw [range_inl_union_range_inr]
    _ ≤ diam (range inl : Set (X ⊕ Y)) + dist (inl default) (inr default) +
        diam (range inr : Set (X ⊕ Y)) :=
      (diam_union (mem_range_self _) (mem_range_self _))
    _ = diam (univ : Set X) + (dist (α := X) default default + 1 + dist (α := Y) default default) +
        diam (univ : Set Y) := by
      rw [isometry_inl.diam_range, isometry_inr.diam_range]
      /- This line errors with:
      tactic 'rfl' failed, the left-hand side
        diam univ + dist (inl default) (inr default) + diam univ
      is not definitionally equal to the right-hand side
        diam univ + (dist default default + 1 + dist default default) + diam univ -/
      sorry -- rfl
    _ = 1 * diam (univ : Set X) + 1 + 1 * diam (univ : Set Y) := by simp
    _ ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by gcongr <;> norm_num

Kevin Buzzard (Apr 15 2025 at 10:43):

These errors are because you're still using Sum.dist which uses choice rather than Inhabited.

Kevin Buzzard (Apr 15 2025 at 10:46):

So rfl is failing because the proof is using both the given and the classical Inhabited instances.

Michael Rothgang (Apr 17 2025 at 14:45):

Review ping on #23909 --- which fixes various warnings by the (off-by-default) flexible linter. I can split the diff (+120/-80) if preferred.

github mathlib4 bot (Apr 21 2025 at 04:07):

Current number Change Type
1586 -2 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
122 0 adaptation notes
38 0 disabled simpNF lints
919 -1 erw
7 0 maxHeartBeats modifications
74 1 disabled deprecation lints
366 0 documentation nolint entries
0 -3 large files
4873 0 exceptions for the docPrime linter
6 1 Deprecated files
737 180 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit dc4f49f1f4
Reference commit 71d3df641b

Jeremy Tan (Apr 21 2025 at 04:27):

#24238 clears the next batch of >6 month old deprecations

Michael Rothgang (Apr 22 2025 at 12:36):

#24109 adds an allow-list mechanism to the directoryDependency linter. This is task 14 in this list.

github mathlib4 bot (Apr 28 2025 at 04:08):

Current number Change Type
1573 -13 porting notes
0 0 backwards compatibility flags
0 0 skipAssignedInstances flags
122 0 adaptation notes
38 0 disabled simpNF lints
915 -4 erw
7 0 maxHeartBeats modifications
70 -4 disabled deprecation lints
366 0 documentation nolint entries
0 0 large files
4870 -3 exceptions for the docPrime linter
6 0 Deprecated files
737 0 total LoC in Deprecated files

Changed 'Deprecated' lines by file

Current commit ff8f7874ef
Reference commit 72dd74b29e

Johan Commelin (Apr 28 2025 at 11:18):

With porting notes, I've been focussing on LinearAlgebra/ and Order/.

For example, there are only 38 porting notes left in LinearAlgebra/:

$ rg -i "porting note" Mathlib/LinearAlgebra | sed 's|\(Mathlib/LinearAlgebra/[^/]*\)/.*|\1|' | sort | uniq -c
      1 Mathlib/LinearAlgebra/AffineSpace
      8 Mathlib/LinearAlgebra/CliffordAlgebra
      1 Mathlib/LinearAlgebra/Contraction.lean:-- Porting note: we need high priority for this to fire first; not the case in ML3
      1 Mathlib/LinearAlgebra/Dimension
      1 Mathlib/LinearAlgebra/Dual
      2 Mathlib/LinearAlgebra/Finsupp
      5 Mathlib/LinearAlgebra/LinearIndependent
      1 Mathlib/LinearAlgebra/LinearPMap.lean:    -- Porting note: This is just
      7 Mathlib/LinearAlgebra/Matrix
      1 Mathlib/LinearAlgebra/Multilinear
      2 Mathlib/LinearAlgebra/Prod.lean:  -- Porting note: proofs were `tidy` or `simp`
      1 Mathlib/LinearAlgebra/Projection.lean:    -- Porting note: type ascriptions needed on the RHS
      1 Mathlib/LinearAlgebra/Projection.lean:@[simp, nolint simpNF] -- Porting note: linter claims that LHS doesn't simplify, but it does
      3 Mathlib/LinearAlgebra/QuadraticForm
      1 Mathlib/LinearAlgebra/Quotient
      2 Mathlib/LinearAlgebra/TensorAlgebra

Notification Bot (Apr 28 2025 at 14:52):

3 messages were moved from this topic to #mathlib4 > simpNF lint with hyps by Johan Commelin.

Johan Commelin (May 01 2025 at 06:21):

refactor(Order/Heyting): convert toBiheytingHomClass from lemma to instance #24437

Johan Commelin (May 01 2025 at 06:22):

chore(Order): process misc porting notes #24431

Michael Rothgang (May 01 2025 at 09:08):

#24492 removes a few adaptation notes: I had three questions about specific changes, where a second opinion would be helpful.

Last updated: May 02 2025 at 03:31 UTC