Work on adding user feedback by opening a github issue from game

[ndcroos]

See https://github.com/leanprover-community/lean4game/issues/218

This is work in progress. So far, I have an extra dropdown option, which opens a popup with a button, which opens a GitHub issue with title and body prefilled. This 'UX workflow' probably needs to change a little bit, for example adding more context to the button, i.e. that this will create a GitHub issue)/ For now, I got as far as without playing a game to get the specific data of the level and the proof. I am not sure in which directory I should place the local game I use for testing purposes. I placed the NNG4 repo dir in the directory of the lean4game So output from ls looks something like this:

lean4game (dev)
$ ls
LICENSE             client/               index.html         relay/
NNG4/     ...

This 'works', but I actually could not play the game locally, as it could not find the game. Also; for pushing changes, I need to remove the NNG4 directory. In .gitignore, there is a pattern for games/, so maybe the game should be added under this directory, but I am not sure how (I tried different options related to http://localhost:3000/#/g/local/FOLDER, but they did not work for me).

[joneugster]

Thank you very much for your effort, and sorry for the late response due to vacation, I will have time to look at PRs early next week!

As for running the game locally:

some_common_folder/
|-- lean4game/
|-- NNG4/

would be the right structure to use localhost:3000/#/g/local/NNG4

or alternatively

some_common_folder/
|-- lean4game/
    |-- games/
        |-- leanprover-community/
            |-- nng4/

for localhost:3000/#/g/leanprover-community/nng4. (That's what happens if a game is imported ising the import mechanism).

[ndcroos]

Thanks for getting back to me and for explaining the needed folder structure.

At the moment, I kind of assumed in this draft that the user already has a GitHub account. I'm thinking of what happens when a user tries to create an issue when the user is not logged in GitHub.

[joneugster]

Thank you for the PR, I think this already looks quite good the way it is!

If you want I'd be happy to merge this as is and then have optional improvements follow later.

[joneugster]

At the moment, I kind of assumed in this draft that the user already has a GitHub account. I'm thinking of what happens when a user tries to create an issue when the user is not logged in GitHub.

I think that's a fair assumption to make. Ideally it would ask you first to login, and then redirect to the issue page. I'd hope github does this automatically?

[ndcroos]

Thanks for getting back to me. I'm fine with merging this already, although I haven't been able to test this fully. I also haven't been able to test the github login and redirect.