leanprover-community
feat: user feedback
Add functionality to get some user feedback:
- easy option to open an github issue from any level
- have the option of a final playground level in a world, where users can create and submit their own questions related to the current world.
Hello, I'd like to work on this functionality. Can you assign this to me? Also, can you explain the second bullet point a bit more?
For (1) I would probably start with a button in the dropdown menu ("Report problem" or so) and then we can later see if it should be placed more visibly (for example in chat if there is an error on the last command). The report would Ideally have a template with a link to the level and the user's proof pre-inserted.
Point (2) is probably more convoluted and was a preliminary suggestion by somebody. I dont know yet if it's actually a good idea... I think the idea was that you had a level where you could modify the statement (starting with just True for example) and a button where you can "Submit your level" if it compules and the proof is conplete. Probably a username for credit would need to be taken.
One part to keep in mind is that players would somehow need to forfeit their copyright on content they submit (or have it under a good license), so that would need to be displayed somehow.
If you aren't keen on (2) you might just drip that for now, it was just a random idea...
and make sure to work off the dev branch, even though it's still a mess from the heavy refactor I'm in the middle of
Thanks for the help. How can I see feedback on changes that I make on lean4game? What instructions should I follow to 'run' lean4game?
https://github.com/leanprover-community/lean4game/blob/main/doc/DOCUMENTATION.md#modifying-the-server
I believe this is the relevant part of the manual