Mario's FMM 2021 talk

Stream: mathlib4

[Patrick Massot]

Mario Carneiro said:

Here are my slides: Porting_Mathlib.pdf

My internet access here doesn't allow me to attend Zoom talks. Can anyone reveal whether Mario answered any questions about the porting schedule?

[Mario Carneiro]

I estimated one year, but there is a large variance on that. There is nothing like a schedule in terms of milestones

[Patrick Massot]

One year from now?

[Patrick Massot]

It's hard to tell from the slides: did you decide on one strategy (maybe mixing several tools)?

[Mario Carneiro]

less seems plausible, but I still don't know what some stages of the process will actually look like

[Patrick Massot]

What does the grey color mean on Page 26?

[Mario Carneiro]

At that point I said that olean-port and lean3-port are strictly dominated by synport because it has better information to work from

[Mario Carneiro]

and the plan involves all three of the remaining methods

[Mario Carneiro]

the next slide tries to summarize how they interact

[Mario Carneiro]

Daniel has argued that the current binport in the mathport repo is actually somewhere between what I called olean-port and binport

[Patrick Massot]

I really think we shouldn't be afraid of "stop the world and port everything". We simply have to reach a consensus among all mathlib maintainers to simply stop merging stuff. I'm pretty sure everyone is convinced this is extremely important, we are simply waiting for your signal.

[Daniel Selsam]

Patrick Massot said:

It's hard to tell from the slides: did you decide on one strategy (maybe mixing several tools)?

We have not converged on a specific roadmap yet. The solution will very likely involve a mix of synport, binport, delabbing defs/types from binport, running large-scale proof search to fix broken proofs, and then a (still unclear how herculean) manual process at the end. I think there is good chance the whole process takes much less than a year, but TBD

[Mario Carneiro]

as long as we can do that sufficiently quickly it's not a bad strategy. But we need the porting tools to be ready to make sure it is straightforward

[Patrick Massot]

Most people expect it will be a lot of manual work anyway. The key is whether this can be parallelized. It's not only about having several people working in parallel, it's about how much things will diverge (we can fear the early files will force so many variations that the late files will have to be rewritten from scratch).

[Mario Carneiro]

I would really like to avoid that

[Patrick Massot]

Of course I understand we all want to avoid that.

[Mario Carneiro]

We have some really promising results, it might actually be largely automatic

[Patrick Massot]

Anyway, my point is that once you get the tactics working in Lean 4 and you'll be happy with your porting tool then I'm sure we can provide a lot of forces for grunt work.

[Gabriel Ebner]

I don't think there's any way we can avoid a massive cleanup operation afterwards. There's lots of Lean 3-specific workaround and hacks in mathlib after all.

[Mario Carneiro]

The examples on my slides were mostly autogenerated, except for formatting and name resolution (which isn't hooked up yet but will eventually be part of synport)

[Mario Carneiro]

the output was formatted, but it doesn't quite hit the style guide yet

[Patrick Massot]

Mario, how much MSR time do you still have?

[Patrick Massot]

On Page 29, do we have to use the obfuscated Lean 4 forall or can we reintroduced the readable notation, at least in mathlib?

[Patrick Massot]

It's even worse on the next page :sad:

[Mario Carneiro]

until 27 Aug

[Patrick Massot]

Oh, that's too soon. I should stop writing questions and let you work.

[Mario Carneiro]

Right now there is a hole in synport where we insert the "DArrow heuristic" - once types become available it will be easier to use forall for props

[Mario Carneiro]

it is capable of producing both ATM

[Mario Carneiro]

we could just use forall everywhere too

[Mario Carneiro]

but I don't know if people feel Pi should be Pi

[Patrick Massot]

Mathematicians would definitely prefer forall everywhere.

[Mario Carneiro]

lean 3 uses Pi when the codomain is a type

[Patrick Massot]

For us it makes sense that forall and Pi are different, but if we need to choose only one then it's definitely forall

[Mario Carneiro]

also, this is one of the cases where lean forgets which is which very early in parsing so that the AST doesn't record it; if we modify lean to keep track of the distinction we can just use forall iff the user used forall in lean 3, which will probably yield the best results

[Mario Carneiro]

another case is lemma vs theorem, which you will note also shows up in the example. Lean 3 forgets which is which right in the tokenizer, so the parser doesn't export the info

[Mario Carneiro]

But I have heard it said that mathlib's lemma vs theorem markings are way off anyway so maybe preserving them isn't worth it

[Patrick Massot]

Honestly that lemma vs theorem information is not worth fighting for. Our current mathlib is a mess here.

[Mario Carneiro]

also fun vs \lam and -> vs \r

[Patrick Massot]

You already know what mathematicians want (no ascii art, $\mapsto$).

[Daniel Selsam]

Patrick Massot said:

Anyway, my point is that once you get the tactics working in Lean 4 and you'll be happy with your porting tool then I'm sure we can provide a lot of forces for grunt work.

We will not be shy about enlisting this help when it is appropriate. Right now there is still both (a) a lot of low-hanging fruit to improve the automatic part and (b) still too many hard-to-diagnose issues when using the binported oleans for it to be worth having non-devs experimenting with them yet. We may be within ~1 week of solving enough elab issues for it to be extremely useful if users start trying to patch random synport-importing-binport files and reporting issues they hit.

[Kevin Buzzard]

So lemme get this straight: is there any way at all I can have mathlib3's Scheme in Lean 4 right now?

[Mario Carneiro]

You can get a translated Mathlib.scheme in lean 4 right now with binport; a lean 4 file that appears to be defining Scheme but actually has lots of errors is coming soonish

[Daniel Selsam]

@Kevin Buzzard Yes, these .oleans work with Lean4 master: https://github.com/dselsam/mathport/releases/tag/v0.0.0.0 I can also run the same pipeline on other repos e.g. liquid if it would be useful. HOWEVER when trying to use these oleans, you will currently hit subtle yet-to-be-addressed issues elaborating new terms. We are making rapid progress here and the experience should be much better in ~1 week.

[Daniel Selsam]

Most of the remaining issues only emerge once the typeclass instances start getting insanely big later in the library. This works:

import Mathlib.Data.Nat.Prime

namespace Nat

theorem exists_infinite_primes_alt (n : ℕ) : ∃ p, n ≤ p ∧ Prime p :=
  let p := minFac (n.factorial + 1)
  have f1 : n.factorial + 1 ≠ 1 := ne_of_gt $ succ_lt_succ' $ factorial_pos n
  have pp : Prime p := min_fac_prime f1
  have np : n ≤ p := le_of_not_ge $ λ h =>
    have h₁ : p ∣ n.factorial := dvd_factorial (min_fac_pos _) h
    have h₂ : p ∣ 1 := (Nat.dvd_add_iff_right h₁).2 (min_fac_dvd _)
    pp.not_dvd_one h₂
  ⟨p, np, pp⟩

end Nat

Note the annoying prime in the name succ_lt_succ' -- this is due to a clash with the existing one. Still hoping somebody will backport https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/backporting.20Nat.2ELe/near/246798442

[Kevin Buzzard]

I don't really understand what it means to backport Nat.le . Does this mean changing the definition of nat.le in Lean 3 or mathlib or wherever it is to something different and then picking up all the pieces?

[Daniel Selsam]

Yes, it means somehow making Lean's nat.le def-eq-compatible with Lean4's. I suspect the refactor can be contained after patching a small number of proofs and won't leak very far out of the file defining it.

[Notification Bot]

4 messages were moved from this topic to #mathlib4 > lemma vs theorem by Eric Wieser.