load levels via uri

client/src/App.tsx

@@ -32,7 +32,7 @@ function App() {
   const [leanClient, setLeanClient] = useState<null|LeanClient>(null)
 
   useEffect(() => {
-    const uri = monaco.Uri.parse('file:///LeanProject/Level1.lean')
+    const uri = monaco.Uri.parse('file:///')
     const leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
     setLeanClient(leanClient)
   }, [])

client/src/components/Level.tsx

@@ -5,6 +5,7 @@ import '@fontsource/roboto/400.css';
 import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
 
+import { Button } from '@mui/material';
 import Grid from '@mui/material/Unstable_Grid2';
 
 import LeftPanel from './LeftPanel';
@@ -15,6 +16,7 @@ import { LeanClient } from 'lean4web/client/src/editor/leanclient';
 import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
 import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
 import { InfoProvider } from 'lean4web/client/src/editor/infoview';
+import 'lean4web/client/src/editor/infoview.css'
 import { renderInfoview } from '@leanprover/infoview'
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 
@@ -31,6 +33,9 @@ function Level({ leanClient, nbLevels, level, setCurLevel, setLevelTitle, setFin
   const [index, setIndex] = useState(level) // Level number
   const [tacticDocs, setTacticDocs] = useState([])
   const [lemmaDocs, setLemmaDocs] = useState([])
+  const [editor, setEditor] = useState(null)
+  const [infoProvider, setInfoProvider] = useState(null)
+  const [infoviewApi, setInfoviewApi] = useState(null)
 
   const [leanData, setLeanData] = useState({goals: []})
   const [history, setHistory] = useState([])
@@ -57,12 +62,8 @@ function Level({ leanClient, nbLevels, level, setCurLevel, setLevelTitle, setFin
     // }
   }
 
-  // The next function will be called when the level changes
   useEffect(() => {
-    const uri = monaco.Uri.parse('file:///LeanProject/Level1.lean')
-    const model = monaco.editor.createModel('', 'lean4', uri)
     const editor = monaco.editor.create(codeviewRef.current!, {
-      model,
       glyphMargin: true,
       lightbulb: {
         enabled: true
@@ -78,25 +79,42 @@ function Level({ leanClient, nbLevels, level, setCurLevel, setLevelTitle, setFin
       'semanticHighlighting.enabled': true,
       theme: 'vs-code-theme-converted'
     })
-    // setEditor(editor)
-    new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
 
     const infoProvider = new InfoProvider(leanClient)
     const div: HTMLElement = infoviewRef.current!
     const infoviewApi = renderInfoview(infoProvider.getApi(), div)
-    infoviewApi.serverRestarted(leanClient.initializeResult)
+
-    infoProvider.openPreview(editor, infoviewApi)
+    setEditor(editor)
-    // setInfoProvider(infoProvider)
+    setInfoProvider(infoProvider)
-    // setInfoviewApi(infoviewApi)
+    setInfoviewApi(infoviewApi)
-
+  }, [])
-    leanClient.sendRequest("loadLevel", {number: level}).then((res) => {
+
-      setLevelTitle("Level " + res["index"] + ": " + res["title"])
+  // The next function will be called when the level changes
-      setIndex(parseInt(res["index"]))
+  useEffect(() => {
-      setTacticDocs(res["tactics"])
+    if (editor) {
-      setLemmaDocs(res["lemmas"])
+      const uri = monaco.Uri.parse(`file:///level${level}`)
-      processResponse(res)
+      const model = monaco.editor.createModel('', 'lean4', uri)
-    });
+
-  }, [level, leanClient])
+      editor.setModel(model)
+      infoviewApi.serverRestarted(leanClient.initializeResult)
+      infoProvider.openPreview(editor, infoviewApi)
+
+      new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
+
+      // setInfoProvider(infoProvider)
+      // setInfoviewApi(infoviewApi)
+
+      leanClient.sendRequest("loadLevel", {number: level}).then((res) => {
+        setLevelTitle("Level " + res["index"] + ": " + res["title"])
+        setIndex(parseInt(res["index"]))
+        setTacticDocs(res["tactics"])
+        setLemmaDocs(res["lemmas"])
+        processResponse(res)
+      });
+
+      return () => { model.dispose(); }
+    }
+  }, [editor, level, leanClient])
 
   function sendTactic(input) {
     leanClient.sendRequest("runTactic", {tactic: input}).then(processResponse);
@@ -145,7 +163,8 @@ function Level({ leanClient, nbLevels, level, setCurLevel, setLevelTitle, setFin
       </Grid>
       <Grid xs={4}>
         <div ref={infoviewRef} className="infoview"></div>
-        <TacticState goals={leanData.goals} errors={errors} lastTactic={lastTactic} completed={completed} />
+        <Button onClick={loadNextLevel} sx={{ ml: 3, mt: 2, mb: 2 }} disableFocusRipple>Go to Next Level</Button>
+        {/* <TacticState goals={leanData.goals} errors={errors} lastTactic={lastTactic} completed={completed} /> */}
       </Grid>
     </Grid>
   )

server/leanserver/GameServer/FileWorker.lean

@@ -55,6 +55,14 @@ open JsonRpc
 
 section Elab
 
+-- TODO: Find a better way to pass on the file name?
+def levelIdFromFileName (fileName : String) : IO Nat := do
+  if fileName.startsWith "/level" then
+    if let some id := (fileName.drop "/level".length).toNat? then
+      return id
+  throwServerError s!"Could not find level ID in file name: {fileName}"
+  return 1
+
 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool) (couldBeEndSnap : Bool) : IO Snapshot := do
   let cmdState := snap.cmdState
@@ -85,15 +93,15 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
       fileMap      := inputCtx.fileMap
       tacticCache? := some tacticCacheNew
     }
-    IO.FS.writeFile "test.txt" s!"{tacticStx}"
     let (output, _) ← IO.FS.withIsolatedStreams (isolateStderr := server.stderrAsMessages.get scope.opts) <| liftM (m := BaseIO) do
       Elab.Command.catchExceptions
         (getResetInfoTrees *> do
           let levels := levelsExt.getState (← getEnv)
+          let levelId ← levelIdFromFileName inputCtx.fileName
           let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[]
           let tacticStx := (tacticStx.getArgs.push done).map (⟨.⟩)
           let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
-          let cmdStx ← `(command| theorem mythm $(levels[1].get!.goal) := by {$(⟨tacticStx⟩)} )
+          let cmdStx ← `(command| theorem mythm $(levels[levelId].get!.goal) := by {$(⟨tacticStx⟩)} )
           Elab.Command.elabCommandTopLevel cmdStx)
         cmdCtx cmdStateRef
     let postNew := (← tacticCacheNew.get).post

server/leanserver/GameServer/Game.lean

@@ -30,6 +30,10 @@ structure LevelInfo where
   lemmas: Array LemmaDocEntry
 deriving ToJson
 
+structure LoadLevelParams where
+  number : Nat
+  deriving ToJson, FromJson
+
 partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
   match ev with
   | ServerEvent.clientMsg msg =>
@@ -41,8 +45,9 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
       let game := {← gameExt.get with nb_levels := levels.size }
       c.hOut.writeLspResponse ⟨id, game⟩
       return true
-    | Message.request id "loadLevel" _ =>
+    | Message.request id "loadLevel" params =>
-      let idx := 1
+      let p ← parseParams LoadLevelParams (toJson params)
+      let idx := p.number
       let s ← get
       let c ← read
       let levels := levelsExt.getState s.env