fix: respect leanOptions in development mode

Author: joneugster

Projects/MathlibDemo/MathlibDemo.lean

@@ -6,3 +6,4 @@ import MathlibDemo.Bijection
 import MathlibDemo.Logic
 import MathlibDemo.Rational
 import MathlibDemo.Ring
+import MathlibDemo.MathlibDemo

Projects/MathlibDemo/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d6bc0a15829bf478c4ab90b491dd5e7f000021b1",
+   "rev": "81295dfbd8dc35fc1d1f399b7b61dd6cf6e05cb2",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

Projects/README.md

@@ -1,8 +1,8 @@
 # Adding Projects
 
-To add new projects, add any Lean project in the folder `Projects/`, e.g. `Projects/my-cool-project/`.
+To add new projects, add any Lean project in the folder `Projects/`, e.g. `Projects/MyCoolProject/`.
 You can either build your Lean project manually or you include a script
-`Projects/my-cool-project/build.sh` for automatic builds.
+`Projects/MyCoolProject/build.sh` for automatic builds.
 Usually a build script looks like this:
 
 ```
@@ -16,16 +16,16 @@ cd $(dirname $0)
 lake build
 ```
 
-A project added this way can then be accessed online with `https://your.url.com/#project=my-cool-project`.
+A project added this way can then be accessed online with `https://your.url.com/#project=MyCoolProject`.
 For the project to appear in the Settings, you need to update `client/config/config.json` by adding
-a new entry `{folder: "my-cool-project", name: "My Cool Project"}` to `projects`; here `folder` is the
+a new entry `{folder: "MyCoolProject", name: "My Cool Project"}` to `projects`; here `folder` is the
 folder name inside `Projects/` and `name` is the free-text display name.
 
 If you want to add Examples, you should add them as valid Lean files to your project and then expand
 the config entry of your project in `config.json` as follows:
 
 ```
-{ "folder": "my-cool-project`",
+{ "folder": "MyCoolProject`",
   "name": "My Cool Project",
   "examples": [
     { "file": "MyCustomProject/Demo1.lean",
@@ -35,6 +35,10 @@ the config entry of your project in `config.json` as follows:
 ```
 
 This will add an entry `My Cool Example` to the Example menu which loads
-the file from `Projects/my-cool-project/MyCustomProject/Demo1.lean`.
+the file from `Projects/MyCoolProject/MyCoolProject/Demo1.lean`.
 
 You might want to look at the provided `MathlibDemo` project for comparison.
+
+
+**Important**: In order for lake to use any "leanOptions" specified in the projects lakefile, you must make sure there is a file `Projects/MyCoolProject/MyCoolProject.lean`
+where folder name and file name coincide.

client/src/App.tsx

@@ -6,6 +6,7 @@ import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco'
 import LZString from 'lz-string'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faCode } from '@fortawesome/free-solid-svg-icons'
+import * as path from 'path'
 
 // Local imports
 import LeanLogo from './assets/logo.svg'
@@ -178,7 +179,7 @@ function App() {
     _leanMonaco.setInfoviewElement(infoviewRef.current!)
     ;(async () => {
         await _leanMonaco.start(options)
-        await leanMonacoEditor.start(editorRef.current!, `/project/${project}.lean`, code)
+        await leanMonacoEditor.start(editorRef.current!, path.join(project, `${project}.lean`), code)
 
         setEditor(leanMonacoEditor.editor)
         setLeanMonaco(_leanMonaco)

package-lock.json

@@ -7,12 +7,22 @@ ulimit -t 3600
 LEAN_ROOT="$(cd $1 && lean --print-prefix)"
 LEAN_PATH="$(cd $1 && lake env printenv LEAN_PATH)"
 
+PROJECT_NAME="$(basename $1)"
+
 # # print commands as they are executed
 # set -x
 
-if command -v bwrap >/dev/null 2>&1; then
+if ! command -v bwrap >/dev/null 2>&1; then
+  echo "bwrap is not installed! You could try to run the development server instead."
+  # # Could run without bubblewrap like this, but this might be an unwanted
+  # # security risk.
+  # (exec
+  #   cd $1
+  #   lake serve --
+  # )
+else
   (exec bwrap\
-    --ro-bind "$1" /project \
+    --ro-bind "$1" "/$PROJECT_NAME" \
     --ro-bind "$LEAN_ROOT" /lean \
     --ro-bind /usr /usr \
     --dev /dev \
@@ -32,13 +42,7 @@ if command -v bwrap >/dev/null 2>&1; then
     --unshare-uts  \
     --unshare-cgroup \
     --die-with-parent \
-    --chdir "/project/" \
-    lean --server
-  )
-else
-  echo "bwrap is not installed. Running without container." >&2
-  (exec
-    cd $1
+    --chdir "/$PROJECT_NAME/" \
     lean --server
   )
 fi

server/bubblewrap.sh

@@ -74,15 +74,18 @@ if (crtFile && keyFile) {
 
 const wss = new WebSocketServer({ server })
 
+// The path to the projects folder relative to the server
+let projectsBasePath = path.join(__dirname, '..', 'Projects')
+
 function startServerProcess(project) {
-  let projectPath = __dirname + `/../Projects/` + project
+  let projectPath = path.join(projectsBasePath, project)
 
   let serverProcess
   if (isDevelopment) {
     if (!isGithubAction) {
       console.warn("Running without Bubblewrap container!")
     }
-    serverProcess = cp.spawn("lean", ["--server"], { cwd: projectPath })
+    serverProcess = cp.spawn("lake", ["serve", "--"], { cwd: projectPath })
   } else {
     console.info("Running with Bubblewrap container.")
     serverProcess = cp.spawn("./bubblewrap.sh", [projectPath], { cwd: __dirname })
@@ -107,6 +110,40 @@ function startServerProcess(project) {
   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 urlRegEx = /^\/websocket\/([\w.-]+)$/
   const reRes = urlRegEx.exec(req.url)
@@ -127,12 +164,17 @@ wss.addListener("connection", function(ws, req) {
   const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close())
   const serverConnection = jsonrpcserver.createProcessStreamConnection(ps)
   socketConnection.forward(serverConnection, message => {
+    const prefix = isDevelopment ? projectsBasePath : "/"
+    urisToFilenames(prefix, message)
+
     if (isDevelopment && !isGithubAction) {
       console.log(`CLIENT: ${JSON.stringify(message)}`)
     }
     return message;
   })
   serverConnection.forward(socketConnection, message => {
+    const prefix = isDevelopment ? projectsBasePath : "/"
+    FilenamesToUri(prefix, message)
     if (isDevelopment && !isGithubAction) {
       console.log(`SERVER: ${JSON.stringify(message)}`)
     }