Porting Mathlib: Essential Changes

Stream: lean4

[Mohamed Al-Fahim]

It would be helpful to list all the essential changes here.

[Mohamed Al-Fahim]

https://leanprover.github.io/lean4/doc/lean3changes.html is a starting point

[Mohamed Al-Fahim]

begin-end Blocks and Commas

Without the macro in https://leanprover.github.io/lean4/doc/tactics.html#begin-end-lovers, begin-end blocks and commas are gone.

[Mohamed Al-Fahim]

> Macro Approach

open Lean in
macro "begin " ts:tactic,*,? "end"%i : term => do
  -- preserve position of the last token, which is used
  -- as the error position in case of an unfinished proof
  `(by { $[$ts:tactic]* }%$i)

theorem ex1 (x : Nat) : x + 0 = 0 + x :=
  begin
    rw Nat.zeroAdd,
    rw Nat.addZero,
  end

> Built-in Approach

theorem ex1 (x : Nat) : x + 0 = 0 + x := by
  rw Nat.zeroAdd
  rw Nat.addZero

[Mohamed Al-Fahim]

I think the non-macro approach would be cleaner in the long-term.

[Mohamed Al-Fahim]

Type*

Without the macro in https://leanprover.github.io/lean4/doc/typeobjs.html, Type* is gone.

[Mohamed Al-Fahim]

> Macro Approach

macro "Type*" : term => `(Type _)

def f (α : Type*) (a : α) := a

def g (α : Type _) (a : α) := a

#check f
#check g

> Built-in Approach

def f (α : Type _) (a : α) := a

def g (α : Type _) (a : α) := a

#check f
#check g

[Mario Carneiro]

I don't think it will be a big deal to switch to by. There is no need to preserve syntax this much, particularly if we're going to be doing the port based on an initial syntax transformation of mathlib to lean 4 style

[Mario Carneiro]

I do think it's worth it to keep Type* and Sort* though, which as I mentioned in another thread can be added to the mathlib prelude

[Bryan Gin-ge Chen]

Rather than figuring out every last syntax / style detail now, it might be more fun to look into writing a linter in Lean 4.

[Mario Carneiro]

syntax aware linters will make things so much better

[Bryan Gin-ge Chen]

I said "linter" but I think I meant "code formatter".

[Mario Carneiro]

@Sebastian Ullrich How close do the delaborator + parenthesizer on full file ASTs get to a pretty-printer style code formatter? leanfmt would be so cool

[Bryan Gin-ge Chen]

I did find this, which seemed related: https://github.com/leanprover/lean4/blob/master/tests/lean/Reformat.lean

[Sebastian Ullrich]

Right, this the output of that test given this input: https://github.com/leanprover/lean4/blob/master/tests/lean/Reformat.lean.expected.out
I've already spent quite a bit of time on getting formatting as pretty as possible both on the command and term level, using both general heuristics (e.g. automatic indentation of subterms) and specific annotations (e.g. hard line breaks after match ... with I mentioned on Gather yesterday), but there are many more of these yet to cover before anyone before the output is acceptable for a code formatter.

[Eric Wieser]

Mario Carneiro said:

I don't think it will be a big deal to switch to by. There is no need to preserve syntax this much, particularly if we're going to be doing the port based on an initial syntax transformation of mathlib to lean 4 style

Is it remotely viable to write a suite of macros that preserves syntax almost exactly, so that the porting process would be:

• Remove all the lean3 expressions that are too weird to fit in those macros, by rewriting them in an uglier way
• Switch to the macro suite, and build all the code as lean 4
• Slowly remove uses of the macros over time and modernize the code to lean 4?

(ie, copy how people managed the python2 to python3 transition)

[Sebastian Ullrich]

Btw, just for completeness: the delaborator and parenthesizer are the exactly the pretty printer components not involved here :) . There are no Exprs involved, nor are we combining different syntax trees such that we could end up with badly parenthesized trees.