custom examples from projects

Projects/.gitignore

@@ -2,5 +2,6 @@
 
 # But not these files...
 !.gitignore
-!Wededitor/
-!MathlibLatest/
+!lean4web-tools/
+!mathlib-demo/
+!README.md

Projects/MathlibLatest/MathlibLatest.lean

@@ -1,3 +1,8 @@
 import Webeditor
 import Mathlib
 import ProofWidgets
+
+import Examples.Bijection
+import MathlibLatest.Logic
+import MathlibLatest.Rational
+import MathlibLatest.Ring

Projects/README.md

@@ -15,3 +15,18 @@ Projects can be any Lean projects.
 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.
+
+* Optionally, you can also specify examples in the `config.json` each of these
+    examples will appear under "Examples" in the menu. A full project entry would then
+    look as follows:
+    ```
+    { "folder": "folder name inside `Projects/`",
+      "name": "My Custom Lean Demo",
+      "examples": [
+        { "file": "path/inside/the/lean/package.lean",
+          "name": "My Cool Example"},
+        ...
+      ]
+    }
+    ```
+* Compare to the entry for the `mathlib-demo` project.

client/src/App.tsx

@@ -54,7 +54,7 @@ const App: React.FC = () => {
 
   const [content, setContent] = useState<string>('')
   const [url, setUrl] = useState<string>(null)
-  const [project, setProject] = useState<string>('MathlibLatest')
+  const [project, setProject] = useState<string>('mathlib-demo')
   const [contentFromUrl, setContentFromUrl] = useState<string>(null)
 
   const readHash = () => {
@@ -123,7 +123,7 @@ const App: React.FC = () => {
 
   useEffect(() => {
     //let args = parseArgs()
-    let _project = (project == 'MathlibLatest' ? null : project)
+    let _project = (project == 'mathlib-demo' ? null : project)
     if (content === contentFromUrl) {
       let args = {project: _project, url: encodeURIComponent(url), code: null}
       history.replaceState(undefined, undefined, formatArgs(args))

client/src/Editor.tsx

@@ -145,7 +145,7 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
 
   const restart = async (project) => {
     if (!project) {
-      project = 'MathlibLatest'
+      project = 'mathlib-demo'
     }
     console.log(`project got to here! ${project}`)
     await infoProvider.client.restart(project);

client/src/Examples.tsx

@@ -1,6 +1,7 @@
 import * as React from 'react'
 import { faStar } from '@fortawesome/free-solid-svg-icons';
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome';
+import * as lean4webConfig from './config.json'
 
 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}) => {
 
@@ -10,11 +11,10 @@ const Examples: React.FC<{loadFromUrl:(url: string, project?: string|null) => vo
   }
 
   const exampleMenu = <>
-    <span className="nav-link" onClick={() => load("logic.lean", "MathlibLatest")}>Logic</span>
-    <span className="nav-link" onClick={() => load("bijection.lean", "MathlibLatest")}>Bijections</span>
-    <span className="nav-link" onClick={() => load("rational.lean", "MathlibLatest")}>Rational numbers</span>
-    <span className="nav-link" onClick={() => load("ring.lean", "MathlibLatest")}>Commutative rings</span>
-    <span className="nav-link" onClick={() => {loadFromUrl("https://raw.githubusercontent.com/JOSHCLUNE/DuperDemo/main/DuperDemo.lean", "DuperDemo"); closeNav()}}>Duper</span>
+    {lean4webConfig.projects.map(proj => proj.examples?.map(example =>
+      <span key={`${proj.name}-${example.name}`} className="nav-link" onClick={() => load(`${proj.folder}/${example.file}`, proj.folder)}>{example.name}</span>
+
+    ))}
   </>
 
   return <span className="nav-link" onClick={(ev) => {openSubmenu(ev, exampleMenu)}}>

client/src/Settings.tsx

@@ -144,7 +144,7 @@ const Settings: React.FC<{closeNav, theme, setTheme, project, setProject}> =
                     console.log(`set Lean project to: ${ev.target.value}`)
                     }} >
                 {lean4webConfig.projects.map(proj =>
-                  <option key={proj.folder} value={proj.folder}>{proj.name}</option>
+                  <option key={proj.folder} value={proj.folder}>{proj.name ?? proj.folder}</option>
                 )}
               </select>
             </p>

client/src/config.json

@@ -1,6 +1,22 @@
 {
   "projects": [
-    {"folder": "lean4web-tools", "name": "Stable Lean"},
-    {"folder": "MathlibLatest", "name": "Latest Mathlib"}
+    { "folder": "lean4web-tools",
+      "name": "Stable Lean",
+      "examples": [
+        {"file": "Webeditor.lean", "name": "Test"}
+      ]
+    },
+    { "folder": "mathlib-demo",
+      "name": "Latest Mathlib",
+      "examples": [
+        { "file": "MathlibLatest/Bijection.lean",
+          "name": "Bijection"},
+        { "file": "MathlibLatest/Logic.lean",
+          "name": "Logic"},
+        { "file": "MathlibLatest/Ring.lean",
+          "name": "Ring"},
+        { "file": "MathlibLatest/Rational.lean",
+          "name": "Rational"}
+      ]}
   ]
 }

client/src/editor/leanclient.ts

@@ -98,7 +98,7 @@ export class LeanClient implements Disposable {
     const startTime = Date.now()
 
     if (!project) {
-      project = 'MathlibLatest'
+      project = 'mathlib-demo'
     }
 
     console.log(`[LeanClient] Restarting Lean Server with project ${project}`)

server/index.js

@@ -13,7 +13,15 @@ const crtFile = process.env.SSL_CRT_FILE
 const keyFile = process.env.SSL_KEY_FILE
 
 const app = express()
-app.use(express.static(path.join(__dirname, '../client/dist/')))
+app.use('/examples/*', (req, res, next) => {
+  const filename = req.params[0];
+  console.debug(`trying to load ${filename}`)
+  req.url = filename;
+  express.static(path.join(__dirname, '..', 'Projects'))(req, res, next)
+  // express.static(path.join(__dirname, '..', 'Projects', filename))(req, res, next);
+})
+app.use(express.static(path.join(__dirname, '..', 'client', 'dist')))
+
 app.use(nocache())
 
 let server;

vite.config.ts

@@ -33,6 +33,9 @@ export default defineConfig({
         target: 'ws://localhost:8080',
         ws: true
       },
+      '/examples': {
+        target: 'http://localhost:8080',
+      },
     }
   },
   resolve: {