search

leanprover-community / lean4game

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

Failed to Configure mathlib Dependency for GlimpseOfLean in lean4game #256

Open RexWzh opened 3 months ago

RexWzh commented 3 months ago

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 commented 3 months ago

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.)