Swapping the arguments to `Membership.mem`

Stream: mathlib4

[Matthew Ballard]

The RFC lean#4932 was accepted but mathlib needs to fix itself before it is executed. For context, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Ways.20to.20speed.20up.20Mathlib/near/455951854 and the comments below.

If it wasn't the start of the fall semester, I would take a couple days and just thrash it out. I am sure many people are in a similar situation.

Does anyone foresee spending significant time on fixing a Lean PR branch for this change? If so, we can get one started now. If not, maybe we can wait until there is critical mass.

[Jeremy Tan]

Where is that Lean branch?

[Matthew Ballard]

It doesn't exist yet. There are nontrivial changes to the core tests to make PR toolchains release.

[Matthew Ballard]

#15457 replaces everything that doesn't work with sorry to get a sense of the damage

[Matthew Ballard]

You can see it is has rotted significantly since inception

[Matthew Ballard]

Batteries also needs a fix but that is minor

[Joachim Breitner]

Matthew Ballard said:

It doesn't exist yet. There are nontrivial changes to the core tests to make PR toolchains release.

Is there a lean PR for this? You should get PR toolchain releases even if the core tests fail

[Matthew Ballard]

I should?!

[Matthew Ballard]

The changes to core itself are minor so I'll try now

[Joachim Breitner]

Yes, the job to run the test suite (“Linux nix”) is separate from the job that builds the release (“Linux”), and for the PR release it suffices if the latter fails.

[Matthew Ballard]

I thought tests were also run on certain arch/OS combinations.

[Joachim Breitner]

This may stop working after a mathlib build failed and it added the release-ci label automatically (which I am mildly annoyed by, as it also makes CI take noticably longer, but it’s important for Kim’s workflow to have that label on failing PRs), as that then runs the test suite as part of the release builds.

Hmm, I guess non-developers cannot remove that label. That’s a bit of a snag. Let me know if you run into this.

[Joachim Breitner]

Not in the default PR CI configuration.

[Joachim Breitner]

(They used to at some point)

[Matthew Ballard]

Ok, I have been testing in my fork and probably running a different workflow

[Matthew Ballard]

(You can guess what happens to failing tests there...)

[Matthew Ballard]

lean#5020

[Matthew Ballard]

The yoots may have suffered but there is a working copy of mathlib with this change. #15870 with the comments highlights some things about it.

[Matthew Ballard]

If anyone can figure out why typeclass search is failing all over Lie algebras, even if you declare instances with the correct keys, I would be appreciative.

[Kim Morrison]

I've rebased lean#5020 (it's now based off nightly-2024-08-23, and merged nightly-testing-2024-08-23 into #15870 (which is the branch#lean-pr-testing-5020).

[Kim Morrison]

Still building locally so not sure if I've broken too much during the merge.

[Kim Morrison]

Anyone looking at #15870 who has looked at it previously should run elan toolchain uninstall $(<lean-toolchain) first, to make sure they get the updated toolchain.

[Kim Morrison]

I'm not sure how much time I'll have for this today, so I'll note here places my local build is running into errors. Hopefully @Matthew Ballard, or the authors noted below, can take a look.

[Kim Morrison]

There are new failures in Mathlib/MeasureTheory/Measure/Typeclasses.lean, in new material that @Rémy Degenne added last week.

[Kim Morrison]

Also in Mathlib/Geometry/Manifold/AnalyticManifold.lean, in changes @Geoffrey Irving added a few days ago.

[Kim Morrison]

And in Mathlib/ModelTheory/PartialEquiv.lean, in material added by @Gabin Kolly two weeks ago.

[Kim Morrison]

If any of @Rémy Degenne, @Geoffrey Irving, or @Gabin Kolly have a chance to look at the above mentioned errors, please feel free to push fixes directly to branch#lean-pr-testing-5020.

[Kim Morrison]

(I'm done for now on this branch, having fixed all the merge problems / new problems except the three noted above, so @Matthew Ballard is in charge again. :-) Note that there is still a merge conflict on this PR, so we still need to rebase #5020 again onto nightly-2024-08-25, and then merge nightly-testing-2024-08-25 into lean-pr-testing-5020. I'm hoping @Matthew Ballard can do this one?)

[Geoffrey Irving]

I checked out https://github.com/leanprover-community/mathlib4/pull/15870, but it seems to be currently failing in Batteries.Data.List.Lemmas so I can't see the AnalyticManifold errors:

julia:mathlib4% lake build
✖ [547/4999] Building Batteries.Data.List.Lemmas
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH= /Users/irving/.elan/toolchains/leanprover--lean4-pr-releases---pr-release-5020/bin/lean -Dlinter.missingDocs=true ././.lake/packages/batteries/././Batteries/Data/List/Lemmas.lean -R ././.lake/packages/batteries/./. -o ././.lake/packages/batteries/.lake/build/lib/Batteries/Data/List/Lemmas.olean -i ././.lake/packages/batteries/.lake/build/lib/Batteries/Data/List/Lemmas.ilean -c ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/List/Lemmas.c --json
error: ././.lake/packages/batteries/././Batteries/Data/List/Lemmas.lean:162:97: unsolved goals
α : Type u_1
a : α
n : Nat
l : List α
⊢ Option.map (Function.const α a) l[n]? = Option.map (fun x => a) l[n]?
error: Lean exited with code 1
Some required builds logged failures:
- Batteries.Data.List.Lemmas
error: build failed

[Markus Himmel]

@Geoffrey Irving I have pushed the necessary bumps to the branch (and verified locally that it now gets to AnalyticManifold.lean) so you will be able to look at the error message once CI has finished.

[Matthew Ballard]

Thanks Kim and Markus!

I will get as much done today as I can (teaching + meeting with a grad student + office hours). I looked at the error from AnalyticManifold and I would guess you need a black triangle in place of a .subst.

[Geoffrey Irving]

I'm looking at it now. What's a black triangle?

[Matthew Ballard]

\t I think

[Markus Himmel]

I have just pushed the fix, and Matthew's guess was correct. @Geoffrey Irving, the black triangle \t is a smarter version of Eq.subst.

[Markus Himmel]

There is a new failure in Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean, I'm looking at it now.

[Matthew Ballard]

Same?

[Matthew Ballard]

For reference, docs#Lean.Elab.Term.elabSubst

[Geoffrey Irving]

It’s a shame there is no documentation of how it is different!

[Matthew Ballard]

nightly-2024-08-25 is this a tag? What commit does it represent? Is it aleady done?

[Markus Himmel]

Yes, it's already done :)

[Matthew Ballard]

Thanks! The log for lean#5020 had commits from 8/25 but I couldn't figure out where nightly-2024-08-25 was pointing

[Markus Himmel]

The nightly tags are hosted in a separate repository which you can add as an additional remote to your lean4 checkout: https://github.com/leanprover/lean4-nightly

[Matthew Ballard]

I've got to start getting people ready for school (including myself). I won't be sitting at a computer with any modicum of focus until 2024-08-26T12:00:00-04:00 at the earliest. But I can still try to answer questions here

[Kyle Miller]

(@Geoffrey Irving There's documentation on the syntax docs#Lean.Parser.Term.subst

The thing about Eq.subst is that elaborating the motive argument is difficult (it's a higher-order unification problem). You can think of the triangle operator h ▸ e as being an elaborator that uses both the expected type of the whole expression and the inferred type of e to try to come up with the motive. It also tries using h.symm if it has to. In particular, it's like it does rw [h]; exact e or have this := e; rw [h] at this; exact this, or one of these with h.symm. So, it's comparable in some way to Eq.subst, but I'd say it's like a term version of rw.

Side note: it appears that Eq.subst might be missing @[elab_as_elim]. That would help it infer the motive using the expected type. However, unlike the triangle operator it would not be able to make use of the inferred type of its argument, and it would cause Eq.subst to throw an error if an expected type is not available.)

[Eric Wieser]

Is it possible to write custom elaborators for certain constants, or only via new notation?

[Kyle Miller]

@Eric Wieser You can sort of write custom elaborators for constants (you can key on app syntax, check that the function is an identifier, resolve it, and check that it's the correct global constant), but it's not too hard to imagine there could be a better system! There could be a @[term_app_elab] attribute for creating elaborators for specific constant applications, hooked into the same part of the code that's already checking for the @[elab_as_elim] attribute.

[Eric Wieser]

Can you really write an elaborator rule that matches `($f $x) !?