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

66 Open 140 Closed
66 Open 140 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
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

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 priority-low nice to have
#235 opened Jun 1, 2024 by JadAbouHawili
5
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
Support writing math symbols using ; in addition to \ client Functionality of the client side code enhancement New feature or request priority-low nice to have
#225 opened May 5, 2024 by JadAbouHawili
1
Question: Can you have calc blocks in games? 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
#223 opened May 2, 2024 by lnay
5
Bug: Lost progress bug Something isn't working client Functionality of the client side code priority-high address ASAP
#221 opened Apr 24, 2024 by joneugster
feat: user feedback ideal for volunteers Feature request which should make for a good isolated project. Currently out-of-scope/unclaimed
#218 opened Apr 17, 2024 by joneugster
feat: add bonus levels 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
#217 opened Apr 17, 2024 by joneugster
local notation in inventory bug Something isn't working
#216 opened Apr 17, 2024 by joneugster
forbidden keywords bug Something isn't working priority-low nice to have server Concerning the lean gameserver
#215 opened Apr 16, 2024 by joneugster
1
proof statement with itself bug Something isn't working
#213 opened Apr 16, 2024 by joneugster
lake exe i18n --export-json does not support #~
#210 opened Apr 11, 2024 by JiechengZhao
2
(some?) error messages appear twice
#209 opened Apr 10, 2024 by TentativeConvert
The layout jumps for a split second every time a tooltip is displayed bug Something isn't working client Functionality of the client side code priority-low nice to have
#207 opened Mar 28, 2024 by noamraph
3
repeat causes server crash bug Something isn't working priority-medium should be addressed within the next months
#201 opened Mar 7, 2024 by krtab
2
Feature request: Allow options for deleting information client Functionality of the client side code enhancement New feature or request priority-low nice to have
#199 opened Mar 2, 2024 by djvelleman
1
bug: disable not imported theorems bug Something isn't working client Functionality of the client side code priority-low nice to have server Concerning the lean gameserver
#196 opened Feb 26, 2024 by joneugster
Dev Container npm/node issues bug Something isn't working priority-high address ASAP
#195 opened Feb 21, 2024 by Trequetrum
2
Unlock things on "relaxed" rules client Functionality of the client side code enhancement New feature or request priority-low nice to have
#194 opened Feb 20, 2024 by joneugster
Editor mode broken on mobile bug Something isn't working client Functionality of the client side code priority-medium should be addressed within the next months
#193 opened Feb 7, 2024 by joneugster
Weird font in infoview client Functionality of the client side code enhancement New feature or request priority-low nice to have
#192 opened Jan 31, 2024 by abentkamp
2
"unknown identifier" error message enhancement New feature or request priority-low nice to have
#187 opened Jan 23, 2024 by joneugster
ProTip! Updated in the last three days: updated:>2024-06-03.