Skip to content

Issues: leanprover-community/lean4game

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

75 Open 154 Closed
75 Open 154 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

There is no responsive answer from the game after executing command bug Something isn't working
#273 opened Nov 9, 2024 by yourcomrade
2
Suggestion: Dependencies throw an error if there is a missing world.
#272 opened Oct 27, 2024 by Louw123
NNG talks about Hypotheses, UI has Assumptions
#271 opened Oct 27, 2024 by jackie-scholl
1
Don't show locked items in inventory.
#265 opened Oct 10, 2024 by miguelmarco
1
have a hypothesis that has multiple premises
#264 opened Oct 5, 2024 by Qinggao1729
1
Building issue
#263 opened Oct 5, 2024 by kant2002
3
fix filtering of "unsolved goal" error bug Something isn't working
#257 opened Aug 18, 2024 by joneugster
Failed to Configure mathlib Dependency for GlimpseOfLean in lean4game bug Something isn't working priority-high address ASAP
#256 opened Aug 17, 2024 by RexWzh
1
Delete tmp games client Functionality of the client side code enhancement New feature or request priority-medium should be addressed within the next months
#255 opened Aug 13, 2024 by joneugster
1
Struggling to run games locally manually
#254 opened Jul 28, 2024 by ndcroos
4
Does this game have hints for new beginner ?
#252 opened Jul 19, 2024 by geraltgod
4
Website Translation from German to English fails on Robo wontfix This will not be worked on
#247 opened Jul 3, 2024 by AMindToThink
2
feat: inventory of cheat sheets/summaries in addition to tactics, definitions and theorems enhancement New feature or request wontfix This will not be worked on
#246 opened Jul 1, 2024 by TentativeConvert
1
feat: navigation buttons "previous lemma", "next lemma" in inventory enhancement New feature or request
#245 opened Jul 1, 2024 by TentativeConvert
Update to Lean v4.8 priority-high address ASAP server Concerning the lean gameserver
#243 opened Jun 21, 2024 by MithicSpirit
2
Competition
#242 opened Jun 19, 2024 by swisstackle
3
Always show solutions after level completion enhancement New feature or request priority-medium should be addressed within the next months
#240 opened Jun 17, 2024 by matthiasgeihs
1
"solution" button/indicator light for next intended next step client Functionality of the client side code enhancement New feature or request priority-low nice to have server Concerning the lean gameserver
#239 opened Jun 14, 2024 by joneugster
1
TheoremDoc: Usage of [[mathlib_doc]] not documented
#238 opened Jun 13, 2024 by JadAbouHawili
2
feat: allow for custom translations client Functionality of the client side code enhancement New feature or request fixed on dev Will be part of the next update priority-low nice to have
#237 opened Jun 5, 2024 by joneugster
2
Adding Image to the left side pane of a world client Functionality of the client side code enhancement New feature or request fixed on dev Will be part of the next update priority-low nice to have
#235 opened Jun 1, 2024 by JadAbouHawili
10
Player proceeds after error bug Something isn't working priority-medium should be addressed within the next months
#233 opened May 27, 2024 by joneugster
Level Introduction Auto-Scrolling bug Something isn't working client Functionality of the client side code fixed on dev Will be part of the next update priority-medium should be addressed within the next months
#230 opened May 14, 2024 by Trequetrum
Gray mouse-over documentation boxes problematic on small screens bug Something isn't working client Functionality of the client side code priority-medium should be addressed within the next months
#228 opened May 10, 2024 by TentativeConvert
Ask question on Zulip client Functionality of the client side code enhancement New feature or request ideal for volunteers Feature request which should make for a good isolated project. Currently out-of-scope/unclaimed priority-low nice to have
#227 opened May 8, 2024 by joneugster
@ndcroos
2
ProTip! Exclude everything labeled bug with -label:bug.