Integrate with the Agdapad

[iblech]

I'll assign myself on this one; this pull request is for discussions and to track progress.

@felixwellen kindly brought TheHoTTGame to my attention. I believe that it is extremely worthwhile, closing an important gap in our quest of making Agda more accessible. Your efforts are very much appreciated!

I'd like to integrate this as soon as possible with the Agdapad. In case you don't know it, this is an online version of Agda running directly in the browser, no installation required, collaborative playing possible.

An easy way of combining these two projects would be to give the Agdapad containers access to git (and the Internet), or perhaps to have TheHoTTGame pre-cloned in each home directory.

A more involved combination would try to resemble the Lean game more closely.

Do you have any ideas on how to best move forward? :-)

[Jlh18]

Hi! Thanks so much for getting in touch. It would be amazing to have an interactive online version since the biggest difficulty with learning agda is installing agda.

I think simply being able to use the game in Agdapad (by having the game precloned in it) would already be amazing. It would be nice if (this proposed version of) Agdapad could have the evil-mode as its default, as that is the format we decide to give instructions in, but this is not super important.

I feel somewhat reluctant to have the game integrated into the website because

1. I would like it to be such that after playing a bunch of the game, people can feel confident using agda themselves. For example the later quests are mostly instructions (and solutions) with no partially made code at all (unlike the natural numbers game), so that they have to write pretty much the whole file. I think having access to whole files rather than just single theorems would be better for this.
2. As you said this would be more involved.

What do you think?

Some thoughts about Agdapad:

• it looks like if I make a session and then come back to it then everything there is saved - is that right? If so that would be perfect, so that people can just come back to their version of the game.
• I can't paste stuff in agdapad, it only has access to the keyring inside Agdapad?
• is there a way to clone a repo into the file system of Agdapad? Is there a way to export work that is done on Agdapad?

[iblech]

Thank you for your feedback! Regarding your questions:

1. Yes, everything is saved.
2. Indeed, the clipboard on the server which is remote-controlled by the browser is distinct from the local clipboard. The clipboard icon in the lower right allows for some exchange. However, this is cumbersome. Hence I just implemented optional auto-synchronization of the two clipboards.
3. The containers don't have Internet access (however I could change this (and use a Tor tunnel) if you'd have some use case for that). However, you can download the Agdapad contents via plain HTTP, and can even mount it as a network volume using WebDAV (see clipboard icon).

In other news, a first version of the integration of TheHoTTGame into the Agdapad is now available. All new sessions come with an already checked out copy of TheHoTTGame, the welcome text refers to TheHoTTGame and the game can be "started" from the Help menu. A cronjob will keep the clone up to date (but only for new sessions, already existing sessions will not have any files changed behind your back). What do you think?

I'm glad that you actually prefer having the integration not too tight (so unlike the Lean game) because that would be much more involved :-)

[Jlh18]

Amazing! I tried it out and it works great. I will add instructions to our website for using Agdapad.

Thanks for getting all of this working - I'm excited for more people to try out our game because of this!