Lean 4 port

Stream: sphere eversion

[Patrick Massot]

I'm now settled in Pittsburgh, so I now have time to work on the sphere eversion port. @Yury G. Kudryashov could you describe the current status of your efforts? I see you worked in the lean4 branch of the project, and I also saw commits in mathlib clearly coming from this project. Could you tell me more?

[Patrick Massot]

The beginning isn't too promising:

~/lean/sphere-eversion4$ lake build
error: dependency mathlib of SphereEversion not in manifest, use `lake update` to update

~/lean/sphere-eversion4$ lake update
cloning https://github.com/leanprover-community/mathlib4.git to lake-packages/mathlib
warning: improperly formatted manifest: unknown manifest version `5`
cloning https://github.com/leanprover/std4 to lake-packages/std
cloning https://github.com/gebner/quote4 to lake-packages/Qq
cloning https://github.com/JLimperg/aesop to lake-packages/aesop
cloning https://github.com/mhuisi/lean4-cli.git to lake-packages/Cli
cloning https://github.com/EdAyers/ProofWidgets4 to lake-packages/proofwidgets
warning: improperly formatted manifest: unknown manifest version `5`

[Patrick Massot]

@Mac Malone any idea?

[Kyle Miller]

I had a similar error today -- I think you need to make sure your lean-toolchain file matches mathlib's?

[Mac Malone]

@Patrick Massot I believe @Kyle Miller is right: the lean-toolchain is not up-to-date with mathlib's.

[Patrick Massot]

It's not meant to be up to date with current mathlib.

[Patrick Massot]

I believe the problem is that Yury didn't commit the manifest file.

[Patrick Massot]

I'm trying to create a manifest by hand.

[Patrick Massot]

But I think it is still a serious problem that lake suggests commands that make things worse.

[Patrick Massot]

I give up. I'll wait to see whether @Yury G. Kudryashov has a copy of the project that works (presumably including a lake-manifest.json)

[Mac Malone]

Patrick Massot said:

But I think it is still a serious problem that lake suggests commands that make things worse.

Interesting. The thought process with the current errors is: (1) The initial problem is that there is no manifest, so Lake suggests running lake update to create it. (2) Running lake update downloads mathlib, but the mathlib is too new, so it reports it does not know anything about the newer manifest version (5) being used by mathlib.

What were you hoping it would report? I would be happy to adjust the error messages here to make things clearer!

[Patrick Massot]

I think in the absence of manifest there is nothing to suggest apart from asking whoever forgot to commit the manifest to do it.

[Mac Malone]

@Patrick Massot The problem here is that Lake cannot easily tell the difference between a user who checkout a repository without a manifest (and thus needs to ask for it) and a developer who needs to generate it (which is essentially what Lake is currently assuming you are).

[Yury G. Kudryashov]

Sorry, I had an untracked manifest. Pushed.

[Yury G. Kudryashov]

It would be nice if someone who knows how it works will setup CI.

[Yury G. Kudryashov]

I have a WIP mathlib branch with equivariant (w.r.t +c) maps. I'll try to make it compile & open a CI tomorrow.

[Yury G. Kudryashov]

Updated to the latest version. Let's see how many files compile...

[Kyle Miller]

@Mac Malone It could tell you about this -- here's a possibility:

~/lean/sphere-eversion4$ lake build
error: Dependency mathlib of SphereEversion not in manifest since a manifest does not exist.
If this is a checked-out repository, check with the developer of SphereEversion to see if they forgot to include a manifest file.
Otherwise, use `lake update` to generate a manifest.

[Kyle Miller]

~/lean/sphere-eversion4$ lake update
cloning https://github.com/leanprover-community/mathlib4.git to lake-packages/mathlib
warning: lean-toolchain file does not match lake-packages/mathlib/lean-toolchain
warning: improperly formatted manifest: unknown manifest version `5`
...

[Mac Malone]

Kyle Miller Thanks for the suggestions! I thin your improvement of the lake build error is great!

warning: lean-toolchain file does not match lake-packages/mathlib/lean-toolchain

This is probably too strict, we generally want Lake to permit packages to have mismatched toolchains. Even in mathlib, all of its dependencies are rarely on the same toolchain.

[Kyle Miller]

It's just a warning, but an info: would be great too. It's something I'd like to be aware of when doing lake update (bonus: have it say what the toolchain differences are? maybe do it only in some verbose mode?)

[Patrick Massot]

Thanks Yury! I'll take a look but avoid files about equivariant maps.

[Patrick Massot]

Actually I won't because:

info: downloading component 'lean'
Error(Download(Msg("error during download")), State { next_error: Some(Error { description: "Timeout was reached", code: 28, extra: Some("Connection timeout after 30000 ms") }), backtrace: InternalBacktrace { backtrace: None } })
error: could not download file from 'https://github.com/leanprover/lean4/releases/expanded_assets/v4.0.0-rc4' to '/home/pmassot/.elan/tmp/nsceebrvvvd3xbmf_file'

[Patrick Massot]

Using elan toolchain install leanprover/lean4:v4.0.0-rc4 worked but it's hard to know whether this is due to a GitHub glitch.

[Patrick Massot]

I just pushed https://github.com/leanprover-community/sphere-eversion/commit/b221ceb4dcc346644824bdb68919fdd44f2b2da1 which is very weird since it mostly reverts https://github.com/leanprover-community/sphere-eversion/commit/8d4eba3f477ef75892f68986257e10480b83cd1c that was meant to fix that file.

[Patrick Massot]

I started to port the file defining 1-jet bundles here. It's no longer uniformly red, but there are lots of errors remaining, especially simp failures. I would really appreciate getting some help there. @Floris van Doorn @Yury G. Kudryashov @Heather Macbeth

[Yury G. Kudryashov]

I'm busy this week-end. I can have a look on Monday.

[Patrick Massot]

Thanks. Hopefully someone else isn't in a time-zone where it's already week-end.

[Mario Carneiro]

it's always the weekend somewhere :grinning:

[Yury G. Kudryashov]

I meant, I'm busy before and on weekend (teaching, preparing tests, family).

[Patrick Massot]

It seems I ported everything that didn't depend on either equivariant or 1-jet bundles so I''ll probably fix the equivariant map file without waiting for your branch.

[Patrick Massot]

I need to stop for today since it's time to take care of my family and then finish preparing my next lecture. But I made very good progress. If you set aside differential geometry files, fixing the mathport output is very easy. It requires patience but very little thinking.

[Yury G. Kudryashov]

#6143 needed some thinking

[Yury G. Kudryashov]

I was getting very strange error messages in the SEP.

[Yury G. Kudryashov]

Possibly, I renamed some vars before fixing it in mathlib.

[Yury G. Kudryashov]

BTW, find build/lib/SphereEversion -name \*.olean | wc -l gives 61 (out of 86) now

[Patrick Massot]

I finished porting the loop chapter.

[Patrick Massot]

I try to take the opportunity to discuss many regressions that people didn't fully solved when porting mathlib, as can be seen in the lean4 and mathlib4 streams. However this afternoon I got tired of minimizing and discussing, so I rushed through the last two files, as you can see from the porting notes, especially in the Loops.Exists file. It's good to see files ported, but it is not realistic to continue without at least some fixes to simp. This simply won't work for manifold files.

[Patrick Massot]

In addition to issues with simp, I'm faced with lots tactic state explosion issues. I would appreciate some help from @Floris van Doorn or @Kyle Miller. In Lean 3 I can see things like:

h: (⇑(⇑𝓕 t) (s, x)).fst = (⇑(𝓕₀.uncurry) (s, x)).fst ∧ (⇑(⇑𝓕 t) (s, x)).snd = (⇑(𝓕₀.uncurry) (s, x)).snd
⊢ (⇑(⇑(𝓕.curry) (t, s)) x).fst = (⇑(⇑𝓕₀ s) x).fst ∧ (⇑(⇑(𝓕.curry) (t, s)) x).snd = (⇑(⇑𝓕₀ s) x).snd

which become in Lean 4:

h: (↑{ f := FamilyJetSec.f 𝓕.toFamilyJetSec t, f_diff := (_ : 𝒞 ⊤ (↿𝓕.f ∘ fun x => (t, _root_.id x))),
            φ := FamilyJetSec.φ 𝓕.toFamilyJetSec t, φ_diff := (_ : 𝒞 ⊤ (↿𝓕.φ ∘ fun x => (t, _root_.id x))) }
        (s, x)).fst =
    JetSec.f (FamilyFormalSol.uncurry 𝓕₀).toJetSec (s, x) ∧
  (↑{ f := FamilyJetSec.f 𝓕.toFamilyJetSec t, f_diff := (_ : 𝒞 ⊤ (↿𝓕.f ∘ fun x => (t, _root_.id x))),
            φ := FamilyJetSec.φ 𝓕.toFamilyJetSec t, φ_diff := (_ : 𝒞 ⊤ (↿𝓕.φ ∘ fun x => (t, _root_.id x))) }
        (s, x)).snd =
    JetSec.φ (FamilyFormalSol.uncurry 𝓕₀).toJetSec (s, x)
⊢ (JetSec.φ (FamilyFormalSol.uncurry 𝓕₀).toJetSec (s, x)).comp (inr ℝ P E) =
  (↑{ f := FamilyJetSec.f 𝓕₀.toFamilyJetSec s, f_diff := (_ : 𝒞 ⊤ (↿𝓕₀.f ∘ fun x => (s, _root_.id x))),
          φ := FamilyJetSec.φ 𝓕₀.toFamilyJetSec s, φ_diff := (_ : 𝒞 ⊤ (↿𝓕₀.φ ∘ fun x => (s, _root_.id x))) }
      x).snd

Note that I can do change ((𝓕.curry (t, s)) x).1 = (𝓕₀ s x).1 ∧ ((𝓕.curry (t, s)) x).2 = (𝓕₀ s x).2, but the tactic state display stays the same. This is here.

[Patrick Massot]

I really doesn't help debugging the sea of simp failures.

[Floris van Doorn]

I unfortunately have no time at all to investigate this right now... Good luck!

[Anatole Dedecker]

I think the typical fix is to give a name to the coercion, tag it as @[coe], and then use that in the Coe/CoeTC/... instance.

[Eric Wieser]

I really think it would help if the default for pp.proofs.withType was false not true

[Eric Wieser]

I don't know whether we should campaign for a core change, or just add that to mathlib's lakefile.lean

[Eric Wieser]

But for that specific goal, it looks like the coe_mk simp lemma sending ↑{ f := f, f_diff := _} x to f x is missing

[Patrick Massot]

Missing simp lemmas don't explain why tactic state is impossible to read. This seems to be a printing issue.

[Eric Wieser]

The printing issue is pp.proofs.withType

[Eric Wieser]

But the goal state is genuinely different as well

[Anatole Dedecker]

It's true that the tactic state seems different, but I've tested adding @[coe] attributes and it brings back the goal to two lines

[Anatole Dedecker]

pp.proofs.withType makes things worse, but the true issue is that we shouldn't see the actual implementation of the coercions at all (that's the point of coercions)

[Eric Wieser]

Is the real problem here that we're not using FunLike?

[Patrick Massot]

Where did you add the coe attribute?

[Patrick Massot]

Eric, you're looking in the wrong direction. We are talking about regression from Lean 3 to Lean 4. In Lean 3 everything worked.

[Patrick Massot]

So there is a fundamental issue independent of FunLike.

[Eric Wieser]

FunLike is pretty much our workaround to make coe behave like it did in Lean 3 though (as well as solving the problems it solved in Lean 3)

[Eric Wieser]

Otherwise Lean4 just unfolds everything, which is even worse due to nested structures

[Patrick Massot]

But FunLike already existed in Lean 3.

[Eric Wieser]

We added a lot of FunLike instances when porting for this reason

[Patrick Massot]

Ok, I see. It still looks like a very serious regression to me. The fact that a workaround was found during porting instead of fixing Lean 4 may be bad in the long run.

[Anatole Dedecker]

I just pushed to anatole/lean4 branch. Changes are here, here and here

[Anatole Dedecker]

Basically this is a consequence of coe not existing as a function anymore. The up arrow is now replaced inline by the actual definition of the coercion. But to be displayed back as an arrow, this definition needs to be given a name and the @[coe] attribute. The FunLike trick is just a way to "undo" this by saying that a bunch of coercions are actually just defined as FunLike.coe.

[Patrick Massot]

You mean https://github.com/leanprover-community/sphere-eversion/compare/lean4...anatole/lean4
What is this new @[coe] abbrev dance?

[Anatole Dedecker]

Basically this is a consequence of coe not existing as a function anymore. The up arrow is now replaced inline by the actual definition of the coercion. But to be displayed back as an arrow, this definition needs to be given a name and the @[coe] attribute.

:up:

Essentially, ignoring any FunLike shenanigans, the new rule is that all CoeX instances should look like

instance : CoeX A B := ⟨foo⟩

where foo is a def/abbrev with @[coe].

[Eric Wieser]

I think it would be better to replace that CoeFun instance with a FunLike instance, rather than putting coe on an abbrev

[Eric Wieser]

Though maybe it's not injective, in which case I'd suggest that abbrev might still be asking for trouble and def would be safer

[Patrick Massot]

It is definitely injective.

[Eric Wieser]

In fact, its base class already has a funlike instance

[Anatole Dedecker]

Note that it doesn't work for the first coercion in this file though (so we need to do it manually)

[Eric Wieser]

even replacing

instance (R : RelLoc E F) : CoeFun (FamilyFormalSol P R) fun _ => P → JetSec E F :=
  ⟨fun S t =>
    { f := S.f t
      f_diff := S.f_diff.comp (contDiff_const.prod contDiff_id)
      φ := S.φ t
      φ_diff := S.φ_diff.comp (contDiff_const.prod contDiff_id) }⟩

with

instance (R : RelLoc E F) : CoeFun (FamilyFormalSol P R) fun _ => P → JetSec E F :=
  ⟨fun S => S.toFamilyJetSec⟩

would help a lot

[Patrick Massot]

Indeed it makes things a lot nicer.

[Patrick Massot]

Thanks Anatole and Eric!

[Anatole Dedecker]

I wasn't very active during the port, but do I remember correctly that the point of having this unique FunLike.coe name for FunLike coercions was to make sure that generic lemmas like docs#map_add would still apply?

[Patrick Massot]

I am still really worried that all this makes Lean 4 a lot harder to use than Lean 3.

[Anatole Dedecker]

Eric Wieser said:

Though maybe it's not injective, in which case I'd suggest that abbrev might still be asking for trouble and def would be safer

I went with abbrev because I didn't want to fix failures later due to slightly-heavier rfls, I don't know if it's worse than def

[Patrick Massot]

I also don't understand why dot notation became opt-in (using @[pp_dot]) instead of opt-out as in Lean 3. This also make a lot of goals hard to read.

[Patrick Massot]

After another rather frustrating and intense day of work, I'm pleased to announce the local story is fully ported. This includes the appendix, so Lean 4 knows about to turn a sphere inside-out!

[Patrick Massot]

But it still doesn't know this follows from a much more general theorem since this would involve fixing files using the differential geometry part of Mathlib. I don't think I can do that without help from either @Floris van Doorn or @Heather Macbeth.

[Patrick Massot]

The good news is we are only 10 files away from porting the whole project.

[Patrick Massot]

But everything is blocked on SphereEversion.Global.OneJetBundle.

[Yury G. Kudryashov]

When I was doing initial port, I left some sorrys.

[Patrick Massot]

'sphere_eversion_of_loc' depends on axioms: [propext, Classical.choice, Quot.sound]

[Patrick Massot]

No sorry there.

[Kevin Buzzard]

Congratulations to Patrick and the team! Porting is a lot of effort and this work is nontrivial.

[Patrick Massot]

I have some porting update. Since Leo worked on the simplifier recently, I decided to resume the sphere eversion porting effort. I'm trying a new strategy to get help. I am fixing definitions and statement but putting sorries on proofs whose fix isn't obvious. This includes a lot of failing simp of course. Most of them probably come from Lean 4 being a lot more picky about not abusing defEq, but some may also come from little differences in definitions coming from the way Lean 4 handles coercions for instance. The files that are currently in this state are:

• OneJetBundle
• TwistedOneJet
• Relation
• ParametricityForFree

[Patrick Massot]

An interesting problem in ParametrictyForFree is that heterogeneous operations in Lean 4 makes life a lot harder for the elaborator when the Lean 3 version used several nested defEq. This is the only place in Lean code I wrote since 2017 where I had to manually use a hard type ascription with id.

[Patrick Massot]

Help removing those sorries would be very much appreciated. @Floris van Doorn @Oliver Nash @Heather Macbeth @Yury G. Kudryashov

[Ruben Van de Velde]

I looked at one proof and got it to work:

--- SphereEversion/Global/OneJetBundle.lean
+++ SphereEversion/Global/OneJetBundle.lean
@@ -224,13 +224,28 @@ theorem oneJetBundle_chartAt_apply (v v' : OneJetBundle I M I' M') :
 theorem oneJetBundle_chart_source (x₀ : J¹MM') :
     (chartAt HJ x₀).source =
       π (E →L[𝕜] E') FJ¹MM' ⁻¹' (chartAt (ModelProd H H') x₀.proj).source := by
-  sorry
-  /- simp only [FiberBundle.chartedSpace_chartAt, trivializationAt_one_jet_bundle_source, mfld_simps]
-  simp_rw [prod_univ, ← preimage_inter, ← Set.prod_eq, preimage_preimage, inter_eq_left_iff_subset,
+  -- Porting note: was
+  -- simp only [FiberBundle.chartedSpace_chartAt, trivializationAt_one_jet_bundle_source, mfld_simps]
+  rw [FiberBundle.chartedSpace_chartAt]
+  simp_rw [
+    LocalHomeomorph.trans_toLocalEquiv,
+    LocalEquiv.trans_source,
+    LocalHomeomorph.prod_toLocalEquiv,
+    LocalEquiv.prod_source,
+    LocalHomeomorph.coe_coe,
+    Trivialization.coe_coe,
+    LocalHomeomorph.refl_localEquiv,
+    LocalEquiv.refl_source,
+    prodChartedSpace_chartAt,
+    LocalHomeomorph.prod_toLocalEquiv,
+    trivializationAt_one_jet_bundle_source,
+    LocalEquiv.prod_source,
+    Set.preimage_inter]
+  simp_rw [prod_univ, ← preimage_inter, ← Set.prod_eq, preimage_preimage, inter_eq_left,
     subset_def, mem_preimage]
   intro x hx
   rwa [Trivialization.coe_fst]
-  rwa [trivializationAt_one_jet_bundle_source, mem_preimage, ← Set.prod_eq] -/
+  rwa [trivializationAt_one_jet_bundle_source, mem_preimage, ← Set.prod_eq]

 /-- In `J¹(M, M')`, the target of a chart has a nice formula -/
 theorem oneJetBundle_chart_target (x₀ : J¹MM') :

Pretty labour-intensive to find a working simp_rw order on the lean 3 side first, unfortunately.

Not sure if it would be desirable to land this (or whether I have push access anyway)

[Patrick Massot]

Thanks a lot Ruben. Unfortunately I don't have a more efficient approach to "Pretty labour-intensive to find a working simp_rw order on the lean 3 side first, unfortunately.". Could you open a PR? I'll try to get a better proof, but I'll start with yours.

[Ruben Van de Velde]

https://github.com/leanprover-community/sphere-eversion/pull/86

[Patrick Massot]

Thanks!

[Patrick Massot]

Porting update: all definitions and statements are now ported. Concretely it means the full project compiles in Lean 4 but there are about 50 to 60 sorries in proofs. Those sorries are not meant to be coming from name issues. Most of them are failing simp or rw. Help is still very welcome. @Floris van Doorn, @Oliver Nash, @Heather Macbeth.

[Patrick Massot]

Actually a more precise number of sorries upper bound is 44. All hits outside of the Global folder are either in commented out code or unused code.

[Patrick Massot]

The real nightmare is any proof that involved simp .. with mfld_simps. They all fail in Lean 4 and there is no way to see which lemmas where applied in Lean 3 because squeeze_simp simply repeats with mfld_simps.

[Patrick Massot]

Down to 21 sorries.

[Mario Carneiro]

what is the issue with mfld_simps?

[Mario Carneiro]

The syntax has changed but it should still work

[Patrick Massot]

Mario, the issue is first that simp using mfld_simps typically hides a simp with 20 to 50 lemmas, so there are lots of opportunity for a simp regression to show up. And then the huge issue is that in Lean 3, squeeze_simp will not report any of those 50 lemmas.

[Eric Rodriguez]

painful, but can't a list of all mfld_simps be gathered, and then copy-pasted round the Lean3 codebase to see what squeeze_simp uses?

[Patrick Massot]

I will probably end up doing something like this, but I'm not looking forward to it.

[Mario Carneiro]

rather than copy paste, you could make a macro squeeze_simp' which calls squeeze_simp with those 50 lemmas

[Eric Wieser]

I would guess the issue is that @[mfld_simps] means "call simp [my_lemma, my_other_lemma]", but you're in a situation where you actually need simp [(my_lemma), (my_other_lemma)]

[Patrick Massot]

Do we have a Lean 4 issue about this crazy parentheses thing?

[Eric Wieser]

I couldn't find one. It seems that a recent lean patch removed the need for ~90% of the workarounds we had in mathlib (my PR removing them was recently merged), but there's still one left, and I've been seeing the problem in my PR branches. I suspect there are lots of cases where the person porting wasn't aware of the () trick, and so found a different solution without leaving a breadcrumb to the issue

[Mario Carneiro]

import tactic.squeeze
import data.set.basic

setup_tactic_parser

namespace tactic
namespace interactive

private meta def split_brackets : option string.iterator → string.iterator → list string
| none it :=
  if it.has_next then
    if it.prev.curr = '\n' ∧ it.curr = '[' then
      split_brackets (some it.next) it.next
    else
      split_brackets none it.next
  else
    []
| (some start) it :=
  if it.has_next then
    if it.curr = ']' then
      (start.extract it).get_or_else "" :: split_brackets none it.next
    else
      split_brackets (some start) it.next
  else
    []

meta def parse_simp_lemmas (s : simp_lemmas) : tactic (list name) := do
  f ← simp_lemmas.pp s,
  let s := f.to_string (options.mk.set_nat `pp.width 100000),
  pure $ (split_brackets none s.mk_iterator).map name.from_string

meta def squeeze_simp'
  (key : parse cur_pos)
  (slow_and_accurate : parse (tk "?")?)
  (use_iota_eqn : parse (tk "!")?) (no_dflt : parse only_flag) (hs : parse simp_arg_list)
  (attr_names : parse with_ident_list) (locat : parse location)
  (cfg : parse struct_inst?) : tactic unit := do
hs ← attr_names.mfoldl (λ hs attr, do
  S ← get_user_simp_lemmas attr,
  names ← parse_simp_lemmas S,
  pure $ hs ++ names.map (λ c, simp_arg_type.expr (expr.const c []))
) hs,
squeeze_simp key slow_and_accurate use_iota_eqn no_dflt hs [] locat cfg

end interactive
end tactic

open set
theorem mem_univ {α} (x : α) : x ∈ @univ α := by squeeze_simp' with mfld_simps
-- Try this: simp only [set.mem_univ]

[Patrick Massot]

Thank you very much Mario!

[Patrick Massot]

I'm down to four sorries, all involving mfld_simps. It's time to play with Mario's macro...

[Patrick Massot]

And now some bad news: Mario's macro works in an empty file, but trying to use it on a real example leads to deterministic timeout.

[Mario Carneiro]

Here's another version of the tactic:

meta def explain_simp
  (key : parse cur_pos)
  (slow_and_accurate : parse (tk "?")?)
  (use_iota_eqn : parse (tk "!")?) (no_dflt : parse only_flag) (hs : parse simp_arg_list)
  (attr_names : parse with_ident_list) (locat : parse location)
  (cfg : parse struct_inst?) : tactic unit := do
(cfg',c) ← parse_config cfg,
args ← attr_names.mfoldl (λ hs attr, do
  S ← get_user_simp_lemmas attr,
  names ← parse_simp_lemmas S,
  pure $ hs ++ names.map (λ c, simp_arg_type.expr (expr.const c []))
) hs,
let use_iota_eqn' := if use_iota_eqn.is_some then "!" else "",
let loc := loc.to_string locat,
mk_suggestion (key.move_left 1)
  sformat!"Try this: simp{use_iota_eqn'} only"
  sformat!"{loc}{c}" args,
simp use_iota_eqn none no_dflt hs attr_names locat cfg'

This one doesn't try to do any squeezing, it just gives you the whole list of lemmas

[Patrick Massot]

Thanks. I've manage to reprove many lemmas by hand, using lots of rw? (unfortunately rw_search never managed to do it). There is a very nasty remaining one but I made good progress. I need to go now, but I hope I'll have a sorry-free version tonight.

[Patrick Massot]

I just finished porting the sphere eversion project to Lean 4! The master branch is now using Lean 4, and the main theorem are fully sorry-free. Huge thanks to @Yury G. Kudryashov for his crucial help during summer.

[Patrick Massot]

An interesting data point for people interested in mathport (@Mario Carneiro). Yury ran mathport on July 16th and then we never ran it again. There were many bumps of lean4+Mathlib4 during the port, but I never felt the need to re-run mathport. I simply fixed stuff after each bump in the same way I would be have been fixing a project outside a porting effort.

[Kevin Buzzard]

Congratulations! Are there more parts of it which should move to mathlib? Do you intend to keep it compiling with mathlib master?

[Patrick Massot]

I think all of it could move to mathlib, but not all of it is ready.

[Mario Carneiro]

I think it makes sense that you wouldn't be re-running mathport, since the aligns aren't being updated much - doing the bumps by hand is probably the best we can do at the moment. I am hoping that we get better automatic migration tooling for mathlib, because the instability of mathlib is a major issue for using it as a library

[Patrick Massot]

My point was precisely to give one more data point suggesting it is not useful to keep aligns around, or work on maintaining them. The question of having better tooling for Mathlib bumps in projects depending on Mathlib is different, and certainly very important.

[Mario Carneiro]

I'm not sure that this is true at all / can be derived from your observation. If the #aligns weren't present I think you would have more difficulty running mathport if you were starting the port today instead of in july

[Mario Carneiro]

Also, the difficulty of mathlib bumping will grow linearly with time since port-complete or whenever we decide to stop updating mathport. You were staying up to date the entire time from july until now, so the bumps were not so bad, but doing it all in one go would probably have been a lot harder and that's what most people are faced with going forward

[Patrick Massot]

I don't say we can derive anything from this observation. this is why I was careful to speak about "one data point".

[Patrick Massot]

It would be really useful to know whether there is any big project that want to be ported to Lean 4 but hasn't started yet.

[Floris van Doorn]

Thank you for pushing forward the port Patrick! I'm sorry I couldn't help at all lately.

[Oliver Nash]

Thank you Patrick!

[Yaël Dillies]

Patrick Massot said:

It would be really useful to know whether there is any big project that want to be ported to Lean 4 but hasn't started yet.

LeanAPAP was ported in September, fwiw.

[Mario Carneiro]

Patrick Massot said:

It would be really useful to know whether there is any big project that want to be ported to Lean 4 but hasn't started yet.

LTE is the elephant in the room here, no?

[Mario Carneiro]

I'm guessing that it doesn't "want to be ported", but we still have a ToMathlib folder to mathlib

[Mario Carneiro]

Ditto for flypitch

[Patrick Massot]

I think nobody plans to port LTE.

[Kevin Buzzard]

People are directly implementing lessons learnt from LTE, e.g. Joel Riou has made a heroic effort getting a lot of basic concepts of homological algebra into mathlib; these were all very experimental in LTE, and it took people a while to find the best approach. For example the understanding that the cohomology of a complex was both a limit and a colimit, and needed to be formalised as such in order to minimise pain, was a lesson learnt in LTE. All of this is now in mathlib, but it's not in LTE which set things up in what we now regard as a suboptimal way. So in order to port that part of LTE the entire thing would need to be refactored using Joel's approach first, and that is not high on anyone's job list.

Here's another thing: LTE proved a random theorem about liquid vector spaces, but solid abelian groups are more fundamental so we should probably do those first -- and Dagur is indeed doing this. Even the solid theory is not stable -- Scholze is giving some talks now about "light" versions of these ideas. Somehow parts of the theory are still in flux.