## Stream: lean4

### Topic: Porting Mathlib: Essential Changes

#### Mohamed Al-Fahim (Jan 07 2021 at 19:01):

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

#### Mohamed Al-Fahim (Jan 07 2021 at 19:05):

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

## 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.

### > 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
end


### > Built-in Approach

theorem ex1 (x : Nat) : x + 0 = 0 + x := by


#### Mohamed Al-Fahim (Jan 07 2021 at 23:55):

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

## Type*

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

### > 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 (Jan 08 2021 at 00:30):

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 (Jan 08 2021 at 00:31):

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 (Jan 08 2021 at 00:32):

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 (Jan 08 2021 at 00:33):

syntax aware linters will make things so much better

#### Bryan Gin-ge Chen (Jan 08 2021 at 00:36):

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

#### Mario Carneiro (Jan 08 2021 at 00:45):

@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 (Jan 08 2021 at 00:46):

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

#### Sebastian Ullrich (Jan 08 2021 at 10:08):

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 (Jan 08 2021 at 10:10):

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 (Jan 08 2021 at 10:10):

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.

Last updated: May 07 2021 at 11:09 UTC