submit or share nng solutions

Stream: Lean for teaching

[Thanos Tsouanas]

I'm teaching a course on reading/writing math proofs and definitions and I'm using Lean as some kind of TA (first time).
(The objective of the course is to learn how to write proper human-text proofs; Lean is just a tool I think will help a lot towards this goal.)
I have asked my students to play NNG to familiarize themselves with Lean and the whole idea.
Is there an easy way to extract ones solutions to some kind of file(s) form to submit them?
Or a way to share a link with your current "state"? (They're using the online, browser-based version.)

[Thanos Tsouanas]

One challenge is that the class has a very mixed level of computer skills: the more techy students have already installed Lean, shared git repos, and are now working on further exercises; on the opposite side of the spectrum some have copy-pasted their partial solutions into MS Word documents and sent me .docx files...

[Kevin Buzzard]

Golly, I don't know. I'll ping @Mohammad Pedramfar but I am pretty sure that functionality isn't there. One day we might want to make a Lean 4 version of all this, and this would be a nice addition. I'm not sure people are going to be too keen to get all this working in Lean 3. It might be easiest in practice to cut and paste solutions into MS Word documents right now...

[Thanos Tsouanas]

Ah, I see, I can at least hope to get them to use plain text .lean files, ehehe..

[Thanos Tsouanas]

I imagine the core of the functionality is there, since something does get saved.. somewhere. The thing is where exactly and how to extract it for sharing.

[Thanos Tsouanas]

Ah, greping around I found the my whole NNG "state" is on firefox's webappsstore.sqlite db file. That's something! :nerd:

[Thanos Tsouanas]

Ok, and I see from firefox's browser tools that I can navigate to the savedGameData fairly easily:
Storage tab > Local storage > (NNG url)
There's a key-val pair that I imagine replacing its value would have the effect of "loading" somebody else's saved game.

[Thanos Tsouanas]

Update: I tried editing this value (I just altered a -- testing comment of one of the solutions to -- toasting) and the game's toasted now (white page, nothing shown) so... warning to anybody else who might think this would work.

[Thanos Tsouanas]

2nd update: actually editing this value does work: I go to the "main" page, edit it, save it, reload the page, and it works. I must have messed something on my first attempt, and it ended up leaving the site broken.

[Mohammad Pedramfar]

The functionality to share the game state isn't there, but the game saves its state where you said, in Storage tab > Local storage > (NNG url).

[Mohammad Pedramfar]

If you want to save and load the game, right now, you can add these bookmarks and then click on them from the game :)

save:

javascript:(function save(data, filename) {     if(!window.location.href.endsWith("natural_number_game/")){         alert("To load saved game, go to the main page first!");       return;     };     var file = new Blob([data]);     var a = document.createElement("a"),             url = URL.createObjectURL(file);     a.href = url;     a.download = filename;     document.body.appendChild(a);     a.click();     setTimeout(function() {         document.body.removeChild(a);         window.URL.revokeObjectURL(url);       }, 0);  })(window.localStorage.getItem("Natural number game-1-savedGameData"), "Natural number game saved data.txt");

load:

javascript:(function(){     return new Promise((resolve) => {       if(!window.location.href.endsWith("natural_number_game/")){           alert("To load saved game, go to the main page first!");           resolve("");         }else{   const uploader = document.createElement('input');             uploader.type = 'file';             uploader.style.position = 'relative';             uploader.addEventListener('change', () => {                 const files = uploader.files;                 if (files.length) {                     const reader = new FileReader();                     reader.addEventListener('load', () => {                         uploader.parentNode.removeChild(uploader);                         resolve(reader.result);                     });                     reader.readAsText(files[0]);                 };             });             document.body.appendChild(uploader);           document.getElementById("root").style.display = 'none';         };     }); })().then(text => {     console.log(text);   if(text){   window.localStorage.setItem("Natural number game-1-savedGameData", text);   window.location.reload();     }; });

[Mohammad Pedramfar]

The codes that I've wrote should be the url of the bookmark. When you click on those bookmarks, the browser runs the code and saves/loads the game.

[Thanos Tsouanas]

Thanks @Mohammad Pedramfar! I had no idea that I can have bookmarks with URL's with javascript:, that's quite useful! Now the challenge is to get my students to use these.

[Mohammad Pedramfar]

You're welcome :)
It is useful. It's called a bookmarklet. If you google it, you'll find all kinds of useful little functions you can have with them.

[Mohammad Pedramfar]

I'll add the save and load buttons in the next commit to the Lean-game-maker.

[Mohammad Pedramfar]

Now that the topic of bookmarklets have come up, let me mention something I found a few days ago.
Firefox doesn't allow any extensions to do anything to pdf files, because reasons!!
So if you're used to the dark mode, and you want to use the pdf reader inside firefox, you're out of luck since extensions like Dark Reader won't be able to help.
However, this bookmarklet let's you see pdfs in dark mode :D

javascript:(function(){viewer.style = 'filter: grayscale(1) invert(1) sepia(1) contrast(75%)';})()

[Thanos Tsouanas]

Thanks again for mentioning the whole bookmarklets thing! :nerd:

[Marc Masdeu]

I think that the "game maker" of @Mohammad Pedramfar is great to introduce Lean to novices, and that it has still lots of potential. A bunch of us in Barcelona are developing a topology game, and we found it useful to have "hinted proofs". I added this feature to my fork (see https://github.com/mmasdeu/lean-game-maker). The idea is that you can write part of the solution so that the player only fills in a sorry or two in it. Maybe you want o show the structure of the proof, or do one case as illustration and let the player do the other...

Another feature which I don't know how to do would be to have levels with two (or more) lemmas such that solving one of them gives you the check. That would be useful to ask questions like "Which of the two statements is true? Prove it."

Cheers!

[Kevin Buzzard]

Hiya Marc. I absolutely agree with you that the game maker idea has got a lot of potential. I have written several "not-the-game-maker-but-still-perfectly-playable" things such as the complex number game but nothing gets anywhere near as much attention as the natural number game, simply because installing Lean 3 is still a huge PITA for most people. One thing I didn't like about NNG was that every lemma needed its own page, after a while I didn't have anything in particular to say about some levels -- "you know all the tactics, we need these results for later, just prove the below". It would be good if we could have multiple things happening on one page and flexibility for what needs to be done (e.g. "prove both of these" or "prove precisely one of these" etc)

[Filippo A. E. Nuccio]

What kind of topology will we be able to play with, there? I will (try to) teach some students what Lean is by playing around with $\pi_1$ and I am very much interested.

[Mohammad Pedramfar]

Hi Marc! That's great. If the changes are complete and they're working, please make a pull request and I'll be happy to merge it.

As for having several lemmas in one page, I'm not completely sure what the easiest approach would be. If the code is unclear anywhere or you'd like to discuss the best way to implement such a feature, I would be happy to help.

[Marc Masdeu]

Filippo, you can take a look at github.com/mmasdeu/topologygame (it'll be basic point set topology, targeted at students first encountering it). You are welcome to suggest new levels!

[Filippo A. E. Nuccio]

Thanks! I will certainly have a look.

[Kevin Buzzard]

We should make a collection of these games

[Kevin Buzzard]

They deserve more publicity