From 1cd3b7b7ede1be5c866261db02ce98bc37433ee3 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 12 Sep 2024 18:37:39 +0200 Subject: [PATCH 1/2] fix: leanOptions are not used --- cypress/e2e/spec.cy.ts | 11 +++++ demo/server/LeanProject/LeanProject.lean | 1 - .../server/LeanProject/LeanProject/Test0.lean | 2 + .../server/LeanProject/LeanProject/Test1.lean | 2 + demo/server/LeanProject/Main.lean | 4 -- demo/server/LeanProject/lakefile.lean | 16 +++---- demo/server/index.mjs | 47 +++++++++++++++++-- demo/src/LeanMonaco.tsx | 8 +++- 8 files changed, 72 insertions(+), 19 deletions(-) create mode 100644 demo/server/LeanProject/LeanProject/Test0.lean create mode 100644 demo/server/LeanProject/LeanProject/Test1.lean delete mode 100644 demo/server/LeanProject/Main.lean diff --git a/cypress/e2e/spec.cy.ts b/cypress/e2e/spec.cy.ts index 5555689..a9baf84 100644 --- a/cypress/e2e/spec.cy.ts +++ b/cypress/e2e/spec.cy.ts @@ -71,4 +71,15 @@ describe('Editor Test', () => { cy.contains('#check 0').click() cy.iframe().contains('0 : Nat') }) + + it('check leanOptions', () => { + cy.on('uncaught:exception', (err, runnable) => { + // Note: see note about console errors above + return false + }) + cy.visit('http://localhost:5173/') + cy.contains('#print f') + cy.contains('#print f').click() + cy.iframe().contains('def f : Nat → Nat := fun x ↦ x + 1') + }) }) \ No newline at end of file diff --git a/demo/server/LeanProject/LeanProject.lean b/demo/server/LeanProject/LeanProject.lean index e99d3a6..e69de29 100644 --- a/demo/server/LeanProject/LeanProject.lean +++ b/demo/server/LeanProject/LeanProject.lean @@ -1 +0,0 @@ -def hello := "world" \ No newline at end of file diff --git a/demo/server/LeanProject/LeanProject/Test0.lean b/demo/server/LeanProject/LeanProject/Test0.lean new file mode 100644 index 0000000..5bd7296 --- /dev/null +++ b/demo/server/LeanProject/LeanProject/Test0.lean @@ -0,0 +1,2 @@ +-- demonstrates that the 1st and 2nd editor use the `leanOptions` as they specify +-- and existing file, while all further do not as they reference a fictional file. diff --git a/demo/server/LeanProject/LeanProject/Test1.lean b/demo/server/LeanProject/LeanProject/Test1.lean new file mode 100644 index 0000000..5bd7296 --- /dev/null +++ b/demo/server/LeanProject/LeanProject/Test1.lean @@ -0,0 +1,2 @@ +-- demonstrates that the 1st and 2nd editor use the `leanOptions` as they specify +-- and existing file, while all further do not as they reference a fictional file. diff --git a/demo/server/LeanProject/Main.lean b/demo/server/LeanProject/Main.lean deleted file mode 100644 index 9e75120..0000000 --- a/demo/server/LeanProject/Main.lean +++ /dev/null @@ -1,4 +0,0 @@ -import LeanProject - -def main : IO Unit := - IO.println s!"Hello, {hello}!" diff --git a/demo/server/LeanProject/lakefile.lean b/demo/server/LeanProject/lakefile.lean index 5326b30..7fa6663 100644 --- a/demo/server/LeanProject/lakefile.lean +++ b/demo/server/LeanProject/lakefile.lean @@ -1,15 +1,13 @@ import Lake open Lake DSL -package leanProject { +package leanProject where -- add package configuration options here -} - -lean_lib LeanProject { - -- add library configuration options here -} + leanOptions := #[ + ⟨`pp.unicode.fun, true⟩ ] @[default_target] -lean_exe leanProject { - root := `Main -} +lean_lib LeanProject where + -- add library configuration options here + leanOptions := #[ + ⟨`pp.unicode.fun, true⟩ ] diff --git a/demo/server/index.mjs b/demo/server/index.mjs index b876fab..681e40b 100644 --- a/demo/server/index.mjs +++ b/demo/server/index.mjs @@ -18,9 +18,11 @@ const server = app.listen(PORT, () => console.log(`Listening on ${PORT}`)); const wss = new WebSocketServer({ server }) +const leanProjectPath = path.join(__dirname, 'LeanProject') + function startServerProcess() { - const serverProcess = cp.spawn("lake", ["serve", "--"], { cwd: path.join(__dirname, 'LeanProject') }) + const serverProcess = cp.spawn("lean", ["--server"], { cwd: leanProjectPath }) serverProcess.on('error', error => console.error(`Launching Lean Server failed: ${error}`) @@ -35,6 +37,40 @@ function startServerProcess() { return serverProcess } +/** Transform client URI to valid file on the server */ +function urisToFilenames(prefix, obj) { + for (let key in obj) { + if (obj.hasOwnProperty(key)) { + if (key === 'uri') { + obj[key] = obj[key].replace('file://', `file://${prefix}`) + } else if (key === 'rootUri') { + obj[key] = obj[key].replace('file://', `file://${prefix}`) + } else if (key === 'rootPath') { + obj[key] = path.join(prefix, obj[key]) + } + if (typeof obj[key] === 'object' && obj[key] !== null) { + urisToFilenames(prefix, obj[key]); + } + } + } + return obj; +} + +/** Transform server file back into client URI */ +function FilenamesToUri(prefix, obj) { + for (let key in obj) { + if (obj.hasOwnProperty(key)) { + if (key === 'uri') { + obj[key] = obj[key].replace(prefix, '') + } + if (typeof obj[key] === 'object' && obj[key] !== null) { + FilenamesToUri(prefix, obj[key]); + } + } + } + return obj; +} + wss.addListener("connection", function(ws, req) { const ps = startServerProcess() console.log(`[${new Date()}] Socket opened`) @@ -50,8 +86,9 @@ wss.addListener("connection", function(ws, req) { const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close()) const serverConnection = jsonrpcserver.createProcessStreamConnection(ps) socketConnection.forward(serverConnection, message => { - // console.log(`CLIENT: ${JSON.stringify(message)}`) + urisToFilenames(leanProjectPath, message) + console.log(`CLIENT: ${JSON.stringify(message)}`) // Here would be the first place we could determine the server OS // and modify the data sent. // TODO: Maybe it could be an option to search `message` recursively for `uri` fields @@ -60,7 +97,9 @@ wss.addListener("connection", function(ws, req) { return message; }) serverConnection.forward(socketConnection, message => { - // console.log(`SERVER: ${JSON.stringify(message)}`) + FilenamesToUri(leanProjectPath, message) + + console.log(`SERVER: ${JSON.stringify(message)}`) return message; }); @@ -75,7 +114,7 @@ wss.addListener("connection", function(ws, req) { "code": "-1" } } - // console.log(`SERVER: ${JSON.stringify(msg)}`) + console.log(`SERVER: ${JSON.stringify(msg)}`) ws.send(JSON.stringify(msg)) }) diff --git a/demo/src/LeanMonaco.tsx b/demo/src/LeanMonaco.tsx index ce348c5..5060ff4 100644 --- a/demo/src/LeanMonaco.tsx +++ b/demo/src/LeanMonaco.tsx @@ -29,7 +29,13 @@ function LeanMonacoComponent({options, numberEditors} : {options: LeanMonacoOpti <> {[...Array(numberEditors)].map((_x, i) => - + )}
From b91a0e341425505f9ff6bfe9de7899becb4a9e62 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 12 Sep 2024 18:40:38 +0200 Subject: [PATCH 2/2] restore LeanProject.lean --- demo/server/LeanProject/LeanProject.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/demo/server/LeanProject/LeanProject.lean b/demo/server/LeanProject/LeanProject.lean index e69de29..99415d9 100644 --- a/demo/server/LeanProject/LeanProject.lean +++ b/demo/server/LeanProject/LeanProject.lean @@ -0,0 +1 @@ +def hello := "world"