Lean 4 survival guide for Lean 3 users

Stream: mathlib4

[Floris van Doorn]

I added a page to the Mathlib 4 wiki with a Lean 4 survival guide for Lean 3 users. It is part of the mathlib repo, since I want to document changes that are only relevant for mathlib users.

Please contribute if you notice anything that is missing!

[Sam van G]

Wrote a little note about Cache on the page because I was pretty confused about this myself a few weeks ago. This was just written in two minutes based on my own naive understanding, so can probably be improved!

[Sebastian Ullrich]

I don't think get! should be necessary ever since !4#2751. Does anyone have a disagreeing experience?

[Damiano Testa]

I think that the parents of a structure should be separated by commas, even when they are on different lines and (or maybe because) they do not seem to be affected by whitespace.

[Damiano Testa]

If this is correct, I can update the wiki page!

[Mario Carneiro]

Function notation changed from λ x, f x to fun x => f x or λ x => f x. If you import (almost) any file from mathlib, you can also use fun x ↦ f x or λ x ↦ f x.

This notation is implemented in core, you don't need to import anything from mathlib

[Mario Carneiro]

Damiano Testa said:

I think that the parents of a structure should be separated by commas, even when they are on different lines and (or maybe because) they do not seem to be affected by whitespace.

yes this is correct (I thought you meant the extends list but I guess you mean { <here> with ... })

[Damiano Testa]

Mario, thank you for the confirmation! Also, I always have a really hard time to use this notation and your comment about extends may be something that I had not considered.

[Damiano Testa]

I will add the minimal change of placing a comma between parent1 and parent2 in the wiki and if someone else who actually knows what they are doing wants to explain this better, I will likely learn something! :smile:

[Damiano Testa]

{ parent1,    -- <-- added this comma here
  parent2 with
  field1 := value1
  field2 := value2 }

[Sam van G]

Sebastian Ullrich said:

I don't think get! should be necessary ever since !4#2751. Does anyone have a disagreeing experience?

I remember being in trouble with my cache once after March 10th and being told to use get! but don't know how to reproduce the exact situation.

[Scott Morrison]

I think ctrl-c during download can still potentially leave a broken file in place?

[Yury G. Kudryashov]

Is there a curl option to use a .part file?

[Yury G. Kudryashov]

(like browsers do)

[Yury G. Kudryashov]

Probably, not, but we can do it manually: download with curl to file.part, then move to file.

[Scott Morrison]

Yes, this was discussed at !4#2751 but not implemented. Apparently this is not a lean-native function for moving a file. :-)