search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
136 stars 25 forks source link

Update to Lean v4.8 #243

Open MithicSpirit opened 1 week ago

MithicSpirit commented 1 week ago

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 commented 1 week ago

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 commented 1 week ago

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