Typo in "success_if_fail" in lean reference manual

Stream: new members

[Sara Fish]

The description says "Succeeds if the given tactic succeeds." rather than what I assume should be "Succeeds if the given tactic fails."

[Jalex Stark]

which document is this? if it's in a leanprover-community repo then it's easy to submit a PR to fix it. There are some old, unmaintained documents floating around, though.

[Sara Fish]

https://leanprover.github.io/reference/lean_reference.pdf

[Sara Fish]

I saw authors listed so figured PR was out of the question

[Jalex Stark]

Sara Fish said:

I saw authors listed so figured PR was out of the question

files in mathlib have authors :)

[Jalex Stark]

but yeah I don't think this will be updated

[Jalex Stark]

i think everyone with write access to the leanprover repo is trying to release Lean 4 by the end of summer

[Jalex Stark]

fwiw there is an up-to-date tactic doc at tactic#success_if_fail, along with docs generated from the source code in all the tactics

[Sara Fish]

ah, is the key difference here leanprover.github.io versus leanprover-community.github.io ?

[Jalex Stark]

that's right, leanprover-community manages mathlib and the community version of lean

[Jalex Stark]

and mathlibtools and the community website

[Sara Fish]

well it's a shame it's out of date since a big list of tactics is nice for beginners

[Jalex Stark]

hmm is your point that it's more "curated" than the tactic docs? (this page that I linked to earlier)

[Sara Fish]

This reference manual is linked here (https://leanprover-community.github.io/learn.html) fwiw

[Jalex Stark]

hmm then the status of the document is probably something like "it's mostly correct, at least relative to lean 3.4, but isn't being updated with errata"

[Sara Fish]

yeah something like that might've been a good disclaimer so I would have known what to expect

[Sara Fish]

This is of course kind of an edge case since I don't think anyone will be confused about what "success_if_fail" specifically does

[Jalex Stark]

There's a button "Suggest edits to this page on GitHub" at the bottom of https://leanprover-community.github.io/learn.html

[Sara Fish]

Jalex Stark said:

i think everyone with write access to the leanprover repo is trying to release Lean 4 by the end of summer

how different will lean 4 be? I have vaguely heard that backwards compatibility hasn't been an extremely high priority, historically at least

[Jalex Stark]

mathlib will probably end up being ported to lean 4 in such a way that 95%+ of the lines of code don't require human translation

[Jalex Stark]

leo and sebastian gave a talk recently, I'll try to find it

[Patrick Massot]

This estimate is very optimistic, and probably completely wrong, but we'll manage.

[Jalex Stark]

(I think I'm repeating an estimate from leo and sebastian's talk, and indeed, one should expect them to be optimistic)

[Jalex Stark]

lean 4 talk

[Kevin Buzzard]

@Sara Fish the Microsoft lean pages are completely out of date and completely out of our control. Google prefers them to the community pages, but all the lean action right now is happening here and on the community lean pages. Microsoft is talking about lean 3.4.2 from 2018. We're now on 3.17.1 in the community fork

[Scott Morrison]

Porting to Lean 4 is going to be a crazy big job, and it's completely unclear how it will go.

[Scott Morrison]

However, there are some reasons for optimism.

[Scott Morrison]

Gabriel Ebner has already demonstrated that it's possible to import Lean 3 olean files (that is, the compiled output) as imports of Lean 4 files. So a transition period where .lean3 files and .lean files coexist, with some dual compilation scheme, may help us out.

[Scott Morrison]

Lean 4 has a very flexible and configurable parser, so we're going to have a much more capable tool at the destination end of the port, which may be able to hint (e.g. writing code automatic linters, renamers, code fixers, etc).

[Scott Morrison]

There's a lot of enthusiasm in the community for Lean 4, so hopefully there's going to be a lot of willingness to do the work required for the port!

[Scott Morrison]

We are really looking forward to the new features. And the community generally is pretty forward looking --- we all know we're still probably several tool iterations away from interactive theorem proving "really mattering" to research mathematics, so we want to keep moving!