Zulip Chat Archive

Stream: lean4

Topic: Porting Mathlib: Essential Changes


view this post on Zulip Mohamed Al-Fahim (Jan 07 2021 at 19:01):

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

view this post on Zulip Mohamed Al-Fahim (Jan 07 2021 at 19:05):

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

view this post on Zulip Mohamed Al-Fahim (Jan 07 2021 at 23:37):

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.

view this post on Zulip Mohamed Al-Fahim (Jan 07 2021 at 23:54):

> 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

view this post on Zulip Mohamed Al-Fahim (Jan 07 2021 at 23:55):

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

view this post on Zulip Mohamed Al-Fahim (Jan 08 2021 at 00:06):

Type*

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

view this post on Zulip Mohamed Al-Fahim (Jan 08 2021 at 00:08):

> 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 08 2021 at 00:33):

syntax aware linters will make things so much better

view this post on Zulip Bryan Gin-ge Chen (Jan 08 2021 at 00:36):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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