Getting back up to date with Lean + mathlib

Stream: general

[Wrenna Robson]

Hi all. I've been out of sync with Lean stuff for the last six-eight months or so (busy with other stuff), but I'd somewhat like to re-sync myself and read about what the community has been up to and what the state of things is. What's the best way to get myself up to speed/does anyone feel like giving me a potted summary of what I've missed?

[Eric Wieser]

The state of the port (#port-dashboard) is probably the main thing to be aware of right now. Unfortunately we haven't managed to keep up the "this month in lean" blog posts, as curating those is a lot of work that never ends!

[Moritz Doll]

If you want to help with the port, then there is now a script that makes some automatic fixes. The workflow is now: find a unported file on the dashboard, checkout the current master, run scripts/start_port.sh Mathlib/Foo/Bar/Baz.lean and fix all the remaining issues.

[Moritz Doll]

and we have lake exe cache get for getting caches

[Wrenna Robson]

Good to know. Thanks. It would be good to help with the port.

[Jason Rute]

If you are also looking for news/gossip there is this: #general > Moving to AWS

[Wrenna Robson]

As it happens I already heard that gossip a few days earlier via a source <_<

[Wrenna Robson]

For working on port files, do I want to be using stable or nightly?

[Mauricio Collares]

Nightly, but elan should take care of that for you automatically if you work inside the mathlib4 directory

[Wrenna Robson]

Where does one find Mathlib4 docs?

[Henrik Böving]

docs4#Group here

[Wrenna Robson]

Ta. Having a go at porting a file just to understand the process. I'm not sure if my cache download has worked right though as when I open the file I'm just getting the orange bars of death.

[Wrenna Robson]

Hmm - worse yet, it is now red bars.

[Wrenna Robson]

Looks like the build failed.

[Wrenna Robson]

info: Building Aesop.Index
error: > LEAN_PATH=./build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib LD_LIBRARY_PATH=/home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-03-31/lib::/usr/local/lib:/usr/local/lib:./build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib:./build/lib /home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-03-31/bin/lean -DwarningAsError=true -Dpp.unicode.fun=true ./././Mathlib/Init/Logic.lean -R ././. -o ./build/lib/Mathlib/Init/Logic.olean -i ./build/lib/Mathlib/Init/Logic.ilean -c ./build/ir/Mathlib/Init/Logic.c
error: stdout:
./././Mathlib/Init/Logic.lean:275:70: error: unsolved goals
a b c d : Prop
p : ?m.25422
h : Decidable False
⊢ ¬False
error: external command `/home/wrobson/.elan/toolchains/leanprover--lean4---nightly-2023-03-31/bin/lean` exited with code 1

Anyone got any suggestions?

[Wrenna Robson]

It does look like Mathlib.Init.Logic has an issue, having opened it directly...

[Eric Wieser]

You have to ensure nothing is building your code when you get the cache, otherwise that running lean process may overwrite cache files as they're downloaded

[Wrenna Robson]

Aha.

[Wrenna Robson]

So kill all lean processes before I get it.

[Wrenna Robson]

Still not really sure why Mathlib.Init.Logic broke (it didn't when I rolled back to master...)

[Wrenna Robson]

Hmm - still getting orange bars. But Mathlib.Init.Logic builds now. Let's see if the bars resolve.

[Wrenna Robson]

Ah, there we go. A little slow but fine.

[Wrenna Robson]

Two questions: in Lean 4, is there an equivalent of include/omit statements. And where is there a list of Mathlib4 linters?

[Johan Commelin]

include/omit are gone. Instead, all variables are automatically included, but once the proof/statement is done, all the unused variables are automatically omitted.

[Johan Commelin]

This creates the small risk that one (or more likely, some automation) uses a variable that would not have been included in Lean 3.

[Wrenna Robson]

Yeah - the particular pattern I am running into is somewhere where a definition doesn't use a variable but you want to make it dependent on it anyway.

[Johan Commelin]

Yeah, in that case you have to manually include it in the statement.

[Wrenna Robson]

Cool.

[Wrenna Robson]

Hmm (sorry to ask so many little questions). I have a linear map - there's an "apply"-style lemma, where it is being coerced to a function. But the coercion doesn't seem to be happening.

[Wrenna Robson]

Linear maps should still be able to be used like functions, right?

[Wrenna Robson]

Ah it seems like it's because the type of the function is implicit...

[Wrenna Robson]

noncomputable def single (i : ℕ) : M →+ PolynomialModule R M :=
  Finsupp.singleAddHom i
#align polynomial_module.single PolynomialModule.single

theorem single_apply (i : ℕ) (m : M) (n : ℕ) : single R i m n = ite (i = n) m 0 :=
  Finsupp.single_apply
#align polynomial_module.single_apply PolynomialModule.single_apply

/-- `polynomial_module.single` as a linear map. -/
noncomputable def lsingle (i : ℕ) : M →ₗ[R] PolynomialModule R M :=
  Finsupp.lsingle i
#align polynomial_module.lsingle PolynomialModule.lsingle

theorem lsingle_apply (i : ℕ) (m : M) (n : ℕ) : lsingle R i m n = ite (i = n) m 0 :=
  Finsupp.single_apply
#align polynomial_module.lsingle_apply PolynomialModule.lsingle_apply

So why is it happy with single_apply, in which single coerces to a function of type (M → (ℕ → M)), but in lsingle_apply it appears to not be able to work out that lsingle R i can coerce to a function of the same type.

[Wrenna Robson]

I am wondering if it cannot find an AddHomClass instance for LinearMap...

[Wrenna Robson]

Yeah... I think maybe? https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Hom/Group.html#AddHomClass

[Wrenna Robson]

Yes. The definition of semilinear_map_class (https://leanprover-community.github.io/mathlib_docs/algebra/module/linear_map.html#semilinear_map_class) seems to automatically create semilinear_map_class.to_add_hom_class. However, no such instance exists for SemilinearMapClass (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/LinearMap.html#SemilinearMapClass).

[Riccardo Brasca]

You can try

set_option synthInstance.etaExperiment true

just before the theorem (I don't understand all the details, but it sometimes works).

[Wrenna Robson]

That has made it work, but I do think the issue I've identified above is an issue?

[Wrenna Robson]

LinearMap extends AddHom but there is no corresponding instance of AddHomClass I think.

[Wrenna Robson]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Hom/Group.html#AddHomClass very clearly states that an instance of it should be declared whenever you extend AddHom (I think probably with the name instAddHomClass) but this does not exist.

[Wrenna Robson]

semilinear_map_class.to_add_hom_class was auto-generated before from however extending a class was defined.

[Eric Wieser]

docs4#SemilinearMapClass.addMonoidHomClass exists. The extends-generated instance just isn't shown in the docs, I think

[Wrenna Robson]

That was previously semilinear_map_class.add_monoid_hom_class. semilinear_map_class.add_monoid_hom_class and semilinear_map_class.to_add_hom_class are I think different.

[Wrenna Robson]

The latter uses out_param, for one thing...

[Wrenna Robson]

Indeed, yes, they are different.

[Wrenna Robson]

Ah: as you note here, Eric, I suppose this is a new-style-structures issue? https://github.com/leanprover/lean4/issues/2074

[Wrenna Robson]

I can use this experimental fix, and I see that it is used many times in the port, but given that it is explictly for testing only I don't feel great about that...

[Jeremy Tan]

I use with great impunity

[Wrenna Robson]

@Gabriel Ebner might have some thoughts given aiui it's his fix?

[Jireh Loreaux]

@Wrenna Robson the lean4#2074 issue is one which Gabriel and others have been giving lots of thought. We have collectively decided that for the time being we will use the experimental eta option to get past issues while porting. At some point, either we will restructure classes in mathlib (via one of a few different possible methods) or there will be a fix which implements eta for TC synthesis in a feasible way. So, yes, it's a problem, but for the moment we're just working around it with this option. Don't feel bad about using it, especially for linear maps / modules which is a key place that needs it.

[Wrenna Robson]

Super, thank you for the clear guidance.

[Jireh Loreaux]

Some other things you can try instead of eta: attribute [-instance] Ring.toNonAssocRing. This deletes a particularly unfortunate path that TC synthesis takes to get an AddCommGroup instance from a Ring instance and hence forces TC synthesis to take a different route. You can try this if, for instance, using eta causes things to get unbearably slow (which is possible from time to time). There are a few other hacks lying around mathlib and on Zulip, you can grep for 2074 in mathlib to find them.

[Wrenna Robson]

Yeah definitely noticing those speed issues...

[Wrenna Robson]

Deriving e.g. Algebra instance for PolynomialModule requires the eta experiment, and takes ages...