Mathlib4 porting meeting series

Stream: mathlib4

[Mario Carneiro]

Hello all, we're planning on having a public weekly meeting for mathlib4 porting efforts, to replace the mentee meeting for discussing tactic development. It takes place on Thursdays starting 2022-11-10T12:00:00-05:00. The hope is to get both people working on porting mathlib files as well as those porting tactics, and get some cross-communication going, iron out mathport kinks and so on.

https://meet.jit.si/moderated/a58c9883e1b3ef01acd9989d4626b2579d5263d496cacf6e5f3f917699ecb994

[Mario Carneiro]

(We can also use this thread for meeting notes going forward.)

[Sarah Smith]

@mathlib mentees

[Moritz Doll]

Are there other people interested in the meeting that would prefer a different time? It is at 4 in the night for me, but if I am the only person that cannot make it then it does not make sense to have a second meeting.

[Mauricio Collares]

Note that the above widget already shows local time (corresponding to 17:00 UTC in this case).

Edit: Oh, you're in Victoria. Nice! The list of time zones I looked at ignored daylight saving time, so I missed Australia.

[Moritz Doll]

I know

[Kevin Buzzard]

This clashes with Xena for me. (but I was going to experiment with trying to go and also help UGs at the same time...)

[Scott Morrison]

If it was a slightly more Australia compatible time (e.g. starting at least two hours later, or four hours earlier), I would come.

[Johan Commelin]

Four hours earlier or 2 hours later would also be more comfy for me. Right now it clashes with dinner + kids bed time.

[Thomas Murrills]

2 hours or more later would be comfortable for me, but I wouldn’t be able to make four hours earlier.

[Mario Carneiro]

I'm inclined to move to 2022-11-10T14:00:00-05:00 if that's better then, it would be good to see some new faces. Let's do a poll to confirm (vote for all options you think you can come to):

[Mario Carneiro]

/poll Let's do the meeting at...
2022-11-10T08:00:00-05:00
2022-11-10T10:00:00-05:00
2022-11-10T12:00:00-05:00
2022-11-10T14:00:00-05:00
2022-11-10T16:00:00-05:00

[Mario Carneiro]

Well that didn't work. For reference the times are: -4, -2, 0, +2, +4 hours from the current 2022-11-10T12:00:00-05:00 meeting time.

[Kevin Buzzard]

(In general I can do current time -2 but I have a meeting tomorrow)

[David Renshaw]

@Mario Carneiro is there a final decision about the meeting time tomorrow? If it's "-4" then I need to make sure not to sleep too late. :)

[Mario Carneiro]

Let's meet 2022-11-10T16:00:00-05:00, there are surprisingly many Europeans okay with that time and it's a bit easier for the Americans. Apparently every time is better than what we are doing now...

[Mario Carneiro]

(Sorry for the late notice!)

[Riccardo Brasca]

Will the meeting be recorded?

[Mario Carneiro]

uh, dunno I've never tried that with jitsi but I don't mind. This is a weekly meeting, so I don't want it to be too much hassle to post on youtube, and it's more of a meeting than a presentation so the main benefit would be automating the meeting notes

[Scott Morrison]

A recording (apologies for the erratic audio levels) will be available later today at https://youtu.be/0nGwjhi6UlI.

[Scott Morrison]

Are we meeting again at 2022-11-18T08:00:00+11:00?

[Scott Morrison]

I made the bump PR for mathlib4, at mathlib4#624, but there are two places where we might want to find out what went wrong, rather than just paper over a broken proof.

[Scott Morrison]

I'm off to sleep now, but can look again in the morning if it hasn't already been done. I'm excited to have the Lean 4 fixes in so we can proceed on a few porting PRs!

[Alex J. Best]

Scott Morrison said:

I made the bump PR for mathlib4, at mathlib4#624, but there are two places where we might want to find out what went wrong, rather than just paper over a broken proof.

Did you record / report these somewhere else, seeing as 624 is merged they may be forgotten otherwise

[Mario Carneiro]

I reviewed / fixed the proof

[Mario Carneiro]

the short answer is that simp got a bit less powerful in the latest nightly, because it no longer does iota reduction when matching input facts against subterms in the goal

[Mario Carneiro]

I think this is a good thing, or at least explainable, because they don't really look like they would match

[Mario Carneiro]

it is fixed in most cases by doing dsimp only at h; simp [h] where simp [h] was being used before

[Mario Carneiro]

for example if h : ULift.down (ULift.up x) = y, then simp [h] on P x does not result in P y even though it used to, but dsimp only at h; simp [h] will work

[Alex J. Best]

Okay yeah that makes sense, doesn't sound like too much of a loss indeed

[Yaël Dillies]

Isn't that used quite often actually? At least I have the habit of swallowing up dsimp calls into simp ones.

[Yaël Dillies]

That also means simp isn't strictly more powerful than dsimp anymore, right? We really should make a warning about that, then.

[Patrick Massot]

I'm not sure I'll be able to come to the meeting today, but I'd be interested to know whether last week I was the only one who had a lot of trouble hearing what Mario was saying. Basically I had to guess a lot of pieces of sentences that got cut. If I'm not the only one then it would be nice to figure out a way to have a better internet connexion for Mario today.

[Johan Commelin]

I think zoom is generally better than jitsi when it comes to meetings with > N participants.

[Patrick Massot]

I also want to say that it would be very nice for the port effort to put more energy into documenting the new naming conventions and porting tricks.

[Mario Carneiro]

The audio was being picked up by the hoskinson center room mic last time. I will be at home today and using my mic so the audio should be better. Can't say the same about the internet, this seems to be a plague that follows me around

[Patrick Massot]

Are there planned topics of discussion for today?

[Mario Carneiro]

no, we can spend the first 5 minutes working things out, or you can post agenda items here

[Patrick Massot]

If you don't have other ideas, I suggest:

• do a live file porting and making sure for each name issue that https://github.com/leanprover-community/mathlib4/wiki#naming-convention gives a clear answer (unless it's a very special case), edit that file if it doesn't
• do a live mathlib4 PR review, making sure that each issue could have been avoided using the wiki page, edit the wiki page if needed

If editing the wiki page is too slow we could have people volunteering to do the editing work while you continue live coding/reviewing. Those are only suggestions, I don't the perfect way of making porting easier

[Eric Wieser]

I'd be interested in hearing what our current "stop mathlib3 and mathlib4 going out of sync" plan is, and whether there is any CI in the works to aid with that (and if not, what would be useful for me or others to build)

[Eric Wieser]

(@Yakov Pechersky seems to either have something in mind, or some foundations, at https://github.com/leanprover-community/mathlib-tools/pull/137)

[Yakov Pechersky]

Unfortunately I won't be able to attend today

[Eric Wieser]

Is the intent for the meeting link in the top post to be reused?

[Mario Carneiro]

https://meet.jit.si/moderated/a58c9883e1b3ef01acd9989d4626b2579d5263d496cacf6e5f3f917699ecb994

[Mario Carneiro]

yes

[Scott Morrison]

Alex J. Best said:

Did you record  / report these somewhere else, seeing as 624 is merged they may be forgotten otherwise
````
Mario already fixed these in the PR.

[Alex J. Best]

Oh yeah sorry we had a whole conversation about it but it got moved to https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/dsimp.20and.20simp/near/310616043

[Scott Morrison]

TODO list items from after the mathlib4 porting meeting.

[Scott Morrison]

1. explain in the wiki where to find the mathlib3 sha, and where to put it in your mathlib4 PR

[Scott Morrison]

2. write a wiki section about Lean 4 coercions

[Scott Morrison]

3. write a wiki section explaining OfNat.ofNat vs. Nat.cast

[Scott Morrison]

4. scripts/port_status.py should show the git diff for files that have been modified since their recorded sha (presumably this should be controlled by a flag)

[Scott Morrison]

5. scripts/port_status.py should work regardless of which directory it is run from

[Scott Morrison]

6. CI action for mathlib3 that detects changes to any file containing a mathlib4 synchronization message, and adds a label to the PR.

[Scott Morrison]

7. Currently new files in mathlib3 are only added to #port-status either manually, or if someone copy-pastes the output of port_status.yaml (automatically generated in the current directory when you run scripts/port-status.py) back into the wiki. Either automate this, or decide how to manage this.

[Scott Morrison]

8. CI that watches for mathlib4 PRs marked with the mathlib-port label being merged, then automatically creates a PR to mathlib3 adding the synchronization label to the corresponding files.

[Scott Morrison]

9. Switch to the new yaml format that @Yakov Pechersky has proposed for #port-status, and update all CI tools to use it.

[Scott Morrison]

10. One of: work out lake upload to distribute build artifacts / copy over the mathlib3 build artifact solution / investigate how to do something more fine-grained.

[Eric Wieser]

Mind editing those messages to number them?

[Scott Morrison]

Perhaps people could add the :working_on_it: or similar emoji if they are "claiming" an item.

[Scott Morrison]

(of course, claiming is non-exclusive and non-obligatory :-)

[Scott Morrison]

The recording of today's meeting will be available later at https://youtu.be/O90i1nPOEjs.

[Eric Wieser]

My plans for 6 and 8 are slightly different to the above, respectively:

6. CI action for mathlib3 that detects changes to any file containing a mathlib4 synchronization message with a relevant status on the port status wiki, and adds a label to the PR.

.

8. CI that watches for mathlib4 PRs marked with the mathlib-port label being merged runs nightly and reads the wiki page, then automatically creates a PR to mathlib3 adding the synchronization label to all the corresponding files.

[Moritz Doll]

Scott Morrison said:

2. write a wiki section about Lean 4 coercions

I can do parts of that, but I don't know too many examples of mathlib3 coercions ↦ mathlib4 coercions.

[Mario Carneiro]

Nat.cast was discussed in the meeting

[Eric Wieser]

(specifically, docs#has_nat_cast and docs#int.of_nat were the Lean3 analogs of two of the cast-like things discussed)

[Scott Morrison]

@Eric Wieser, your plan for 6. and 8. sounds better! Thanks. We will need to update again when the yaml format changes, but that should be easy; let's not wait on that.

[Eric Wieser]

Yeah, I would guess that most of the work is in the CI glue, and mathlibtools ought to abstract away the rest in a way that's easy to adapt to

[Eric Wieser]

7\. involves writing the wiki page which is probably a big more fragile and better to leave until the format change is done

[Yakov Pechersky]

I'm sorry I couldn't join. Was there discussion of a "leanproject port" that's similar to a "leanproject pr"? I imagine it takes in at least a mathport and mathlib4 path, and a mathlib3 file name

[Scott Morrison]

Yeah. As I wrote the bullet point for 7. I decided that "manage this" was a more plausible outcome than "automate this".

[Scott Morrison]

@Yakov Pechersky, no, there wasn't. What would it do?

[Yakov Pechersky]

Load the yaml. Check that the file indicated hasn't yet been ported or claimed, according to the yaml. Git checkout branch on mathlib 4. Copy file from mathport to mathlib4 directory (possibly modifying Mathlib.lean). Git push new branch. Read the mathport repo Readme for the hash. Use the gh cli to make a PR. Add a port label. Update the wiki yaml with the PR number and mathlib3 hash.

[Yakov Pechersky]

It can do some subset of this initially.

[Eric Wieser]

Regarding my comment in the meeting about the danger of conflicts in the port-status; I just tried making parallel edits on adjacent lines and github did the right thing.

[Eric Wieser]

I don't think we want people using leanproject on their local machine to update the wiki

[Eric Wieser]

Because then if the format changes people with an old version will clobber it

[Eric Wieser]

If CI is the only automation that edits it we at least can control versioning

[Eric Wieser]

Although maybe the port status page just needs a format version number then the problem goes away

[Eric Wieser]

The mathlibtools version number would likely work

[Scott Morrison]

Wow, okay, sounds great. :-)

[Yakov Pechersky]

Regarding the out-of-date mathlibtools, we can put directly into the tool that if the file is of a newer version, it refuses to run the rest of the port subcommands

[Eric Wieser]

Yes, exactly!

[Eric Wieser]

I've mostly done 8. in #17600.

[Jireh Loreaux]

Yay, no more accidental duplicates.

[Moritz Doll]

Scott Morrison said:

2. write a wiki section about Lean 4 coercions

https://github.com/leanprover-community/mathlib4/wiki#coercions I did not know what to write about the attribute and there might be things missing.

[Moritz Doll]

I've also mentioned autoImplicit in a new 'Tips and Tricks` section at the very end

[Riccardo Brasca]

Does the script add_port_comments.py really work? I get

Traceback (most recent call last):
  File "/home/ricky/lean/mathlib/scripts/add_port_comments.py", line 1, in <module>
    from mathlibtools.file_status import PortStatus
ImportError: cannot import name 'PortStatus' from 'mathlibtools.file_status' (/home/ricky/.local/lib/python3.9/site-packages/mathlibtools/file_status.py)

[Notification Bot]

10 messages were moved from this topic to #mathlib4 > add_port_comments.py by Eric Wieser.

[Jireh Loreaux]

Here's another feature for the port_status script it would be nice to have: an option to check all files that have already been ported to see if they have any dubious translations (i.e., things that should have been #alignₓed but were only #aligned). I mention it because I have already made this mistake myself in a couple of places :face_palm:, which I'm about to go and fix.

Checking for this could be as simple as checking out the most recent mathlib3port and doing grep 'warning.*dubious' list-of-files-that-have-been-ported. It would regularly return some false positives (e.g., in files that have been recently ported, they would appear as Yesin the port status wiki, but we would be checking against the last nightly run of mathlib3port). However, it would make it perhaps easy to catch errors like this before they start to get really annoying.

[Mario Carneiro]

by the way, I chose the word dubious specifically because it is uncommon (zero hits in mathlib), so grepping for dubious alone should work

[Jireh Loreaux]

@Eric Wieser I guess your CI for adding synchronization labels isn't running because it needs a new release of mathlibtools?

[Eric Wieser]

It should run nightly

[Eric Wieser]

Someone has to approve the PR it creates though

[Jireh Loreaux]

What does it put in the PR subject line?

[Eric Wieser]

#17642

[Eric Wieser]

Possibly something lousy

[Eric Wieser]

You can run it manually at https://github.com/leanprover-community/mathlib/actions/workflows/add_port_comment.yml

[Eric Wieser]

It's possible I didn't configure the cron job correctly

[Jireh Loreaux]

No, I just didn't realize this is how it works. Thanks. Is nightly 0 UTC?

[Eric Wieser]

Feel free to make a PR to adjust the title of the bot PRs

[Jireh Loreaux]

what you wrote is fine, it just wasn't the first thing that came to mind for me (synchronization, freeze)

[Eric Wieser]

On the assumption that you're much more involved in actually porting than I am, what first comes to mind for you is likely much better than whatever I wrote to get on with fighting CI

[Moritz Doll]

is there a meeting happening tomorrow? I vaguely remember Mario saying that he has no time and I don't how much the time might interfere with a weird american ritual.

[Riccardo Brasca]

We are talking about 2022-11-24T22:00:00+01:00 right? (For me this is "today"...)

[Jireh Loreaux]

If there is, I won't be there, and likely neither will many people in the US. That "weird american ritual" often encompasses most of the day, at least in some form.

[Patrick Massot]

For people outside the USA: the weird ritual mentioned by Jireh is thanksgiving. I don't really know what it means but indeed I noticed that American people tend to be rather serious about not working on that day, even for fun.

[Scott Morrison]

I won't be there. I'm in the US at the moment with family, but my dispensation to be on the computer will probably expire shortly. :-)

[Arien Malec]

One time I suggested to some colleagues in Germany that traveling on Easter Monday shouldn't be a problem & I quickly learned about "a weird German ritual".

[Riccardo Brasca]

Are we meeting at 2022-12-01T22:00:00+01:00 ?

[Scott Morrison]

I will probably be there, but don't wait for me, as I may have weather delays!

[Shreyas Srinivas]

Hi a newbie trying to port data.set.basic.
May I ask what the meeting is about and who is invited?

[Riccardo Brasca]

Everyone is more than welcome! Last time we discussed several problems. If you have questions it's a good idea to be there... If the experts will be there :thinking:

[Shreyas Srinivas]

Thanks a lot. I will try to make it there

[Scott Morrison]

https://meet.jit.si/moderated/a58c9883e1b3ef01acd9989d4626b2579d5263d496cacf6e5f3f917699ecb994

[Scott Morrison]

I keep getting kicked out of the meeting, I suspect just because my network connection is poor.

[Scott Morrison]

I think I'm in the same situation as Johan. I haven't had any audio come through, just connecting noises.

[Riccardo Brasca]

I changed browser to solve this

[Johan Commelin]

Would it be an option to try Zoom next time?

[Floris van Doorn]

It didn't work for me in Chrome, but it is working now in Firefox

[Scott Morrison]

No luck in Chrome, Safari, or Firefox.

[Kevin Buzzard]

Firefox working fine for me on Ubuntu

[Jireh Loreaux]

I'm also having issues in Opera. Firefox works for me.

[Eric Wieser]

Chrome and Edge are both a no for me

[Jireh Loreaux]

I have firefox 106.0.5 installed

[Eric Wieser]

I get as far as seeing a black box labelled @Thomas Murrills's screen, then the call restarts

[Jireh Loreaux]

That's what I was seeing in Opera too, which is Chrome-based.

[Kevin Buzzard]

Next week move to Zoom?

[Moritz Doll]

fyi the bikeshedding is put to a vote at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.5BRFC.5D.20refine_struct.20functionality.20via.20new.20.3F.2E.2E.20syntax/near/313385470

[Scott Morrison]

Do we have a plan for the next meeting? I'm presuming it is 2022-12-09T08:00:00+11:00. Could someone please plan to host a zoom meeting, and post a link for us?

[Mario Carneiro]

2022-12-08T16:00:00-05:00 conflicts with an all-hands meeting at MSR, so I proposed 2022-12-08T15:00:00-05:00 in the meeting last time but that's pretty rough on the Australians IIUC. Should we try for 2022-12-08T17:00:00-05:00 this time?

[Scott Morrison]

The earlier time is fine with me. Not sure if there are others in nearby timezones. But the later time is fine too.

[Mario Carneiro]

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

[Scott Morrison]

Let's go with 2022-12-09T07:00:00+11:00!

[Kevin Buzzard]

I have a mild preference for the later time but I'm not suggesting we change it this week now it's been announced.

[Johan Commelin]

FYI: meeting started

[Mario Carneiro]

Sarah's list of tactics: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Tactic.20porting.20assignments/near/313711324

[Kevin Buzzard]

Is there a porting meeting this week? I am happy with any of the suggested times (the old time, the old time +-1 hour) but my family want to know when I'm coming home from work. Will the Zoom link be the same?

[Johan Commelin]

:this:

[Jireh Loreaux]

I'll show up.

[Riccardo Brasca]

I will be there... but when?

[Mario Carneiro]

oops, same as last time = 2022-12-15T15:00:00-05:00

[Johan Commelin]

@Mario Carneiro With the same zoom link?

[Scott Morrison]

Re: @Patrick Massot's question about documentation of the colouring schemes for the port progress graphs:

https://github.com/leanprover-community/mathlib-tools/pull/158

[Patrick Massot]

I merged that PR. But I think the most useful thing would be to edit https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#porting-procedure step 1 to say that looking at graphs is more currently useful than looking at the list and stick the color explanation there.

[Scott Morrison]

I have substantially rewritten that section of the wiki page. If someone can review and let me know about problems, that would be great.

[Patrick Massot]

It looks great. I just added Mario's find command.

[Johan Commelin]

Will there be another meeting tonight?

[Mario Carneiro]

2022-12-22T15:00:00-05:00 , let's take the next week off though so that people can do the holiday thing

[Johan Commelin]

Meeting started

[Jireh Loreaux]

Sorry, I'm already doing the holiday thing, so I'll miss today.

[Jireh Loreaux]

If there's a recording, please post the link and I'll watch it later.

[Thomas Murrills]

whoops, in my case, I forgot it had been moved to 3! 4 is anchored in my brain for some reason. see you all whenever the next meeting is, and happy holidays! :)

[Mario Carneiro]

https://cmu.zoom.us/rec/share/Wk86mn6ia7f5loXNjrRYMIV1YzrUAXvUD_qKQ1X1NIsuo5em7xPFzEBGtVq0i_5w.vqhOaKUiu4zlQ7q8?startTime=1671739144000
Passcode: UH#Z8X?t

[Shreyas Srinivas]

Is there some more info on this feature to write equivalent definitions, (one for the compiler and one for human use)?

[Shreyas Srinivas]

Shreyas Srinivas said:

Is there some more info on this feature to write equivalent definitions, (one for the compiler and one for human use)?

In the docs for instance

[Mario Carneiro]

It's the @[csimp] attribute

[Johan Commelin]

Meeting in ~90 mins: 2023-01-05T21:00:00+01:00

[Henrik Böving]

Mario Carneiro said:

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

Is this still the meeting link?

[Johan Commelin]

    2014 src/data/real/ennreal.lean
    2061 src/ring_theory/power_series/basic.lean
    2079 src/data/matrix/basic.lean
    2101 src/topology/algebra/module/basic.lean
    2106 src/algebraic_geometry/open_immersion.lean
    2122 src/measure_theory/constructions/borel_space.lean
    2142 docs/references.bib
    2196 src/linear_algebra/basic.lean
    2209 src/analysis/calculus/deriv.lean
    2229 src/analysis/special_functions/pow.lean
    2248 src/category_theory/limits/shapes/pullbacks.lean
    2273 src/measure_theory/function/conditional_expectation/basic.lean
    2355 src/ring_theory/ideal/operations.lean
    2371 src/data/multiset/basic.lean
    2378 src/set_theory/ordinal/arithmetic.lean
    2429 src/analysis/inner_product_space/basic.lean
    2449 src/computability/turing_machine.lean
    2489 src/tactic/core.lean
    2511 src/data/finset/basic.lean
    2611 src/order/filter/basic.lean
    2676 src/data/buffer/parser/basic.lean
    2711 src/measure_theory/integral/interval_integral.lean
    2713 src/topology/order/basic.lean
    2956 src/measure_theory/function/lp_space.lean
    3032 src/measure_theory/integral/lebesgue.lean
    3086 src/topology/metric_space/basic.lean
    3132 src/analysis/calculus/fderiv.lean
    3222 src/group_theory/subgroup/basic.lean
    3494 src/analysis/calculus/cont_diff.lean
    4126 src/measure_theory/measure/measure_space.lean
    4204 src/data/list/basic.lean

[David Renshaw]

4204 src/data/list/basic.lean

all downhill from here

[Scott Morrison]

Is there another meeting about to happen now?

[Johan Commelin]

sounds good to me

[Mario Carneiro]

Sorry for missing the meeting, someone really wanted to finish Data.Multiset.Basic and I ended up in the wrong timezone again ;) . Here's the recording link:

https://cmu.zoom.us/rec/share/ILUT_80UqBLzTrsG0iPVJs4xC7Hmqg1N3ULZy8yzCMG8LD21XhzB2mnJPcVejxui.4XHAUmzBM4-f0m0g?startTime=1673553487000
Passcode: N9Vp+7n8

[Johan Commelin]

/me :see_no_evil: :clock: :in_bed: :cross_mark: :working_on_it: :working_on_it: :working_on_it: :tada: :zzz:

[Evgenia Karunus]

@Mario Carneiro, I think some people wanted you to take a look at their code last time; do you think we could have another 1-hour meeting series, e.g. right before the current porting meeting, where we can ask you questions about porting/would you prefer one-on-one calls/something else?

[Mario Carneiro]

one-on-one sounds best

[Johan Commelin]

I will not be able to make it today.

[Heather Macbeth]

I'll be there but late.

[Chris Hughes]

Is the meeting now?

[Mario Carneiro]

https://cmu.zoom.us/rec/share/mGfpugCNTgzS9qGSAzvYIWZ-ALPSe2z8js45iSSk2bUCq3uzk5KYb6tkc8SK5uf1.xrB-E6ejVRnb29qD?startTime=1674158378000
Passcode: tsp*rgj9

[Jireh Loreaux]

Please confirm: we're meeting in a little less than an hour, right?

[Thomas Murrills]

(Sorry, I will not be there today, as I’m on a trip this week!)

[Mario Carneiro]

https://cmu.zoom.us/rec/share/xUEFxJaCb2fvCqQvpJsdr_JgzL-zrl_kR-qJDPTNZrP-qB_58eXXlBQY6cMbWptF.86ViC07Hvco6xKeK?startTime=1674763150000
Passcode: .2vtyS3$

[Yury G. Kudryashov]

I joined the porting effort but I can't attend the meetings because I have teaching 2023-01-26T14:20:00-06:00-2023-01-26T15:35:00-06:00 .

[Yury G. Kudryashov]

(every Tuesday and Thursday)

[Mario Carneiro]

Since the semester might have disrupted others' schedules as well, let's take a poll to see if there is a different day that works for more people:

[Mario Carneiro]

/poll What day should the porting meeting be on?
Monday
Tuesday
Wednesday
Thursday
Friday

[Yury G. Kudryashov]

What time of day are we talking about? Should I create a more detailed poll on doodle.com?

[Mario Carneiro]

same time, 2023-01-26T15:00:00-05:00

[Mario Carneiro]

given the international crowd the time of day isn't too flexible

[Yury G. Kudryashov]

(deleted)

[Yury G. Kudryashov]

(deleted)

[Johan Commelin]

Mario Carneiro said:

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

[Mario Carneiro]

https://cmu.zoom.us/rec/share/KcYImFOqA1gdSc_qXEPukmkkOMu-e9zndraCKP4EsT6iD1JpqJbt5omWNq2Cx3fI.zeWYueNRrHFXlwHC?startTime=1675368059000
Passcode: AYq+5HXK

[Mario Carneiro]

Based on the poll results, we'll be meeting on Mondays starting next week 2023-02-06T15:00:00-05:00

[Thomas Murrills]

(Unfortunately I have an appointment at 2:30, so I might miss the meeting or only arrive in the latter half)

[Johan Commelin]

meeting started

[Eric Wieser]

@Mario Carneiro, are you planning to join us?

[Mario Carneiro]

Sorry for missing the meeting this week. Here's the recording:

https://cmu.zoom.us/rec/share/bdOGzXdCfjuMh8aENg26nAnk1zURO1Get1HlJ1tqz-N_up2DQ0OVfZS4hpTXbZel.MYXF7WxdfXJtYiqc?startTime=1675713659000
Passcode: &a20kcXe

[Notification Bot]

26 messages were moved from this topic to #mathlib4 > Already-forward-ported files by Eric Wieser.

[Mario Carneiro]

Since many lean people are at the IPAM workshop this week, I propose we cancel today's meeting.

[Eric Wieser]

Are we meeting at 2023-02-20T15:00:00-05:00 today? Or are people travelling from IPAM?

[Kevin Buzzard]

Let's assume everyone travelled over the weekend :-)

[Johan Commelin]

I don't have any input for the meeting.

[Johan Commelin]

Do others have questions that they want to discuss?

[David Renshaw]

what are the current blockers?

[Johan Commelin]

Do you mean lean 4 issues? Or porting PRs? In general, I guess the lack of eta-for-classes is causing trouble.

[Eric Wieser]

We've discovered that in Mario's absence we can't share screens!

[Jireh Loreaux]

oh I thought we weren't meeting?

[David Renshaw]

we're kinda having a co-working session :)

[Kevin Buzzard]

I got bicategory.functor compiiling thanks to Matt :D

[Mario Carneiro]

Sorry about the sharing screens issue. I will try to send out some co-host invites to other maintainers, since there doesn't seem to be a way to enable screen sharing which is sticky over meetings

https://cmu.zoom.us/rec/share/718JCNE9F5zDIbjpPdM_fNa3AaXrUFXbgO71-KYAdqSIJ9-0si2IMe9q80z_PhJq.D2sw7VEdMylmf_xb?startTime=1676923177000
Passcode: &.L785pf

[David Renshaw]

Johan Commelin said:

Mario Carneiro said:

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

meeting now

[Mario Carneiro]

https://cmu.zoom.us/rec/share/zB5iaIqLJmiNCYZ6PR4ddXCPOyB5HV_1sy0OBsCq2rhKIHFdC_VIuA-IvGdWVtBE.g9ncB9TbiXcgorh9?startTime=1677528003000
Passcode: U&5&49zS

[Mario Carneiro]

https://cmu.zoom.us/rec/share/GD7lq_GNxalARWCm8ZsL9LfUJEPCgC-_VYYK_hlydbLFxxKTkPVvZ-uanvasRE4M.3pkJFhcrQUNApgBS?startTime=1678132827000
Passcode: V9SK=m7#

[Eric Wieser]

2023-03-13T20:00:00?

[Matthew Ballard]

Dang daylight savings time

[Jeremy Tan]

can't attend, that's when I'm asleep

[Eric Wieser]

Matthew Ballard said:

Dang daylight savings time

In my timezone that's the same time as always (in the UK it switches Mar 26th). If that's not the case in other people's, then perhaps we should pick a new time

[Matthew Ballard]

We will align again shortly. I say stick with it until then

[Eric Wieser]

I say let @Mario Carneiro decide

[Reid Barton]

Yes, DST in the US started yesterday.

[Jeremy Tan]

My country, Singapore, has no DST

[Matthew Ballard]

I am flexible so have no strong preference. I have to juggle a meeting with student so knowing sooner would help

[Eric Wieser]

What would the alternate time be?

[Matthew Ballard]

2023-03-13T15:00:00-04:00 is 3 EDT now

[Gabriel Ebner]

I thought we're doing meetings at 2023-03-13T15:30:00-07:00 since last week? (i.e., later than before?)

[Eric Wieser]

I don't see a message about that above

[Gabriel Ebner]

Ah, Kevin told me the time got changed and I assumed Mario's post from last week ^^ is the new time.

[Mario Carneiro]

I was assuming it starts now: 2023-03-13T15:00:00-04:00

[Thomas Murrills]

Oh, I thought an hour from now based on the thread. I can be there shortly if we’re meeting now, though…are we?

[Mario Carneiro]

we are

[Eric Wieser]

I'll probably miss the whole thing in that case

[Mario Carneiro]

https://cmu.zoom.us/rec/share/efKAc4UpLWfy1JH6EWxJRefPuuItzM56d2M9ylMbgANuGbbTGAD_kY7rREgixEe1.5GhcB789C_uyxCoQ?startTime=1678734128000
Passcode: 2!FJ7GSt

Next week we'll be meeting at the same time 2023-03-20T15:00:00-04:00 , but let's do another poll to see whether another time of day will be better going forward:

[Mario Carneiro]

/poll When should we meet after daylight savings (on mondays)
10 AM PDT = 1 PM EDT = 7 PM CEST
11 AM PDT = 2 PM EDT = 8 PM CEST
12 PM PDT = 3 PM EDT = 9 PM CEST
1 PM PDT = 4 PM EDT = 10 PM CEST
2 PM PDT = 5 PM EDT = 11 PM CEST

[Gabriel Ebner]

I won't be able to come tomorrow since we have a company event.

[Scott Morrison]

@Mario Carneiro, is there meant to be a meeting now?

[Mario Carneiro]

yes

[Eric Wieser]

Mario Carneiro said:

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

[alex chan]

Is this private meeting, can I join ??

[Scott Morrison]

@alex chan, Eric just posted the link in the other thread.

[Mario Carneiro]

https://cmu.zoom.us/rec/share/9n5VBm-Bfr_4sn_ZBTaP2v7OXt1KKwplE1eiUaXg_z3CxiH4WaNLEBPl5JIeitOB.yzj5ufzzCdejLWFg?startTime=1679338782000
Passcode: Wx5t6G=0

[Notification Bot]

2 messages were moved here from #mathlib4 > port progress by Anne Baanen.

[Scott Morrison]

Did we decide a time?

[Kevin Buzzard]

...asks the person who would prefer it not be 5am their time and who is probably going to bed soon. I am happy with any time between approx 6 and 10 hours from now.

[Eric Wieser]

The poll above suggests 2023-03-27T12:00:00-07:00 as the winning vote

[Jeremy Tan]

(which is 3am my time)

[Scott Morrison]

The meeting link is
Mario Carneiro said:

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

as usual.

[Mario Carneiro]

https://cmu.zoom.us/rec/share/TomcR5TzQHQRYbCWBS9epem2yAvZUsnPfEFrK3NyXbOgo_qVY6fpjqitjY0oba_D.as5EaqTA1IR2xf63?startTime=1679943633000
Passcode: sJ$+^6Lc

[Scott Morrison]

Next meeting at 2023-04-04T05:00:00+10:00! :in_bed: :zzz: :alarm_clock:

[Kevin Buzzard]

(I'll be missing the next two, I'm in India and this is past my bedtime)

[Mario Carneiro]

https://cmu.zoom.us/rec/share/MGhoRl6AY4o7KCRBQefTIm7QgevKLp2nBX8OTx5KTvjEfklZe9kFqE7fXm-CdqHn.fyE7LMZNxR6HRU8a?startTime=1680548385000
Passcode: +B7!gM0#

[Mario Carneiro]

https://cmu.zoom.us/rec/share/aWBe3t38z38VP9v3C5wypNI8Uo-uxYO9UObyLqr9DlsWOvKBTQ9I6FtuTwT72Qf6.yvzco00Augkhs7fc?startTime=1681153165000
Passcode: n8qUk@g6

[Thomas Murrills]

(I’ll be missing at least part of this meeting; if I can, I’ll join later on :) )

[Mario Carneiro]

https://cmu.zoom.us/rec/share/6pSeTBcuv_5hRLjkQnvjoXUo0gKijGDptHlFFtcgfdQYOlxuv-12Hvnzf8zmgrSt.xp9MH03hoPoHB5jm?startTime=1681757930000
Passcode: ^12u+PE3

[Mario Carneiro]

@Eric Wieser You mention in the meeting that you wanted to get information about parser combinators like ,* and ppGroup. Hover and go-to-definition actually works in both cases, but you have to use import Lean or else it won't work because the constants it wants to link to are not in the environment.

import Lean

           -- v click here to go to Lean.Parser.ppGroup
syntax "foo" ppGroup("bla"),* : term
                        -- ^ hover talks about sepBy, although ctrl-click doesn't work

[Mario Carneiro]

compare:

           -- v hover talks about sepBy, no ctrl-click
syntax "foo" ppGroup("bla"),* : term
                        -- ^ hover talks about sepBy, no ctrl-click

[Scott Morrison]

I heard there was discussion at the last meeting of pushing the meeting time later by an hour. If anyone is able to confirm or deny, that would be great, so I can set my alarm clock. :-)

[Eric Wieser]

I can confirm in the last meeting that no one present (@Gabriel Ebner, @Kevin Buzzard, @Matthew Ballard, me, maybe some others who don't appear in the zoom transcript) objected to pushing back by an hour

[Eric Wieser]

But it sounds like we forgot to do a poll / make an announcement and now we're left in the same position as always that people aren't simultaneously awake to agree a new time at short notice

[Scott Morrison]

Okay, I will wake up really early again, and take responsibility for running the poll after the meeting. :-)

[Eric Wieser]

Happening now

[Scott Morrison]

Trying again to move the meeting one hour later:

[Scott Morrison]

/poll Future mathlib4 porting meetings
1pm PDT, 4pm EDT, 10pm CEST, 6am AEST
noon PDT, 3pm EDT, 9pm CEST, 5am AEST

[Mario Carneiro]

https://cmu.zoom.us/rec/share/CFkkDwoogHQpxDV5wrwa6jV7Q8Oq7hRykmEF1Lfd_Z4_f5nQwOOqsgCmvI1JziGO.aw5dEYGG29VCJSDv?startTime=1682362741000
Passcode: 6PN@0=RH

[Scott Morrison]

Okay, this poll came out the way I wanted, so: the next mathlib porting meeting will be at 2023-05-02T06:00:00+10:00!

[Mario Carneiro]

https://cmu.zoom.us/rec/share/MUBVFm33iGZnRiCvvtp1a8nx3deZPTY7J5oYRnhM1dvERce2o4ZSvdw8XLN8rK4-.aXMjXfev9yQ4v9rq?startTime=1682971245000
Passcode: s9Yy?GVE

[Thomas Murrills]

Here's the rfl tactic PR that we discussed in the meeting: !4#3758 (currently awaiting CI)

[Scott Morrison]

Link broken?

[Thomas Murrills]

Oops, transposed the last two digits. :) fixed now!

[Scott Morrison]

There's a suggestion from Mario, otherwise looks good to me. How about run !bench once CI is done?

[Thomas Murrills]

Continued in #mathlib4 > !4#3758 – rfl refactor & fix ! :)

[Scott Morrison]

A reminder the next meeting is coming up at 2023-05-09T06:00:00+10:00!

[Mario Carneiro]

https://cmu.zoom.us/rec/share/zR-VKKIym_l_RI9fswq-qTpsdYk999QE2VGkRLoFQFqiOID8U6OT2FyPtUUZjK7w.fjj60cjItaYh7DjS?startTime=1683575955000
Passcode: ?x0&W8#y

[Kevin Buzzard]

I assume we're meeting in 1 minute from now.

[Mario Carneiro]

https://cmu.zoom.us/rec/share/gbsh6P9sRVfLbfxR046UxVOMIC0f9_XcCCyNZiUlD7chxUO1cK3AGYaXsU2ojekB.QjsI3rrnXP9f_Vyq?startTime=1684180746000
Passcode: auVV2su*

[Mario Carneiro]

@Kevin Buzzard You asked about searching for #aligns in the meeting to translate something where you know the lean 3 name. While you can grep for it, you can also use the #lookup3 command

[Kevin Buzzard]

Are we meeting today in about seven hours?

[Kevin Buzzard]

Me Scott Johan Matt Heather Adam... are all physically in Banff

[Matthew Ballard]

There is a nice talk at 2023-05-22T14:00:00-06:00 also

[Jireh Loreaux]

I'm at a conference and won't be available today.

[Eric Wieser]

Kevin Buzzard said:

Me Scott Johan Matt Heather Adam... are all physically in Banff

Is that an argument for or against meeting?

[Mario Carneiro]

looks like most people aren't available, so let's cancel this week

[Eric Wieser]

I think @Kevin Buzzard also did the time calculation wrong above, it was 8 hours (now) not 7 (an hour ago).

[Kevin Buzzard]

Are we meeting in 3 minutes? Hopefully I didn't do the calculation wrong this time (last time I forgot we'd recently added 1 hour to the start time)

[Eric Wieser]

Can we make a linkifier for the zoom link and put it in the thread title so we don't have to scroll up each week?

[Yury G. Kudryashov]

It seems that I missed the meeting again. I shoulld set up an alarm.

[Mario Carneiro]

Eric Wieser said:

Can we make a linkifier for the zoom link and put it in the thread title so we don't have to scroll up each week?

I usually put the link in a calendar notification for this kind of thing

[Mario Carneiro]

https://cmu.zoom.us/rec/share/D0ojneXcxYzY1F0qw5ih6LXlOxkTA-vaONNo6XB5mfgfvXfYPZoG_BOJRl5H3D9e.HwrohSnLPMAziGzt?startTime=1685390450000
Passcode: %0*i?w+K

[Kevin Buzzard]

Bonus for working out what the passcode does when interpreted as a regex

[Scott Morrison]

Next mathlib porting meeting at 2023-06-06T06:00:00+10:00!

[Scott Morrison]

A quiet meeting today. Discussed and needing follow up:

• the mysterious failure to add a theorem to the environment in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Lean.204.20doesn't.20add.20lemma.20to.20the.20environment, which @Alex J. Best says he'll try to minimize
• unfortunately needing to add many simp lemmas for ModelProd, which is a type synonym for Prod introduced to avoid instances, in !4#4656. It feels like we need a reducibility setting that simp can see through by typeclass synthesis can't.
• the question of allowing variable! from !4#3162 in committed code.

[Alex J. Best]

I think this is as minimal as I can find

variable {ι E : Type} (I : ι)

local notation "ℝ" => ι

def ha (_I : ι) (_f : ℝ → E) : Prop := True

variable {f : ℝ → E}

theorem tndsto (h : ha I f) : True := trivial
#check tndsto

[Scott Morrison]

That's pretty minimal. :-) Want to create a Lean4 issue?

[Alex J. Best]

https://github.com/leanprover/lean4/issues/2257

[Mario Carneiro]

https://cmu.zoom.us/rec/share/Spp7PuOj9pi3j7oXITZvKc6AGkOAVaJVw-MTVZco9UhGci-_W2XWr-1zOmwcekuh.QUmS52_T2UGcptwz?startTime=1685995251000
Passcode: 9D%!jQa1

[Mario Carneiro]

By the way, lean4#2257 looks pretty similar to lean4#2226

[Scott Morrison]

no_index reminds me of something that is maybe worth asking about again.

A common (anti)pattern in category theory is that we have @CategoryStruct.comp D 𝒟 X Y Z f g, and would like to rewrite by a lemma that says @CategoryStruct.comp D 𝒟 X' Y' Z' f g = h, where here the fs and gs appearing are syntactically identical, but the objects these are morphisms between have changed from X Y Z to some definitionally equal objects X' Y' Z'.

Because of the difference in the implicit arguments X Y Z, rw won't fire, and we resort to erw. However this is overkill: the explicit arguments match identically, so we "know" the implicit arguments must match definitionally.

rw is "just" a wrapper around kabstract which is in turn a wrapper around isDefEq, so I think asking for any more powerful behaviour in rw here comes down to asking about isDefEq. Does it even make sense to ask if we can test def-eq-ness in situations like this by comparing the explicit arguments before the implicit ones?

[Scott Morrison]

If we could make some improvement on this it would massively improve life in e.g. algebraic geometry, where this issue arises all the time.

[Scott Morrison]

e.g. !4#4693

[Eric Wieser]

What are X and X' in this example?

[Scott Morrison]

The meeting link is
Mario Carneiro said:

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

as usual.

The next meeting is 2023-06-13T06:00:00+10:00. Likely I won't make it, as I'm going to try to catch some of the PNAS meeting, which is at a ridiculous time for me.

[Kevin Buzzard]

The PNAS meeting finishes just in time for the porting meeting, right?

I'm at two conferences this week :-/ and the meeting clashes with the conference dinner for one of them so I'll probably not make it either.

[Mario Carneiro]

https://cmu.zoom.us/rec/share/fatk9LUh-kgaIMAvmlfhDCNRXebBA7eIVCBNRoteutIFBXHwMhWeOVzHiqG4cO89.MJzhslLq7FWJwuta?startTime=1686600013000
Passcode: 3Dp#JE!+

[Scott Morrison]

Next meeting at 2023-06-20T06:00:00+10:00!

[Damiano Testa]

What is the meeting link?

[Riccardo Brasca]

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09

[Mario Carneiro]

https://cmu.zoom.us/rec/share/04HkxlGzBDMV9ZqbgFVrB5-PFJfcYyRAAerdt7vPUccEapaeB0Znj-OwPr5hvx9k.XrrRIAz2TsayhGTn?startTime=1687204762000
Passcode: v*M2n.i9

[Notification Bot]

42 messages were moved from this topic to #mathlib4 > #stalled PRs by Scott Morrison.

[Scott Morrison]

The meeting link is

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

as usual, at 2023-06-27T06:00:00+10:00.

[Mario Carneiro]

https://cmu.zoom.us/rec/share/B9YS_HX_Ex11HAisB3lDaOibzgqfrDIEP0C5aqV3SDA3HLwo-Co5007qdLOvdPG7.5YYflG9gs7lEfxUk?startTime=1687809696000
Passcode: ^b0k=3qh

[Scott Morrison]

Today's porting meeting was all triage: we went through the #port-dashboard, deciding what to do with the "old stuff", and then started going through the tactic porting tracking issue #430 to see what still needed to be done.

I'm going to now post a whole list of individual TODO items. If you are able to do one of these, please either claim it with a :working_on_it:, or just tell us that you've done it with a :check:.

[Scott Morrison]

• category_theory.limits.constructions.over.default is a "fake" default file that actually has content. It should be renamed in mathlib3. (And we'll subsequently port it like anything else.)

[Scott Morrison]

• many .default files in #port-comments have been deleted from mathlib3, and we should delete them from #port-comments

[Scott Morrison]

• control.random, testing.slim_check.gen, testing.slim_check.sampleable, and testing.slim_check.testable have all been ported by hand (and everything that is needed for slim_check works), so we should just add a header to the mathlib4 file so the dashboard know this is completed.

[Scott Morrison]

• data.buffer.parser contains code parsing strings into arrays, and contains some proofs about its behaviour, not just meta code. We would eventually like to have this, but it needn't be ported now. The proposal is to create a mathlib4 issue saying at least "We would like a replacement implementation of mathlib3's data.buffer.parser", and to port it as an empty file, containing just the header and a link to the issue.

[Scott Morrison]

• data.rat.meta_defs we think has been entirely ported, but the code is spread amongst different locations (and this is fine). Proposal: port as an empty file, containing just a header, and either a TODO to track them down, or references to the places the replacement code now lives.

[Scott Morrison]

• for all the files on #port-dashboard with array in the name, port them so that they are written in terms of the new Array. Still #align declarations, even though they are now talking about a different type! (See zulip discussion.)

[Scott Morrison]

• init.data.list.instances should be ported as a file with just a header and #align statements

[Scott Morrison]

• all the RBTree files can be ported as empty files, just with a header, as all the content we want is in Std already.

[Scott Morrison]

• we would like to use whatever mechanism in https://github.com/leanprover-community/mathlib-port-status/ already exists to not list meta code from Lean 3 core to also not list system.* and init.meta.*

[Scott Morrison]

• update the tactic porting tracking issue #430 to reflect discussion in the meeting

[Scott Morrison]

• write a description of the current meta PRs on the #queue, and solicit additional reviews as needed

[Scott Morrison]

• write a summary of important / interesting tactics that still need porting

[Scott Morrison]

There was mention of an idea for implementing parameter in terms of nullary typeclasses. I can't find any trace of this on zulip: if someone knows a source we can mention this in #430.

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/parameter/near/271747258

[Scott Morrison]

Wow, that is really simple.

[Jeremy Tan]

Scott Morrison said:

• all the RBTree files can be ported as empty files, just with a header, as all the content we want is in Std already.

!4#5504

[Scott Morrison]

@Jeremy Tan, would you mind merging Johan's #5479 into this. I don't think we need to have all the #align's in the later files, but given Johan has already done that effort we shouldn't waste it.

[Scott Morrison]

#5505 adds the headers for the slim_check files.

[Jeremy Tan]

Scott Morrison said:

would you mind merging Johan's #5479 into this

Should be done

[Scott Morrison]

!3#19217 renames category_theory.limits.constructions.over.default and is ready for a :peace_sign: or .

[Mario Carneiro]

On the topic of files from core that were not ported, I just noticed that Mathlib.Init.Data.Nat.Lemmas is an adhoc port, and is missing the majority of #aligns, which is surprising since there are so many important theorems on Nat in there

[Mario Carneiro]

actually, now that I think of it it's probably using the older convention of using #align only when mathport would not be able to guess the name on its own

[Johan Commelin]

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09

Starting in two minutes, I suppose.

[Mario Carneiro]

https://cmu.zoom.us/rec/share/Hb53g_FV5i-9I0Dsn79NqZuvUft2gojG-rrA2T8EXvwQjqVUZ1jed-YTGH0XtTwx.1pghhJtIPgkmdiA9?startTime=1688414370000
Passcode: $F#Y62gu

[Eric Wieser]

Starting 8 minutes ago? Or did last meeting conclude we weren't meeting this week?

[Eric Wieser]

Ah, I guess this programme suggests there might be a clash with an overrunning wine and cheese party!

[Heather Macbeth]

End-of-port party at 2023-07-18T06:00:00+10:00?

[Jireh Loreaux]

BYOB :beer:. For some of you this is a very strange time for a drink. :smiley:

[Johan Commelin]

@porters We'll start in 5 minutes (-;

[Shreyas Srinivas]

Are people who haven't ported recently welcome?

[Scott Morrison]

The meeting link is

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

as "usual".

[Scott Morrison]

Shreyas Srinivas said:

Are people who haven't ported recently welcome?

Yes, please, it's a party, all welcome. :-)

[Ruben Van de Velde]

Clearing out some old tabs, remember when graphs looked like this? https://tqft.net/mathlib4/2023-01-17/number_theory.legendre_symbol.quadratic_reciprocity.pdf

[Shreyas Srinivas]

In line with the discussion, some suggestions for future lines of work from the CS side that do not involve algorithms or verification:

1. Finite Model Theory: The textbook by Leonid libkin might be a good start.
2. Fair division/allocation theory: Many (already proved) theorems about existence of various kinds of allocations and their computation through graph theoretic methods.
3. Computational Social Choice.
4. The book on boolean Fourier analysis by Ryan O Donnell.
5. The matrix cookbook which iirc someone is already working on.
6. Elementary probability theory with accompanying tactics. (For example a tactic that searches the environment for conditions and matches them with the correct concentration inequality out of some tagged ones)
7. If some of the above are done, then the theory of Markov Decision Processes.

[Mario Carneiro]

https://cmu.zoom.us/rec/share/jwUJ-4hubpzzajsByKEGP1jOCXdngVOyRq_Fq5D8YfqeGqXfJhb0rmxgqBppy1TK.pHZS4Ydm2sCCjbIb?startTime=1689623924000
Passcode: ?9^wP6UG

[Scott Morrison]

As follow-up from today's meeting (I forget if it was in the main meeting or after-party):

• feat: says tactic combinator #5980

This is a primitive implementation of the says combinator discussed at today's porting meeting.

If you write X says, where X is a tactic that produces a "Try this: Y" message, then you will get a message "Try this: X says Y". Once you've clicked to replace X says with X says Y, afterwards X says Y will only run Y.

[Scott Morrison]

(When thinking about this earlier, for some reason I had expected that we couldn't write says in between the X and Y, and that it would have had to come first, and thus be quoth instead of says.)

[Mario Carneiro]

(I forget if it was in the main meeting or after-party)

By the way, I want to state that I wasn't really happy with the "after-party" setup; as I expected we just ended up doing more business during the second half of the meeting and that wasn't recorded despite containing lots of useful information for people who might not be in the right time zone. I'd rather not repeat it.

[Sebastian Ullrich]

As mentioned on Monday: counting the remaining porting notes in the speedcenter #5994

[Mario Carneiro]

We're still doing this! At least until we all get bored of it...

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

[Jireh Loreaux]

I have to miss today, sorry.

[Mario Carneiro]

https://cmu.zoom.us/rec/share/sAHBY7S9IQJUS3u3yK1OkfnDsMEAhgn8agdZeltcwgp3zRg1oqVY7nX5gm1EZRPO.VuIl0cA5bwGoz0tU?startTime=1690228917000
Passcode: ^t1NB@QS

[Scott Morrison]

A reminder we're still having Mathlib meetings at the regular time.

2023-08-01T06:00:00+10:00

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

[Mario Carneiro]

https://cmu.zoom.us/rec/share/ozrnh1y__FHz-on9rRTpCYKb6cRf1KhrkSZGeO2IWEAI2wo3W8Z30oc88gSacIzl.bfvxuo_QWvp_5TZR?startTime=1690833651000
Passcode: mq!J1?$g

[Scott Morrison]

I will not make today/tomorrow's meeting at 2023-08-08T06:00:00+10:00 as it's rather soon and I need to sleep. I encourage everyone to think about organising a PR merge sprint. :-)

[Mario Carneiro]

Tune in for the next edition of "what's next for mathlib" at: 2023-08-01T06:00:00+10:00

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

[Eric Wieser]

#queue for reference

[Mario Carneiro]

https://cmu.zoom.us/rec/share/rb1jRfD7YkIE334mxV4YBFwlo-VSLLMNm3TUKJX_OW1wU19Xcrdy7RIjb8N497xX.YMppbvK4yxKqXgzV?startTime=1691438417000
Passcode: !#c2Hejm

[Scott Morrison]

Regarding the Type _ issue discussed in this meeting. Talking to Leo yesterday, he said something that I hadn't appreciated: paraphrasing only slightly: "I wouldn't allow authors to use Type _ in a repository I was responsible for. It will cause delayed unification problems, with potentially unpredictable results or performance problems."

I would suggest that not only do we merge Matthew's PR about this, but that we add a linter forbidding Type _ in Mathlib.

We should perhaps think of it as

• there as a historical legacy, from when it was painful to have to introduce your universes ahead of time (note that's not longer the case: you can just write variable (X : Type u) (Y : Type v).
• an aspect of Lean's great flexibility to write metavariables almost anywhere and then hope for unification to help you, rather than a feature there to support universe polymorphism.

[Mario Carneiro]

there as a historical legacy, from when it was painful to have to introduce your universes ahead of time (note that's not longer the case: you can just write variable (X : Type u) (Y : Type v).

This is not really an improvement over the legacy syntax

[Mario Carneiro]

in particular you can't write variable (X Y Z W : Type _) here

[Eric Wieser]

I would suggest that not only do we merge Matthew's PR about this, but that we add a linter forbidding Type _ in Mathlib.

I think I suggested this in the meeting

[Eric Wieser]

Matthew pointed out that a notable exception is things like def foo : Type _ := ... where you really do just want lean to unify the universe

[Mario Carneiro]

I recall Eric also suggested tweaking variable elaboration to make variable (X Y Z W : Type _) make new universe variables rather than metavariables, like in lean 3

[Eric Wieser]

That's what Matthew's PR does anyway though, using * syntax instead of _

[Scott Morrison]

Even the def foo : Type _ := ... seems pretty dubious to me --- saving characters at the expense of readability.

[Mario Carneiro]

readability of what though? 99% of the time the universe levels just aren't important and obscure the mathematical content

[Eric Wieser]

If you banned Type _ then people would write def foo := which is worse because now you have to guess whether the expression is a type at all

[Eric Wieser]

(ok, we should probably ban that in a linter too)

[Mario Carneiro]

I remain pro-hiding-universes because lean is remarkably good at making the whole level algebra thing invisible in the vast majority of cases, although category theory may be an exception to this (because of its free level variable)

[Mario Carneiro]

Lean core has made some questionable choices regarding universe unification though, like allowing the body to unify level metavariables in the theorem statement. I suspect this is at least partially the cause of the "unpredictable results or performance problems" Leo is hinting at

[Matthew Ballard]

Eric Wieser said:

That's what Matthew's PR does anyway though, using * syntax instead of _

Yes though Kyle wrote the elaborators.

On my most recent pass today, I tried to make universe levels explicit but left two cases: type wrappers and quantification over types.

[Matthew Ballard]

I only encountered one incident of seemingly unintentional monomorphization

[Eric Wieser]

Scott Morrison said:

Regarding the Type _ issue discussed in this meeting. Talking to Leo yesterday, he said something that I hadn't appreciated: paraphrasing only slightly: "I wouldn't allow authors to use Type _ in a repository I was responsible for. It will cause delayed unification problems, with potentially unpredictable results or performance problems."

If you're not allowed to use Type _, then you're also not allowed to use autoImplicit for type variables, right?

[Scott Morrison]

Why?

[Eric Wieser]

Because doesn't that generate a variable of type Sort _?

[Scott Morrison]

Indeed. No explicitly written Type _, then. :-)

[Eric Wieser]

Well "It will cause delayed unification problems, with potentially unpredictable results or performance problems" is true of implicitly-written Type _ too!

[Mario Carneiro]

IIRC Leo also didn't like {X} in declarations, although this was before auto implicits

[Scott Morrison]

Yes, but we would have fewer of them by banning the explicit ones.

[Mario Carneiro]

How about we add an option to make universe metavariables get turned into variables after the type is elaborated? I think this will have minimal fallout on mathlib since lean 3 effectively did this

[Mario Carneiro]

I think that will address the main performance issue with universe metavariables - having no ground terms at all because the base types have universe metavariables in them

[Jireh Loreaux]

I think we should see how performance of that compares to Matthew's PR.

[Scott Morrison]

(deleted)

[Matthew Ballard]

I transitioned from Sort _ to Sort* last night taking care to make explicit any existing constraints on the universe level.

One thing that was very common was having Sort _ when Lean would only accept Type _

[Eric Wieser]

We had a few of those in lean 3 too when we had the binders in the declaration rather than variables

[Matthew Ballard]

Mario Carneiro said:

We're still doing this! At least until we all get bored of it...

https://cmu.zoom.us/j/91251085952?pwd=cnFCK0RTWVJnUS96MTRCMXVSL0haZz09
Meeting ID: 912 5108 5952
Passcode: 730524

Are we bored of this?

[Eric Wieser]

At least bored of turning up the first 10 minutes it seems....

[Matthew Ballard]

Or the first 25 minutes :)

[Kevin Buzzard]

Sorry, I'm in a field with a bunch of other people

[Jireh Loreaux]

I've been at a state fair all day with my kids. I should be more regular once the semester starts.

[Mario Carneiro]

I've been a little under the weather this weekend and appear to have missed it, sounds like the recording will be interesting

[Mario Carneiro]

It appears the recording captured 25 minutes of no talking and Matthew staring at the screen, so I think I will not post it. Here's the chat log:

• Eric Wieser 12:40

  I'm afraid I haven't really been following your work on the with stuff recently, and probably shouldn't distract myself this week by getting re-interested in it!

  (afk for 5 minutes)

• Matthew Ballard (he/him) 14:48

  I got a with to elaborate as let src := a; toA := src and benchmarked it. Lots of changes. Most good but some serious regression mostly around Algebraic Geometry and Calculus.

  Today I got let src :=a; {toA := a} but I tripped the unused variable linter so cannot build and share a toolchain

• Eric Wieser 16:02

  Aren't those the same?

• Matthew Ballard (he/him) 16:16

  The second reduces the let

• Eric Wieser 16:34

  I don't understand the first, it looks like a syntax error

• Matthew Ballard (he/him) 16:48

  Yes it should be {toA := src}

  Currently it elaborates are let src := a; {toA := { x := src.x }}

  For some reason there is an extra eta expansion on top of everything.

  It doesn’t seem to have anything to do with the reenable eta stuff

• Eric Wieser 18:49

  Sorry, I see the difference now

• Matthew Ballard (he/him) 19:23

  https://github.com/leanprover-community/mathlib4/pull/6539 has the benchmark results

• Matthew Ballard (he/him) 21:41

  Apparently the changes also addressed the slowness that ACL was talking about for the algebra instance on a quotient of MvPolynomial

[Matthew Ballard]

Hey, there were far less than 25 minute of me starting at the screen ;)

[Matthew Ballard]

It's happening!

[Matthew Ballard]

A pressing unresolved question: what the does the e in erw stand for?

[Ruben Van de Velde]

Euler's number?

[Matthew Ballard]

It could be!

[Thomas Murrills]

:fire:EXTREME:fire: rw

[Mario Carneiro]

I tracked it down to the original commit: https://github.com/leanprover-community/lean/commit/e2f70371cc6c3527930eb1a6ad30fd0730d116aa . It didn't help.

[Mario Carneiro]

https://cmu.zoom.us/rec/share/fdJnR6o1FAbQR4m43S60_6lm0QYYz79XAvd12m9kwVGEo5F666C0kqDxEE_Zt1U5.TeLi1rKDY2xrzxRu?startTime=1692647990000
Passcode: L12p@!yj

[Floris van Doorn]

Matthew Ballard said:

A pressing unresolved question: what the does the e in erw stand for?

In an email on 26 Jan 2017 to the lean-user Google group (an old Lean mailing list) Leo writes

[you can] use the "expensive" rewrite tactic erewrite. This version will unfold all declarations that are not marked as irreducible. This option works well for simple things, but you may have performance problems

so I think that is the intended interpretation of the e.

[Thomas Murrills]

Nice—mystery solved, I’d say! Btw, in searching zulip for answers initially, I stumbled across this old message (Oct 2022), and I suppose the sentiment is even more justified now in light of that:
Mario Carneiro said:

It occurs to me that erw should maybe be renamed to rw! to follow this naming convention (it is the reducibility := .default version of rw)

[Johan Commelin]

Matthew Ballard said:

A pressing unresolved question: what the does the e in erw stand for?

I've been calling it "engry rewrite" lately :angry: :very_angry: --- :grinning:

[Jeremy Tan]

erw stands for Extra-strength rewrite

[Mario Carneiro]

I think we might have got bored of these meetings, the turnout was quite low again. So I propose we (1) renegotiate timing, since it's a new semester for many of us, (2) lower the frequency, and (3) rebrand, as it's not a porting meeting anymore. Continued in #lean4...

[Patrick Massot]

I intended to attend but I didn't know the time.