Zulip Chat Archive

Stream: Lean for teaching

Topic: submit or share nng solutions

Thanos Tsouanas (Dec 04 2021 at 01:39):

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 (Dec 04 2021 at 01:40):

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 (Dec 04 2021 at 11:30):

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 (Dec 04 2021 at 15:28):

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

Thanos Tsouanas (Dec 04 2021 at 15:32):

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 (Dec 04 2021 at 15:34):

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

Thanos Tsouanas (Dec 04 2021 at 15:41):

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 (Dec 04 2021 at 17:51):

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 (Dec 05 2021 at 15:03):

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 (Dec 05 2021 at 16:31):

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 (Dec 05 2021 at 16:34):

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


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");


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 (Dec 05 2021 at 16:36):

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 (Dec 05 2021 at 17:17):

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 (Dec 05 2021 at 18:18):

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 (Dec 05 2021 at 18:20):

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

Mohammad Pedramfar (Dec 05 2021 at 18:37):

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 (Dec 05 2021 at 19:38):

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

Marc Masdeu (Dec 06 2021 at 16:52):

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


Kevin Buzzard (Dec 06 2021 at 18:23):

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 (Dec 06 2021 at 23:28):

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 π1\pi_1 and I am very much interested.

Mohammad Pedramfar (Dec 07 2021 at 00:20):

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 (Dec 07 2021 at 18:00):

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 (Dec 07 2021 at 18:01):

Thanks! I will certainly have a look.

Kevin Buzzard (Dec 07 2021 at 18:01):

We should make a collection of these games

Kevin Buzzard (Dec 07 2021 at 18:01):

They deserve more publicity

Last updated: Dec 20 2023 at 11:08 UTC