crash lean with `revert`

Stream: general

[Kevin Buzzard]

Lean crashes are rare, for me at least. But I think this one seems to be reproducible (for me at least):

theorem i_crash_lean_342 (K : Type*) (S : K → Prop) : false :=
begin
  revert K S S,
  sorry
end

I don't know how to check whether this still happens in Lean 3.5.0c.

[Bryan Gin-ge Chen]

I believe this is fixed in 3.5.0c: https://github.com/leanprover-community/lean/issues/53

[Kevin Buzzard]

Oh nice -- sorry to waste your time. Can I use 3.5.0c yet by changing my leanpkg.toml? If not, am I right in thinking that it will not be too long before this will be possible?

[Bryan Gin-ge Chen]

Yes, I think you can follow the instructions Simon posted here. Hopefully in a few weeks, update-mathlib will be able to fetch 3.5.0c olean files as well.

[Rob Lewis]

Moving mathlib to 3.5c is on my to-do list for this week. Or more accurately, checking that there will be no complications is on my to-do list, and if there's nothing too bad then the move is too.

[Rob Lewis]

Getting the nightly builds working with GitHub Actions needs to happen first.

[Rob Lewis]

And we should know if Gabriel solved that in 40 minutes or so.

[Kevin Buzzard]

I am in no hurry Rob. Many thanks for dealing with all these infrastructure issues. I only asked because I remember people talking about it in Pittsburgh. I wouldn't normally care about this sort of thing but because of the segfault I noticed that if I knew how to use 3.5.0c I would have been able to try it myself without bothering people here.