fix: leanOptions are not used unless file exists

cypress/e2e/spec.cy.ts

@@ -73,4 +73,22 @@ 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
+    })
+    // check that the lean option to display `fun _ ↦` is activated in the
+    // 1st editor
+    cy.visit('http://localhost:5173/')
+    cy.contains('#print f0')
+    cy.contains('#print f0').click()
+    cy.iframe().contains('def f0 : Nat → Nat := fun x ↦ x + 1')
+    // Test in the 3rd editor that the default setting is indeed still `fun _ =>`
+    cy.get('[data-cy="number-editors"]').type('{selectall}').type('3')
+    cy.contains('#print f2')
+    cy.contains('#print f2').click()
+    cy.iframe().contains('def f2 : Nat → Nat := fun x => x + 1')
+  })
 })

demo/server/LeanProject/LeanProject.lean

@@ -1 +1 @@
-def hello := "world"
+def hello := "world"

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.

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.

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⟩ ]

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("lake", ["serve", "--"], { 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))
     })
 

demo/src/LeanMonaco.tsx

@@ -1,6 +1,7 @@
 import { useEffect, useRef, createContext, useState } from 'react'
 import { LeanMonaco, LeanMonacoOptions } from 'lean4monaco'
 import LeanMonacoEditorComponent from './LeanMonacoEditor'
+import * as path from 'path'
 
 export const LeanMonacoContext = createContext<LeanMonaco|null>(null);
 
@@ -10,7 +11,7 @@ function LeanMonacoComponent({options, numberEditors} : {options: LeanMonacoOpti
 
   // You need to start one `LeanMonaco` instance once in your application using a `useEffect`
   useEffect(() => {
-    var _leanMonaco = new LeanMonaco()
+    const _leanMonaco = new LeanMonaco()
     setLeanMonaco(_leanMonaco)
     _leanMonaco.setInfoviewElement(infoviewRef.current!)
 
@@ -29,13 +30,20 @@ function LeanMonacoComponent({options, numberEditors} : {options: LeanMonacoOpti
     <>
       <LeanMonacoContext.Provider value={leanMonaco}>
         {[...Array(numberEditors)].map((_x, i) =>
-          <LeanMonacoEditorComponent key={i} fileName={`/project/test${i}.lean`} value={`#check ${i}`}/>
+          <LeanMonacoEditorComponent
+            key={i}
+            // fileName: must be a valid file inside the Lean project
+            // (or lake does not read the `leanOptions` in the `lakefile`), AND
+            // must be inside a folder, i.e. 'LeanProject.lean' does not work (monaco bug?) :(
+            fileName={path.join('LeanProject', `Test${i}.lean`)}
+            /* note: The sample content here is used for the cypress tests. */
+            value={`#check ${i}\ndef f${i} : Nat → Nat := fun x ↦ x + 1\n#print f${i}`}/>
         )}
         <div className='infoview' ref={infoviewRef}></div>
       </LeanMonacoContext.Provider>
 
       <div>
-        <button onClick={(_ev)=> {
+        <button onClick={() => {
           console.log('[LeanMonaco] restarting Lean')
           leanMonaco?.clientProvider?.getClients().map(client => {client.restart()})
         }}>Restart Lean</button>