From 6a2fa7aa5648833641bfb3a402bbe4b318915a32 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 17 Dec 2023 00:31:23 +0100 Subject: [PATCH] refactor to allow different lean projects being run by the server --- Projects/.gitignore | 6 + .../MathlibLatest}/.gitignore | 0 .../MathlibLatest/MathlibLatest.lean | 0 Projects/MathlibLatest/build.sh | 26 ++++ .../MathlibLatest}/lake-manifest.json | 12 +- .../MathlibLatest}/lakefile.lean | 12 +- .../MathlibLatest}/lean-toolchain | 0 Projects/README.md | 13 ++ Projects/Webeditor/.gitignore | 3 + Projects/Webeditor/Webeditor.lean | 1 + .../Webeditor}/Webeditor/Tools.lean | 0 .../Webeditor/Tools/PackageVersion.lean | 0 Projects/Webeditor/build.sh | 15 ++ Projects/Webeditor/lake-manifest.json | 5 + Projects/Webeditor/lakefile.lean | 11 ++ Projects/Webeditor/lean-toolchain | 1 + client/src/App.tsx | 131 +++++++++++------- client/src/Editor.tsx | 37 +++-- client/src/Examples.tsx | 15 +- client/src/Settings.tsx | 25 +++- client/src/editor/leanclient.ts | 18 ++- server/WebsocketServer.js | 27 +++- server/bubblewrap.sh | 6 +- server/build.sh | 26 ---- 24 files changed, 267 insertions(+), 123 deletions(-) create mode 100644 Projects/.gitignore rename {server/LeanProject => Projects/MathlibLatest}/.gitignore (100%) rename server/LeanProject/Webeditor.lean => Projects/MathlibLatest/MathlibLatest.lean (100%) create mode 100755 Projects/MathlibLatest/build.sh rename {server/LeanProject => Projects/MathlibLatest}/lake-manifest.json (85%) rename {server/LeanProject => Projects/MathlibLatest}/lakefile.lean (71%) rename {server/LeanProject => Projects/MathlibLatest}/lean-toolchain (100%) create mode 100644 Projects/README.md create mode 100644 Projects/Webeditor/.gitignore create mode 100644 Projects/Webeditor/Webeditor.lean rename {server/LeanProject => Projects/Webeditor}/Webeditor/Tools.lean (100%) rename {server/LeanProject => Projects/Webeditor}/Webeditor/Tools/PackageVersion.lean (100%) create mode 100755 Projects/Webeditor/build.sh create mode 100644 Projects/Webeditor/lake-manifest.json create mode 100644 Projects/Webeditor/lakefile.lean create mode 100644 Projects/Webeditor/lean-toolchain delete mode 100755 server/build.sh diff --git a/Projects/.gitignore b/Projects/.gitignore new file mode 100644 index 00000000..88b59376 --- /dev/null +++ b/Projects/.gitignore @@ -0,0 +1,6 @@ +* + +# But not these files... +!.gitignore +!Wededitor/ +!MathlibLatest/ diff --git a/server/LeanProject/.gitignore b/Projects/MathlibLatest/.gitignore similarity index 100% rename from server/LeanProject/.gitignore rename to Projects/MathlibLatest/.gitignore diff --git a/server/LeanProject/Webeditor.lean b/Projects/MathlibLatest/MathlibLatest.lean similarity index 100% rename from server/LeanProject/Webeditor.lean rename to Projects/MathlibLatest/MathlibLatest.lean diff --git a/Projects/MathlibLatest/build.sh b/Projects/MathlibLatest/build.sh new file mode 100755 index 00000000..edf37eee --- /dev/null +++ b/Projects/MathlibLatest/build.sh @@ -0,0 +1,26 @@ +#!/usr/bin/env bash + +SECONDS=0 +PROJECT=${PWD##*/} +echo "Starting building $PROJECT." | logger -t lean4web + +# Operate in the directory where this file is located +cd $(dirname $0) + +# Updating Mathlib: We follow the instructions at +# https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4 +# +# Note: we had once problems with the `lake-manifest` when a new dependency got added +# to `mathlib`, we may need to add `rm lake-manifest.json` again if that's still a problem. + +# currently the mathlib post-update-hook is not good enough to update the lean-toolchain. +# things break if the new lakefile is not valid in the old lean version +curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain +# note: mathlib has now a post-update hook that modifies the `lean-toolchain` +# and calls `lake exe cache get`. +lake update -R +lake build + +duration=$SECONDS +echo "Finished $PROJECT in $(($duration / 60)):$(($duration % 60)) min." +echo "Finished $PROJECT in $(($duration / 60)):$(($duration % 60)) min." | logger -t lean4web diff --git a/server/LeanProject/lake-manifest.json b/Projects/MathlibLatest/lake-manifest.json similarity index 85% rename from server/LeanProject/lake-manifest.json rename to Projects/MathlibLatest/lake-manifest.json index eedb645b..3ebd026d 100644 --- a/server/LeanProject/lake-manifest.json +++ b/Projects/MathlibLatest/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "baf6defee1fe881ae535519c0776f37f6ef08603", + "rev": "6b4cf96c89e53cfcd73350bbcd90333a051ff4f0", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -49,11 +49,17 @@ {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "rev": "9a694d3f79f81f812c7ff3d1e39934df8a64bda6", + "rev": "c0148961fa8403e13328bf161931479a48cecfb3", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": false, + "configFile": "lakefile.lean"}, + {"type": "path", + "name": "webeditor", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "./../Webeditor", "configFile": "lakefile.lean"}], - "name": "webeditor", + "name": "mathlibLatest", "lakeDir": ".lake"} diff --git a/server/LeanProject/lakefile.lean b/Projects/MathlibLatest/lakefile.lean similarity index 71% rename from server/LeanProject/lakefile.lean rename to Projects/MathlibLatest/lakefile.lean index b31aadab..c8ffb680 100644 --- a/server/LeanProject/lakefile.lean +++ b/Projects/MathlibLatest/lakefile.lean @@ -1,14 +1,16 @@ import Lake open Lake DSL -package webeditor { - -- add package configuration options here -} - require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master" +require webeditor from ".." / "Webeditor" + +package mathlibLatest { + -- add package configuration options here +} + @[default_target] -lean_lib Webeditor { +lean_lib MathlibLatest { -- add library configuration options here } diff --git a/server/LeanProject/lean-toolchain b/Projects/MathlibLatest/lean-toolchain similarity index 100% rename from server/LeanProject/lean-toolchain rename to Projects/MathlibLatest/lean-toolchain diff --git a/Projects/README.md b/Projects/README.md new file mode 100644 index 00000000..ccc7b8ae --- /dev/null +++ b/Projects/README.md @@ -0,0 +1,13 @@ +# Adding Projects + +To add a new project, one needs to add a leanproject here. + +It's important that the project has a file `ProjectName/ProjectName.lean` which imports +anything required! Moreover, there should be a file `ProjectName/build.sh` which +can be called to update the project. + +A project would ideally import `import Webeditor from ".." / "Webeditor"` to allow +the custom lean tools to be available, but that's optional. + +You might want to update `Settings.tsx` and add an option to switch to the added +project. diff --git a/Projects/Webeditor/.gitignore b/Projects/Webeditor/.gitignore new file mode 100644 index 00000000..1282aa2b --- /dev/null +++ b/Projects/Webeditor/.gitignore @@ -0,0 +1,3 @@ +/build +/lake-packages/* +*.olean diff --git a/Projects/Webeditor/Webeditor.lean b/Projects/Webeditor/Webeditor.lean new file mode 100644 index 00000000..72185305 --- /dev/null +++ b/Projects/Webeditor/Webeditor.lean @@ -0,0 +1 @@ +import Webeditor.Tools diff --git a/server/LeanProject/Webeditor/Tools.lean b/Projects/Webeditor/Webeditor/Tools.lean similarity index 100% rename from server/LeanProject/Webeditor/Tools.lean rename to Projects/Webeditor/Webeditor/Tools.lean diff --git a/server/LeanProject/Webeditor/Tools/PackageVersion.lean b/Projects/Webeditor/Webeditor/Tools/PackageVersion.lean similarity index 100% rename from server/LeanProject/Webeditor/Tools/PackageVersion.lean rename to Projects/Webeditor/Webeditor/Tools/PackageVersion.lean diff --git a/Projects/Webeditor/build.sh b/Projects/Webeditor/build.sh new file mode 100755 index 00000000..19328045 --- /dev/null +++ b/Projects/Webeditor/build.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env bash + +SECONDS=0 +PROJECT=${PWD##*/} +echo "Starting building $PROJECT." | logger -t lean4web + +# Operate in the directory where this file is located +cd $(dirname $0) + +lake update -R +lake build + +duration=$SECONDS +echo "Finished $PROJECT in $(($duration / 60)):$(($duration % 60)) min." +echo "Finished $PROJECT in $(($duration / 60)):$(($duration % 60)) min." | logger -t lean4web diff --git a/Projects/Webeditor/lake-manifest.json b/Projects/Webeditor/lake-manifest.json new file mode 100644 index 00000000..35d1382c --- /dev/null +++ b/Projects/Webeditor/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": 7, + "packagesDir": ".lake/packages", + "packages": [], + "name": "webeditor", + "lakeDir": ".lake"} diff --git a/Projects/Webeditor/lakefile.lean b/Projects/Webeditor/lakefile.lean new file mode 100644 index 00000000..46519146 --- /dev/null +++ b/Projects/Webeditor/lakefile.lean @@ -0,0 +1,11 @@ +import Lake +open Lake DSL + +package webeditor { + -- add package configuration options here +} + +@[default_target] +lean_lib Webeditor { + -- add library configuration options here +} diff --git a/Projects/Webeditor/lean-toolchain b/Projects/Webeditor/lean-toolchain new file mode 100644 index 00000000..7638861c --- /dev/null +++ b/Projects/Webeditor/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:stable diff --git a/client/src/App.tsx b/client/src/App.tsx index 72ca2a73..ba4bec87 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -16,10 +16,23 @@ import Examples from './Examples' import LoadingMenu from './LoadingMenu' import { config } from './config/config' +function formatArgs(args) { + let out = '#' + Object.entries(args).map(([key, val]) => (val ? `${key}=${val}` : null)).filter((x) => x).join('&') + if (out == '#') { + return ' ' + } + return out +} -const App: React.FC = () => { - const [restart, setRestart] = useState() +function parseArgs() { + let _args = window.location.hash.replace('#', '').split('&').map((s) => s.split('=')).filter(x => x[0]) + console.log('parsed args') + console.log(Object.fromEntries(_args)) + return Object.fromEntries(_args) +} +const App: React.FC = () => { + const [restart, setRestart] = useState<(project?) => Promise>() const [navOpen, setNavOpen] = useState(false) const menuRef = React.useRef() const submenuRef = React.useRef() @@ -37,10 +50,54 @@ const App: React.FC = () => { setNavOpen(false) } - // Closing the dropdown menu or submenu when clicking outside it. - // Use `ev.stopPropagation()` or `ev.stopImmediatePropagation()` inside - // the menu to prevent. + /* Option to change themes */ + const isBrowserDefaultDark = () => window.matchMedia('(prefers-color-scheme: dark)').matches + const [theme, setTheme] = React.useState(isBrowserDefaultDark() ? 'GithubDark' : 'lightPlus') + + const [content, setContent] = useState('') + const [url, setUrl] = useState(null) + const [project, setProject] = useState('MathlibLatest') + const [contentFromUrl, setContentFromUrl] = useState(null) + + const readHash = () => { + let args = parseArgs() + if (args.code) {setContent(decodeURIComponent(args.code))} + if (args.url) {setUrl(decodeURIComponent(args.url))} + if (args.project) { + console.log(`setting project to ${args.project}`) + setProject(args.project) + } + } + + const onDidChangeContent = (newContent) => { + setContent(newContent) + } + + const save = () => { + var blob = new Blob([content], {type: "text/plain;charset=utf-8"}); + saveAs(blob, "Lean4WebDownload.lean"); + } + + const loadFromUrl = (url: string, project=null) => { + setUrl((oldUrl) => { + if (oldUrl === url) { + setContent(contentFromUrl) + } + return url + }) + if (project) { + setProject(project) + } + } + + useEffect(() => { + // Trigger onhashchange once in the beginning + readHash() + + // Closing the dropdown menu or submenu when clicking outside it. + // Use `ev.stopPropagation()` or `ev.stopImmediatePropagation()` inside + // the menu to prevent. document.body.addEventListener("click", (ev) => { if (menuRef?.current) { if (menuRef.current.contains(ev.target as HTMLElement)) { @@ -62,36 +119,24 @@ const App: React.FC = () => { }) }, []) - /* Option to change themes */ - const isBrowserDefaultDark = () => window.matchMedia('(prefers-color-scheme: dark)').matches - const [theme, setTheme] = React.useState(isBrowserDefaultDark() ? 'GithubDark' : 'lightPlus') - const [content, setContent] = useState('') - const [url, setUrl] = useState(null) - const [contentFromUrl, setContentFromUrl] = useState(null) - - const readHash = () => { - if (window.location.hash.startsWith('#code=')) { - setContent(decodeURIComponent(window.location.hash.substring(6))); - } - if (window.location.hash.startsWith('#url=')) { - setUrl(decodeURIComponent(window.location.hash.substring(5))); - } - } - if ("onhashchange" in window) // does the browser support the hashchange event? - window.addEventListener('hashchange', readHash) - - useEffect(() => { readHash(); }, []) // Trigger onhashchange once in the beginning + // // if ("onhashchange" in window) // does the browser support the hashchange event? + // // window.addEventListener('hashchange', readHash) useEffect(() => { - if (contentFromUrl === content) { - history.replaceState(undefined, undefined, '#url=' + encodeURIComponent(url)); + //let args = parseArgs() + let _project = (project == 'MathlibLatest' ? null : project) + if (content === contentFromUrl) { + let args = {project: _project, url: encodeURIComponent(url), code: null} + history.replaceState(undefined, undefined, formatArgs(args)) } else if (content === "") { - history.replaceState(undefined, undefined, ' '); + let args = {project: _project, url: null, code: null} + history.replaceState(undefined, undefined, formatArgs(args)) } else { - history.replaceState(undefined, undefined, '#code=' + encodeURIComponent(content)); + let args = {project: _project, url: null, code: encodeURIComponent(content)} + history.replaceState(undefined, undefined, formatArgs(args)) } - }, [content]) + }, [project, content]) useEffect(() => { if (url !== null) { @@ -110,23 +155,12 @@ const App: React.FC = () => { } }, [url]) - const onDidChangeContent = (newContent) => { - setContent(newContent) - } - - const save = () => { - var blob = new Blob([content], {type: "text/plain;charset=utf-8"}); - saveAs(blob, "Lean4WebDownload.lean"); - } - - const loadFromUrl = (url: string) => { - setUrl((oldUrl) => { - if (oldUrl === url) { - setContent(contentFromUrl) - } - return url - }) - } + useEffect(() => { + if (restart) { + console.log(`changing Lean version to ${project}`) + restart(project) + } + }, [project]) return (
@@ -148,7 +182,8 @@ const App: React.FC = () => { } - + Restart server @@ -174,7 +209,7 @@ const App: React.FC = () => {
}> + value={content} onDidChangeContent={onDidChangeContent} theme={theme} project={project}/> ) diff --git a/client/src/Editor.tsx b/client/src/Editor.tsx index c3fd77d6..3b472961 100644 --- a/client/src/Editor.tsx +++ b/client/src/Editor.tsx @@ -19,13 +19,11 @@ import { toSocket, WebSocketMessageWriter } from 'vscode-ws-jsonrpc' import { DisposingWebSocketMessageReader } from './reader' import { monacoSetup } from './monacoSetup' -const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + "/websocket" - monacoSetup() -const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: string}> = - ({setRestart, onDidChangeContent, value, theme}) => { - const uri = monaco.Uri.parse('file:///LeanProject/LeanProject.lean') +const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: string, project: string}> = + ({setRestart, onDidChangeContent, value, theme, project}) => { + const uri = monaco.Uri.parse(`file:///project/${project}.lean`) const [editor, setEditor] = useState(null) // const [editorApi, setEditorApi] = useState(null) const [infoviewApi, setInfoviewApi] = useState(null) @@ -84,6 +82,16 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: }) setEditor(editor) const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor) + return () => { + editor.dispose(); + model.dispose(); + abbrevRewriter.dispose(); + } + }, []) + + useEffect(() => { + const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + "/websocket" + "/" + project + console.log(`socket url: ${socketUrl}`) const connectionProvider : IConnectionProvider = { get: async () => { @@ -122,22 +130,23 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: } loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi) setInfoProvider(infoProvider) - client.restart() + client.restart(project) return () => { - editor.dispose(); - model.dispose(); - abbrevRewriter.dispose(); infoProvider.dispose(); client.dispose(); } - }, []) + }, [project]) const showRestartMessage = () => { setRestartMessage(true) } - const restart = async () => { - await infoProvider.client.restart(); + const restart = async (project) => { + if (!project) { + project = 'MathlibLatest' + } + console.log(`project got to here! ${project}`) + await infoProvider.client.restart(project); } useEffect(() => { @@ -157,7 +166,7 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: infoProvider.openPreview(editor, infoviewApi) const taskgutter = new LeanTaskGutter(infoProvider.client, editor) } - setRestart(() => restart) + setRestart((project?) => restart) }, [editor, infoviewApi, infoProvider]) @@ -190,7 +199,7 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: {restartMessage ? {setRestartMessage(false); restart()} } + restart={() => {setRestartMessage(false); restart(project)} } close={() => {setRestartMessage(false)}} /> : ''} diff --git a/client/src/Examples.tsx b/client/src/Examples.tsx index a469cc55..e2b97d86 100644 --- a/client/src/Examples.tsx +++ b/client/src/Examples.tsx @@ -2,18 +2,19 @@ import * as React from 'react' import { faStar } from '@fortawesome/free-solid-svg-icons'; import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'; -const Examples: React.FC<{loadFromUrl:(url: string) => void, openSubmenu: (ev: React.MouseEvent, component: React.JSX.Element) => void, closeNav: any}> = ({loadFromUrl, openSubmenu, closeNav}) => { +const Examples: React.FC<{loadFromUrl:(url: string, project?: string|null) => void, openSubmenu: (ev: React.MouseEvent, component: React.JSX.Element) => void, closeNav: any}> = ({loadFromUrl, openSubmenu, closeNav}) => { - const load = (file) => { - loadFromUrl(`${window.location.origin}/examples/${file}`) + const load = (file, project=null) => { + loadFromUrl(`${window.location.origin}/examples/${file}`, project) closeNav() } const exampleMenu = <> - load("logic.lean")}>Logic - load("bijection.lean")}>Bijections - load("rational.lean")}>Rational numbers - load("ring.lean")}>Commutative rings + load("logic.lean", "MathlibLatest")}>Logic + load("bijection.lean", "MathlibLatest")}>Bijections + load("rational.lean", "MathlibLatest")}>Rational numbers + load("ring.lean", "MathlibLatest")}>Commutative rings + {loadFromUrl("https://raw.githubusercontent.com/JOSHCLUNE/DuperDemo/main/DuperDemo.lean", "DuperDemo"); closeNav()}}>Duper return {openSubmenu(ev, exampleMenu)}}> diff --git a/client/src/Settings.tsx b/client/src/Settings.tsx index f604ed82..d1e967c3 100644 --- a/client/src/Settings.tsx +++ b/client/src/Settings.tsx @@ -9,8 +9,8 @@ import { useWindowDimensions } from './window_width'; import { Button, FormControl, InputLabel, MenuItem } from '@mui/material'; import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -const Settings: React.FC<{closeNav, theme, setTheme}> = - ({closeNav, theme, setTheme}) => { +const Settings: React.FC<{closeNav, theme, setTheme, project, setProject}> = + ({closeNav, theme, setTheme, project, setProject}) => { const [open, setOpen] = React.useState(false); const handleOpen = () => setOpen(true); const handleClose = () => setOpen(false); @@ -120,8 +120,27 @@ const Settings: React.FC<{closeNav, theme, setTheme}> =
-

Settings

{ev.preventDefault(); setOpen(false); closeNav()}}> +

Project settings

+

These settigns are stored in the URL as they change the project's setup

+

+ + +

+ +

User settings

+

These settings are not preserved unless you opt-in to save them.

{ + async restart (project): Promise { const startTime = Date.now() - console.log('[LeanClient] Restarting Lean Server') + if (!project) { + project = 'MathlibLatest' + } + + console.log(`[LeanClient] Restarting Lean Server with project ${project}`) if (this.isStarted()) { await this.stop() } @@ -202,7 +206,7 @@ export class LeanClient implements Disposable { console.log(`[LeanClient] running, started in ${end - startTime} ms`) this.running = true // may have been auto restarted after it failed. if (!insideRestart) { - this.restartedEmitter.fire(undefined) + this.restartedEmitter.fire() } } else if (s.newState === State.Stopped) { this.running = false @@ -242,13 +246,13 @@ export class LeanClient implements Disposable { // eslint-disable-next-line @typescript-eslint/no-unsafe-argument this.client.onNotification(starHandler as any, () => {}) - this.restartedEmitter.fire(undefined) + this.restartedEmitter.fire({project: project}) insideRestart = false } - async start (): Promise { - return await this.restart() - } + // async start (project): Promise { + // return await this.restart(project) + // } isStarted (): boolean { return this.client !== undefined diff --git a/server/WebsocketServer.js b/server/WebsocketServer.js index eec434a0..39656a0f 100644 --- a/server/WebsocketServer.js +++ b/server/WebsocketServer.js @@ -16,14 +16,14 @@ class ClientConnection { re = /Content-Length: (\d+)\r\n/i - constructor (ws, useBubblewrap) { + constructor (ws, useBubblewrap, project) { this.useBubblewrap = useBubblewrap - this.startProcess() + this.startProcess(project) this.ws = ws ws.on('message', (msg) => { - // console.log(`[client] ${msg}`) + console.log(`[client] ${msg}`) this.send(JSON.parse(msg.toString('utf8'))) }) @@ -95,23 +95,29 @@ class ClientConnection { this.lean.stdin.uncork() } - startProcess () { + startProcess (project) { + let path = __dirname + `/../Projects/` + project + + console.log(`The path is ${path}`) + let cmd, cmdArgs, cwd; if (this.useBubblewrap) { cmd = "./bubblewrap.sh"; - cmdArgs = []; + cmdArgs = [path]; cwd = __dirname; } else{ console.warn("Running without Bubblewrap container!") cmd = "lean"; cmdArgs = ["--server"]; - cwd = __dirname + "/LeanProject"; + cwd = path } this.lean = spawn(cmd, cmdArgs, { cwd }) } } +const urlRegEx = /^\/websocket\/([\w.-]+)$/ + class WebsocketServer { constructor(server, useBubblewrap) { @@ -119,11 +125,18 @@ class WebsocketServer { this.socketCounter = 0; this.wss.on('connection', (ws, req) => { + const reRes = urlRegEx.exec(req.url) + if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; } + const project = reRes[1] + + console.log(`Open with project: ${project}`) + this.socketCounter += 1; const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress) console.log(`[${new Date()}] Socket opened - ${ip}`) this.logStats() - new ClientConnection(ws, useBubblewrap) + + new ClientConnection(ws, useBubblewrap, project) ws.on('close', () => { console.log(`[${new Date()}] Socket closed - ${ip}`) this.socketCounter -= 1; diff --git a/server/bubblewrap.sh b/server/bubblewrap.sh index c0810c57..4ed047b6 100755 --- a/server/bubblewrap.sh +++ b/server/bubblewrap.sh @@ -1,9 +1,9 @@ #/bin/bash -ELAN_HOME=$(cd LeanProject && lake env printenv ELAN_HOME) +ELAN_HOME=$(cd Webeditor && lake env printenv ELAN_HOME) (exec bwrap\ - --bind ./LeanProject /LeanProject \ + --bind $1 /project \ --bind $ELAN_HOME /elan \ --bind /usr /usr \ --dev /dev \ @@ -21,6 +21,6 @@ ELAN_HOME=$(cd LeanProject && lake env printenv ELAN_HOME) --unshare-uts \ --unshare-cgroup \ --die-with-parent \ - --chdir "/LeanProject/" \ + --chdir "/project/" \ lean --server ) diff --git a/server/build.sh b/server/build.sh deleted file mode 100755 index 59fa44d0..00000000 --- a/server/build.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/usr/bin/env bash - -SECONDS=0 -echo "Starting build." | logger -t lean4web - -# Operate in the directory where this file is located -cd $(dirname $0) - -# Updating Mathlib: We follow the instructions at -# https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4 -# -# Note: we had once problems with the `lake-manifest` when a new dependency got added -# to `mathlib`, we may need to add `rm lake-manifest.json` again if that's still a problem. -( cd LeanProject && - # currently the mathlib post-update-hook is not good enough to update the lean-toolchain. - # things break if the new lakefile is not valid in the old lean version - curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain && - # note: mathlib has now a post-update hook that modifies the `lean-toolchain` - # and calls `lake exe cache get`. - lake update -R && - lake build) - - -duration=$SECONDS -echo "Finished in $(($duration / 60)):$(($duration % 60)) min." -echo "Finished in $(($duration / 60)):$(($duration % 60)) min." | logger -t lean4web