diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 00000000..3ea949c7 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "Projects/lean4web-tools"] + path = Projects/lean4web-tools + url = https://github.com/hhu-adam/lean4web-tools.git diff --git a/Projects/README.md b/Projects/README.md index 688bdff1..15ea06c4 100644 --- a/Projects/README.md +++ b/Projects/README.md @@ -12,4 +12,6 @@ Projects can be any Lean projects. "https://github.com/hhu-adam/lean4web-tools.git" @ "main" ``` in its `lakefile.lean`. This package adds some simple tools like `#package_version`. -3. For a project to appear in the settings, you need to modify `Settings.tsx` and add a new option with value `ProjectName`. +3. For a project to appear in the settings, you need to add it to `config.json`: + add a new entry `{folder: "_", name: "_"}` to `projects`, where "folder" is the + folder name inside `Projects/` and "name" is the free-text display name. diff --git a/Projects/lean4web-tools b/Projects/lean4web-tools new file mode 160000 index 00000000..9e6468e2 --- /dev/null +++ b/Projects/lean4web-tools @@ -0,0 +1 @@ +Subproject commit 9e6468e250c05450eedf4aff6e30290fb409af2b diff --git a/README.md b/README.md index 95350506..b009f164 100644 --- a/README.md +++ b/README.md @@ -33,9 +33,11 @@ nvm install node npm Now, install `git` and clone this repository: ``` sudo apt-get install git -git clone https://github.com/leanprover-community/lean4web.git +git clone --recurse-submodules https://github.com/leanprover-community/lean4web.git ``` +note that `--recurse-submodules` is needed to load the predefined projects in `Projects/`. + Install Bubblewrap: ``` sudo apt-get install bubblewrap @@ -111,7 +113,7 @@ Install [npm](https://www.npmjs.com/) and clone this repository. Inside the repo 1. `npm install`, to install dependencies 2. `npm run build_server`, to build contained lean projects under `Projects/` (or run `lake build` manually inside any lean project) 3. `npm start`, to start the server. - + The project can be accessed via http://localhost:3000. (Internally, websocket requests to `ws://localhost:3000/`websockets will be forwarded to a Lean server running on port 8080.) ## Running different projects diff --git a/client/src/Settings.tsx b/client/src/Settings.tsx index e80e04b8..60dde009 100644 --- a/client/src/Settings.tsx +++ b/client/src/Settings.tsx @@ -8,6 +8,7 @@ import Select from '@mui/material/Select'; 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' +import * as lean4webConfig from './config.json' const Settings: React.FC<{closeNav, theme, setTheme, project, setProject}> = ({closeNav, theme, setTheme, project, setProject}) => { @@ -142,9 +143,9 @@ const Settings: React.FC<{closeNav, theme, setTheme, project, setProject}> = setProject(ev.target.value) console.log(`set Lean project to: ${ev.target.value}`) }} > - - - + {lean4webConfig.projects.map(proj => + + )}

diff --git a/client/src/config.json b/client/src/config.json new file mode 100644 index 00000000..2a8557c9 --- /dev/null +++ b/client/src/config.json @@ -0,0 +1,6 @@ +{ + "projects": [ + {"folder": "lean4web-tools", "name": "Stable Lean"}, + {"folder": "MathlibLatest", "name": "Latest Mathlib"} + ] +}