From 8fd6b3e015065745c4c139e7cf1c52bff6d9af88 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Fri, 25 Nov 2022 09:53:21 +0100 Subject: [PATCH] load levels via uri --- client/src/App.tsx | 2 +- client/src/components/Level.tsx | 59 +++++++++++++------- server/leanserver/GameServer/FileWorker.lean | 12 +++- server/leanserver/GameServer/Game.lean | 9 ++- 4 files changed, 57 insertions(+), 25 deletions(-) diff --git a/client/src/App.tsx b/client/src/App.tsx index 43ffbfc..17146b8 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -32,7 +32,7 @@ function App() { const [leanClient, setLeanClient] = useState(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) }, []) diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index 51a652e..3d68b8f 100644 --- a/client/src/components/Level.tsx +++ b/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) - // 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) - }); - }, [level, leanClient]) + + setEditor(editor) + setInfoProvider(infoProvider) + setInfoviewApi(infoviewApi) + }, []) + + // The next function will be called when the level changes + useEffect(() => { + if (editor) { + const uri = monaco.Uri.parse(`file:///level${level}`) + const model = monaco.editor.createModel('', 'lean4', uri) + + 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
- + + {/* */} ) diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean index a6325ee..5e36276 100644 --- a/server/leanserver/GameServer/FileWorker.lean +++ b/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 diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean index bb6d832..1a66795 100644 --- a/server/leanserver/GameServer/Game.lean +++ b/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" _ => - let idx := 1 + | Message.request id "loadLevel" params => + let p ← parseParams LoadLevelParams (toJson params) + let idx := p.number let s ← get let c ← read let levels := levelsExt.getState s.env