creat config.json for adding projects

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "Projects/lean4web-tools"]
+	path = Projects/lean4web-tools
+	url = https://github.com/hhu-adam/lean4web-tools.git

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.

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

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}`)
                     }} >
-                <option value="plain">Stable Lean</option>
-                <option value="MathlibLatest">Latest Mathlib</option>
-                <option value="DuperDemo">Latest Duper</option>
+                {lean4webConfig.projects.map(proj =>
+                  <option key={proj.folder} value={proj.folder}>{proj.name}</option>
+                )}
               </select>
             </p>
 

client/src/config.json

@@ -0,0 +1,6 @@
+{
+  "projects": [
+    {"folder": "lean4web-tools", "name": "Stable Lean"},
+    {"folder": "MathlibLatest", "name": "Latest Mathlib"}
+  ]
+}