search

leanprover-community / lean4game

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

feat: user feedback #218

Open joneugster opened 7 months ago

joneugster commented 7 months ago

Add functionality to get some user feedback:

ndcroos commented 4 months ago

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?

joneugster commented 4 months ago

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

joneugster commented 4 months ago

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

ndcroos commented 4 months ago

Thanks for the help. How can I see feedback on changes that I make on lean4game? What instructions should I follow to 'run' lean4game?

joneugster commented 4 months ago

https://github.com/leanprover-community/lean4game/blob/main/doc/DOCUMENTATION.md#modifying-the-server

I believe this is the relevant part of the manual