Playing the game in VsCode

Question

Playing the game in VsCode

Closed this issue a year ago · 1 comments

Hi,
I would like to compliment the game website for its impressive features, such as hinting and uploading. It provides a great user experience. However, I'm curious if there is a way to play the game in VsCode directly. For instance, having a dedicated branch or folder for exercises without proofs.

As an alternative approach, the proof could be removed using the following code:

import re
pattern = "(Statement[\s\S]*:= by)[\s\S]*\nConclusion"
print(re.sub(pattern, r"\1\n  sorry\nConclusion", txt, re.S))

Sorry, it seems unnecessary to play it in VsCode actually.

Answer 1 · 2023-09-07T20:53:05.000Z

One thing that works is that you open the github repo in VSCode in a DevContainer, you can play it at http://localhost:3000
That's more designed for modifying levels I guess.

It would not be hard to have a deployment script that removes the proofs: "Mathematics In Lean" does this for example. However, it would be hard to do this in a way for the NNG such that the hints you get at a certain proofstep are still available in a meaningful way.