Update to Lean v4.8

[MithicSpirit]

It would be nice to update this to lean v4.8.0, as induction_eliminator and cases_eliminator may be helpful for games. I've been working on trying to do this, but got stuck on handling diagnostics (I'm particularly interested in using those in the Lean4 rewrite of the linalg game). It seems that v4.8 has reworked how snapshots work, removing Snapshots.Snapshot.interactiveDiags (leanprover/lean4#3014). I also faced some issues with some usage of String being replaced with Lean.Name, but that wasn't difficult to fix. There may be other problems I haven't gotten to yet, since compilation fails at the diagnostics issue.

[joneugster]

Indeed, the rewriting of snapshots was one reason I put this off so far, as it implied bigger refactors in the FileWorker file. I was hoping to get there in the next two weeks or so.

In particular I've been wondering if the new way how proofs are compiled create a better option how to retrieve all intermediate goals.

[joneugster]

If you have steps to contribute, make sure you are working on the bump_v4.8.0 branch