error: 'src' is not a field of structure 'Dependency'

Stream: new members

[Lucian]

Hello. I am very very new to LEAN and am trying to develop something for the first time. Specifically, I am trying to create a game using the lean4game template found here: https://github.com/leanprover-community/lean4game/blob/main/doc/create_game.md. I cloned the repo and am running into this error when running lake update

[lucian@void leantest](main ?)$ lake update
error: ././lakefile.lean:9:2: error: 'src' is not a field of structure 'Dependency'
error: ././lakefile.lean:14:2: error: 'src' is not a field of structure 'Dependency'
error: ././lakefile.lean: package configuration has errors

I would appreciate any help. Thanks!

[Lucian]

I found this stating that my lakefile.lean might be out of date but I doubt this repo isn't maintained to this level. https://leanprover-community.github.io/archive/stream/270676-lean4/topic/lakefile.20dependencies.html

[Julian Berman]

(Welcome!) What instructions did you follow to install elan (and thereby lean)? And/or what is lake --version showing you?

[Lucian]

I have this for my lake version,

[lucian@void GameSkeleton](main ?)$ lake --version
Lake version 5.0.0-d553333 (Lean version 4.14.0)

I did not install elan and thus built from the source here: https://aur.archlinux.org/packages/lean. I don't see why installing from elan would change things but if you recommend I will try it out.

[Julian Berman]

Yes, that is precisely your issue, you're using the wrong version of Lean for your project, which is the problem elan solves. You should follow the install instructions at https://lean-lang.org/lean4/doc/quickstart.html (or https://leanprover-community.github.io/get_started.html) and uninstall what you built.

[Lucian]

It worked. Thanks for the help! <3

[Julian Berman]

Great! Make something nice :) we need more fun games.