Skip to content

Commit 96c6698

Browse files
joneugsterjoneugster
committed
mostly working
1 parent 928e687 commit 96c6698

File tree

7 files changed

+96
-26
lines changed

7 files changed

+96
-26
lines changed

‎Projects/MathlibDemo/leanweb-config.json‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
{
22
"name": "Latest Mathlib",
3+
"default": true,
34
"hidden": false,
45
"examples": [
56
{ "file": "MathlibDemo/Bijection.lean", "name": "Bijection" },

‎client/src/navigation/NavButton.tsx‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,19 +7,21 @@ export function NavButton({
77
icon,
88
iconElement,
99
text,
10+
title,
1011
onClick = () => {},
1112
href = undefined,
1213
}: {
1314
icon?: IconDefinition
1415
iconElement?: JSX.Element
1516
text: string
17+
title?: string
1618
onClick?: MouseEventHandler<HTMLAnchorElement>
1719
href?: string
1820
}) {
1921
// note: it seems that we can just leave the `target="_blank"` and it has no
2022
// effect on links without a `href`. If not, add `if (href)` statement here...
2123
return (
22-
<a className="nav-link" onClick={onClick} href={href!} target="_blank">
24+
<a className="nav-link" title={title} onClick={onClick} href={href!} target="_blank">
2325
{iconElement ?? <FontAwesomeIcon icon={icon!} />}&nbsp;{text}
2426
</a>
2527
)

‎client/src/navigation/Navigation.tsx‎

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ import ToolsPopup from '../Popups/Tools'
2929
import { mobileAtom } from '../settings/settings-atoms'
3030
import { SettingsPopup } from '../settings/SettingsPopup'
3131
import { setImportUrlAndProjectAtom } from '../store/import-atoms'
32-
import { projectAtom } from '../store/project-atoms'
32+
import { projectAtom, projectsAtom } from '../store/project-atoms'
3333
import { save } from '../utils/SaveToFile'
3434
import { Dropdown } from './Dropdown'
3535
import { NavButton } from './NavButton'
@@ -57,6 +57,7 @@ function FlexibleMenu({
5757
setLoadZulipOpen: Dispatch<SetStateAction<boolean>>
5858
}) {
5959
const [, setImportUrlAndProject] = useAtom(setImportUrlAndProjectAtom)
60+
const [{ data: projects }] = useAtom(projectsAtom)
6061
const loadFileFromDisk = (event: ChangeEvent<HTMLInputElement>) => {
6162
console.debug('Loading file from disk')
6263
const fileToLoad = event.target.files![0]
@@ -83,16 +84,17 @@ function FlexibleMenu({
8384
!isInDropdown && setOpenNav(false)
8485
}}
8586
>
86-
{lean4webConfig.projects?.map((proj) =>
87-
proj.examples?.map((example) => (
87+
{projects.map((it) =>
88+
it.config.examples?.map((example) => (
8889
<NavButton
89-
key={`${proj.name}-${example.name}`}
90+
key={`${it.config.name}-${example.name}`}
9091
icon={faStar}
9192
text={example.name}
93+
title={`${it.config.name}: ${example.name}`}
9294
onClick={() => {
9395
setImportUrlAndProject({
94-
url: `${window.location.origin}/api/example/${proj.folder}/${example.file}`,
95-
project: proj.folder,
96+
url: `${window.location.origin}/api/example/${it.folder}/${example.file}`,
97+
project: it.folder,
9698
})
9799
setOpenExample(false)
98100
}}
@@ -153,6 +155,7 @@ export function Menu({
153155
codeMirror: boolean
154156
setCodeMirror: Dispatch<SetStateAction<boolean>>
155157
}) {
158+
const [{ data: projects }] = useAtom(projectsAtom)
156159
const [project, setProject] = useAtom(projectAtom)
157160
const [code] = useAtom(codeAtom)
158161

@@ -183,9 +186,9 @@ export function Menu({
183186
console.log(`set Lean project to: ${ev.target.value}`)
184187
}}
185188
>
186-
{lean4webConfig.projects?.map((proj) => (
189+
{projects.map((proj) => (
187190
<option key={proj.folder} value={proj.folder}>
188-
{proj.name ?? proj.folder}
191+
{proj.config.name}
189192
</option>
190193
))}
191194
</select>

‎client/src/store/project-atoms.ts‎

Lines changed: 61 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,75 @@
11
import { atom } from 'jotai'
2+
import { atomWithQuery } from 'jotai-tanstack-query'
23

34
import { urlArgsAtom, urlArgsStableAtom } from './url-atoms'
45

5-
const DEFAULT_PROJECT = 'MathlibDemo'
6+
/* An example a project provides */
7+
export interface Example {
8+
file: string
9+
name: string
10+
}
11+
12+
/* A project's user configuration */
13+
export type ProjectConfig = {
14+
name: string
15+
hidden: boolean
16+
default: boolean
17+
examples: Example[]
18+
}
19+
20+
/* A project */
21+
export type Project = {
22+
folder: string
23+
config: ProjectConfig
24+
}
25+
26+
const projectsQueryAtom = atomWithQuery<Project[]>((get) => ({
27+
queryKey: ['projects'],
28+
queryFn: async () => {
29+
const res = await fetch(`/api/projects`)
30+
return res.json()
31+
},
32+
}))
33+
34+
/** Sort alphabetically while the `default` project always comes first */
35+
function sortProjects(p: Project, q: Project): number {
36+
if (p.config.default) return -1
37+
if (q.config.default) return 1
38+
return p.config.name.localeCompare(q.config.name)
39+
}
40+
41+
/** All available projects */
42+
export const projectsAtom = atom((get) => {
43+
const query = get(projectsQueryAtom)
44+
return { ...query, data: query.data?.sort(sortProjects) ?? [] }
45+
})
46+
47+
export const defaultProjectFolderAtom = atom((get) => {
48+
const projects = get(projectsAtom).data
49+
if (projects.length === 0) return 'MathlibDemo' // TODO: is this correct?
50+
const defaultProjects = projects.filter((it) => it.config.default)
51+
52+
if (defaultProjects.length === 0) {
53+
console.warn(`Expected exactly one default project, but found none.`)
54+
return projects[0].folder
55+
}
56+
if (defaultProjects.length > 1) {
57+
console.error(`Expected exactly one default project, but found ${defaultProjects.length}`)
58+
}
59+
return defaultProjects[0].folder
60+
})
661

762
/** The currently selected project */
863
export const projectAtom = atom(
964
(get) => {
1065
const urlArgs = get(urlArgsStableAtom)
11-
return urlArgs.project ?? DEFAULT_PROJECT
66+
return urlArgs.project ?? get(defaultProjectFolderAtom)
1267
},
1368
(get, set, project: string) => {
1469
const urlArgs = get(urlArgsStableAtom)
15-
set(urlArgsAtom, { ...urlArgs, project: project !== DEFAULT_PROJECT ? project : undefined })
70+
set(urlArgsAtom, {
71+
...urlArgs,
72+
project: project !== get(defaultProjectFolderAtom) ? project : undefined,
73+
})
1674
},
1775
)

‎doc/Installation.md‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
- [Back to README](../README.md)
22
- [User Manual](./Usage.md)
33
- Installation
4-
- [Adding Projects](./Projects.md)
54
- [Development](./Development.md)
65
- [Troubleshoot](./Troubleshoot.md)
76

@@ -77,11 +76,11 @@ On a running system, you might already have these installed, if not:
7776
```
7877
- Start the server
7978
```
80-
npm run production
79+
npm run prod
8180
```
8281
- To disable the bubblewrap containers, start the server with
8382
```
84-
ALLOW_NO_BUBBLEWRAP=true npm run production
83+
ALLOW_NO_BUBBLEWRAP=true npm run prod
8584
```
8685
- Start the client seperately, for example with
8786
```
@@ -90,7 +89,7 @@ On a running system, you might already have these installed, if not:
9089
and open http://localhost:3000
9190
- To set the locations of SSL certificates, use the following environment variables:
9291
```
93-
SSL_CRT_FILE=/path/to/crt_file.cer SSL_KEY_FILE=/path/to/private_ssl_key.pem npm run production
92+
SSL_CRT_FILE=/path/to/crt_file.cer SSL_KEY_FILE=/path/to/private_ssl_key.pem npm run prod
9493
```
9594

9695
### Adding different Lean projects

‎ecosystem.config.cjs‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ module.exports = {
88
NODE_ENV: "production",
99
PORT: 8001,
1010
ALLOW_NO_BUBBLEWRAP: false,
11-
GITHUB_ACTIONS: false,
1211
PROJECTS_BASE_PATH: "Projects", // relative path to the folder containing all projects
1312
SSL_CRT_FILE: undefined,
1413
SSL_KEY_FILE: undefined,

‎server/index.mjs‎

Lines changed: 17 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,13 @@
1-
import * as cp from "child_process";
1+
import * as cp from "node:child_process";
2+
import * as fs from "node:fs";
3+
import https from "node:https";
4+
import os from "node:os";
5+
import * as path from "node:path";
6+
import * as url from "node:url";
7+
28
import express from "express";
3-
import https from "https";
49
import anonymize from "ip-anonymize";
510
import nocache from "nocache";
6-
import os from "os";
7-
import * as path from "path";
8-
import * as url from "url";
911
import * as rpc from "vscode-ws-jsonrpc";
1012
import * as jsonrpcserver from "vscode-ws-jsonrpc/server";
1113
import { WebSocketServer } from "ws";
@@ -34,7 +36,7 @@ const keyFile = process.env.SSL_KEY_FILE;
3436
const PROJECTS_BASE_PATH = path.join(
3537
__dirname,
3638
"..",
37-
process.env.PROJECTS_BASE_PATH,
39+
process.env.PROJECTS_BASE_PATH ?? "Projects",
3840
);
3941

4042
const app = express();
@@ -44,6 +46,7 @@ app.get("/health", (_req, res) => {
4446
res.status(200).send("Server is running");
4547
});
4648

49+
// endpoint to list all available projects
4750
app.use("/api/projects", async (req, res) => {
4851
try {
4952
const entries = await fs.promises.readdir(PROJECTS_BASE_PATH, {
@@ -58,17 +61,22 @@ app.use("/api/projects", async (req, res) => {
5861
const configPath = path.join(projectDir, "leanweb-config.json");
5962

6063
let config = null;
61-
6264
try {
6365
const raw = await fs.promises.readFile(configPath, "utf-8");
6466
config = JSON.parse(raw);
6567
} catch (err) {
68+
console.debug(err);
6669
// File missing or invalid JSON — keep config as null
6770
}
6871

6972
projects.push({
70-
name: entry.name,
71-
config,
73+
folder: entry.name,
74+
config: {
75+
name: String(config.name), // TODO: ensure this is not null
76+
hidden: Boolean(config.hidden) ?? false,
77+
default: Boolean(config.default) ?? false,
78+
examples: config.examples ?? [], // TODO: validate
79+
},
7280
});
7381
}
7482

0 commit comments

Comments
 (0)