diff --git a/Projects/.gitignore b/Projects/.gitignore index 88b59376..cf420dfd 100644 --- a/Projects/.gitignore +++ b/Projects/.gitignore @@ -2,5 +2,6 @@ # But not these files... !.gitignore -!Wededitor/ -!MathlibLatest/ +!lean4web-tools/ +!mathlib-demo/ +!README.md diff --git a/Projects/MathlibLatest/MathlibLatest.lean b/Projects/MathlibLatest/MathlibLatest.lean index 38611278..209d7df7 100644 --- a/Projects/MathlibLatest/MathlibLatest.lean +++ b/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 diff --git a/Projects/MathlibLatest/build.sh b/Projects/MathlibLatest/build.sh deleted file mode 100755 index 751de763..00000000 --- a/Projects/MathlibLatest/build.sh +++ /dev/null @@ -1,20 +0,0 @@ -#!/usr/bin/env bash - -# 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 diff --git a/Projects/MathlibLatest/lake-manifest.json b/Projects/MathlibLatest/lake-manifest.json deleted file mode 100644 index 54a2fd84..00000000 --- a/Projects/MathlibLatest/lake-manifest.json +++ /dev/null @@ -1,77 +0,0 @@ -{"version": 7, - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/leanprover/std4", - "type": "git", - "subDir": null, - "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb", - "name": "std", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.30", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/import-graph.git", - "type": "git", - "subDir": null, - "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4", - "type": "git", - "subDir": null, - "rev": "c0fb64828c4e8ac4e0d8ca1c646fd4228ca06aac", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/hhu-adam/lean4web-tools.git", - "type": "git", - "subDir": null, - "rev": "9e6468e250c05450eedf4aff6e30290fb409af2b", - "name": "webeditor", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}], - "name": "mathlibLatest", - "lakeDir": ".lake"} diff --git a/Projects/MathlibLatest/lakefile.lean b/Projects/MathlibLatest/lakefile.lean deleted file mode 100644 index 2ae0b9ab..00000000 --- a/Projects/MathlibLatest/lakefile.lean +++ /dev/null @@ -1,17 +0,0 @@ -import Lake -open Lake DSL - -require mathlib from git - "https://github.com/leanprover-community/mathlib4"@"master" - -require webeditor from git - "https://github.com/hhu-adam/lean4web-tools.git" @ "main" - -package mathlibLatest { - -- add package configuration options here -} - -@[default_target] -lean_lib MathlibLatest { - -- add library configuration options here -} diff --git a/Projects/MathlibLatest/lean-toolchain b/Projects/MathlibLatest/lean-toolchain deleted file mode 100644 index 9ad30404..00000000 --- a/Projects/MathlibLatest/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.7.0 diff --git a/Projects/README.md b/Projects/README.md index 15ea06c4..58a55dc7 100644 --- a/Projects/README.md +++ b/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. diff --git a/Projects/MathlibLatest/.gitignore b/Projects/mathlib-demo/.gitignore similarity index 100% rename from Projects/MathlibLatest/.gitignore rename to Projects/mathlib-demo/.gitignore diff --git a/client/public/examples/bijection.lean b/client/public/examples/bijection.lean deleted file mode 100644 index 1c135014..00000000 --- a/client/public/examples/bijection.lean +++ /dev/null @@ -1,25 +0,0 @@ -import Mathlib.Logic.Equiv.Basic -- import the theory --- of bijections as functions with two-sided inverses - --- Let X, Y and Z be sets -variable (X Y Z : Type) - --- Then there's a bijection between functions `X × Y → Z` --- and functions from `X` to (the space of functions from `Y` to `Z`). - -example : (X × Y → Z) ≃ (X → (Y → Z)) := -{ -- to go from f : X × Y → Z to a function X → (Y → Z), - -- send x and y to f(x,y) - toFun := fun f ↦ (fun x y ↦ f (x,y)) - -- to go from g : X → (Y → Z) to a function X × Y → Z, - -- send a pair p=(x,y) to (g p.1) (p.2) where p.i is the i'th element of p - invFun := fun g ↦ (fun p ↦ g p.1 p.2) - -- Here we prove that if f ↦ g ↦ f' then f' = f - left_inv := by - intro f -- let f : X × Y → Z be arbitrary. - rfl -- turns out f' = f by definition - -- here we prove that if g ↦ f ↦ g' then g' = g - right_inv := by - intro g -- let f : X → (Y → Z) by arbitrary - rfl -- turns out that g' = g by definition -} diff --git a/client/public/examples/logic.lean b/client/public/examples/logic.lean deleted file mode 100644 index f10f9cc8..00000000 --- a/client/public/examples/logic.lean +++ /dev/null @@ -1,16 +0,0 @@ -import Mathlib.Logic.Basic -- basic facts in logic -import Mathlib.Tactic.LibrarySearch -- a tactic which searches for --- theorems in Lean's mathematics library - --- Let P and Q be true-false statements -variable (P Q : Prop) - --- The following is a basic result in logic -example : ¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q := by - -- its proof is already in Lean's mathematics library - exact not_and_or - --- Here is another basic result in logic -example : ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q := by - apply? -- we can search for the proof in the library - -- we can also replace `apply?` with its output diff --git a/client/public/examples/rational.lean b/client/public/examples/rational.lean deleted file mode 100644 index c8626d90..00000000 --- a/client/public/examples/rational.lean +++ /dev/null @@ -1,16 +0,0 @@ -import Mathlib.Data.Rat.Order -- import the rationals -import Mathlib.Data.Rat.Init -- import notation ℚ for rationals -import Mathlib.Tactic.Linarith -- a linear arithmetic tactic -import Mathlib.Tactic.Ring -- import the `ring` tactic - --- let `x`, `y` and `z` be rationals -variable (x y z : ℚ) - --- let's prove that if `x < y` and `y + 3 < z + 10` then `x + 37 < z + 44` -example (h₁ : x < y) (h₂ : y + 3 < z + 10) : x + 37 < z + 44 := by - linarith -- the `linarith` tactic can do this automatically - --- let's prove that (x+y)^2=x^2+2*x*y+y^2 - -example : (x + y)^2 = x^2 + 2 * x * y + y^2 := by - ring -- the `ring` tactic can do this automatically diff --git a/client/public/examples/ring.lean b/client/public/examples/ring.lean deleted file mode 100644 index e77849f0..00000000 --- a/client/public/examples/ring.lean +++ /dev/null @@ -1,13 +0,0 @@ -import Mathlib.Tactic.Ring -- import the `ring` tactic - --- let R be a commutative ring (for example the real numbers) -variable (R : Type) [CommRing R] - --- let x and y be elements of R -variable (x y : R) - --- then (x+y)*(x+2y)=x^2+3xy+2y^2 - -example : (x+y)*(x+2*y)=x^2+3*x*y+2*y^2 := by - -- the `ring` tactic solves this goal automatically - ring diff --git a/client/src/App.tsx b/client/src/App.tsx index 637f3bf9..60c3d91e 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -54,7 +54,7 @@ const App: React.FC = () => { const [content, setContent] = useState('') const [url, setUrl] = useState(null) - const [project, setProject] = useState('MathlibLatest') + const [project, setProject] = useState('mathlib-demo') const [contentFromUrl, setContentFromUrl] = useState(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)) diff --git a/client/src/Editor.tsx b/client/src/Editor.tsx index caf5c4ea..70a39cf3 100644 --- a/client/src/Editor.tsx +++ b/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); diff --git a/client/src/Examples.tsx b/client/src/Examples.tsx index e2b97d86..998c6532 100644 --- a/client/src/Examples.tsx +++ b/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 = <> - 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 + {lean4webConfig.projects.map(proj => proj.examples?.map(example => + load(`${proj.folder}/${example.file}`, proj.folder)}>{example.name} + + ))} return {openSubmenu(ev, exampleMenu)}}> diff --git a/client/src/Settings.tsx b/client/src/Settings.tsx index 60dde009..5003d27b 100644 --- a/client/src/Settings.tsx +++ b/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 => - + )}

diff --git a/client/src/config.json b/client/src/config.json index 2a8557c9..147d86cf 100644 --- a/client/src/config.json +++ b/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"} + ]} ] } diff --git a/client/src/editor/leanclient.ts b/client/src/editor/leanclient.ts index 1f31b0fc..40618101 100644 --- a/client/src/editor/leanclient.ts +++ b/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}`) diff --git a/server/index.js b/server/index.js index 23950fee..b00fd343 100644 --- a/server/index.js +++ b/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; diff --git a/vite.config.ts b/vite.config.ts index 5f213bab..48b768c4 100644 --- a/vite.config.ts +++ b/vite.config.ts @@ -33,6 +33,9 @@ export default defineConfig({ target: 'ws://localhost:8080', ws: true }, + '/examples': { + target: 'http://localhost:8080', + }, } }, resolve: {