diff --git a/Projects/MathlibLatest/MathlibLatest.lean b/Projects/MathlibLatest/MathlibLatest.lean index 5e0851f1..f3335e00 100644 --- a/Projects/MathlibLatest/MathlibLatest.lean +++ b/Projects/MathlibLatest/MathlibLatest.lean @@ -1,3 +1,2 @@ import Mathlib import ProofWidgets -import Webeditor.Tools diff --git a/Projects/MathlibLatest/lake-manifest.json b/Projects/MathlibLatest/lake-manifest.json index 3ebd026d..b127db47 100644 --- a/Projects/MathlibLatest/lake-manifest.json +++ b/Projects/MathlibLatest/lake-manifest.json @@ -54,12 +54,6 @@ "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": false, - "configFile": "lakefile.lean"}, - {"type": "path", - "name": "webeditor", - "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "./../Webeditor", "configFile": "lakefile.lean"}], "name": "mathlibLatest", "lakeDir": ".lake"} diff --git a/Projects/MathlibLatest/lakefile.lean b/Projects/MathlibLatest/lakefile.lean index c8ffb680..5d87e806 100644 --- a/Projects/MathlibLatest/lakefile.lean +++ b/Projects/MathlibLatest/lakefile.lean @@ -4,8 +4,6 @@ open Lake DSL require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master" -require webeditor from ".." / "Webeditor" - package mathlibLatest { -- add package configuration options here } diff --git a/Projects/README.md b/Projects/README.md index ccc7b8ae..1797ca07 100644 --- a/Projects/README.md +++ b/Projects/README.md @@ -6,8 +6,5 @@ It's important that the project has a file `ProjectName/ProjectName.lean` which anything required! Moreover, there should be a file `ProjectName/build.sh` which can be called to update the project. -A project would ideally import `import Webeditor from ".." / "Webeditor"` to allow -the custom lean tools to be available, but that's optional. - You might want to update `Settings.tsx` and add an option to switch to the added project. diff --git a/server/build.sh b/server/build.sh new file mode 100755 index 00000000..cd85d82f --- /dev/null +++ b/server/build.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +SECONDS=0 + +cd $(dirname $0) + +../Projects/Webeditor/build.sh +../Projects/MathlibLatest/build.sh