Failed to Configure mathlib Dependency for GlimpseOfLean in lean4game

[RexWzh]

Hi,

I'm currently working on deploying GlimpseOfLean as a Lean game and encountering difficulties with configuring the mathlib dependency within lean4game.

You can review the project's progress at this link: GlimpseToGame Project. Despite several attempts, I've yet to succeed.

First Attempt:

I tried setting the dependency in lakefile.lean like this:

require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ leanVersion

This resulted in a build error due to GlimpseOfLean needing mathlib version 4.8.0, not 4.7.0 that was obtained:

❯ lake update
# Warnings about missing dependency manifest
❯ lake build 
error: 'Game.Library.Basic' relies on 'Mathlib.RingTheory.Ideal.Maps': no such file or directory (error code: 2)

Second Attempt:

I set the leanprover/lean4:v4.8.0 in lean-toolchain, which led to an error because the repository for GameServer couldn't find the specified revision:

❯ lake update
error: cannot find revision v4.8.0 in repository ././.lake/packages/GameServer

The latest version for lean4game is v4.7.0, which conflicts with the required version.

Other Attempts:

I specified the mathlib version directly in leanfile.lean:

require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.8.0"

This modification caused a new kind of error upon updating:

❯ lake update
# Updating mathlib to a specific revision
error: unknown attribute [test_runner] and package configuration errors in lakefile.lean

Even after using the branch or commit hash, I encountered issues, possibly due to a mismatch with the toolchain version. Attempts to downgrade GlimpseOfLean's version also resulted in errors.

---

I'm in need of assistance to resolve these issues with the mathlib dependency. Any help or guidance would be greatly appreciated.

Thanks in advance!

[joneugster]

We'll eventually update past v4.7.0, just didn't get around it yet due to problems with the vscode-lean4 extension running in a browser.

I think your realistic options are to either downgrade GlimpseOfLean temporarily to v4.7.0 or wait until I figured out how to run the game engine in v4.8.0+ (which has to happen soon! Once it's on v4.8.0 it will simultaneously also work for all stable releases since then.)