diff --git a/.gitmodules b/.gitmodules index 3ea949c7..e69de29b 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +0,0 @@ -[submodule "Projects/lean4web-tools"] - path = Projects/lean4web-tools - url = https://github.com/hhu-adam/lean4web-tools.git diff --git a/Projects/README.md b/Projects/README.md index 58a55dc7..59ed7300 100644 --- a/Projects/README.md +++ b/Projects/README.md @@ -1,32 +1,40 @@ # Adding Projects -To add a new project, one needs to add a lean project here. - -Projects can be any Lean projects. - -1. You can build the lean project manually. For automatic updates, your project should include a file `ProjectName/build.sh` which can be - executed to build the project. See [lean4web-tools](https://github.com/hhu-adam/lean4web-tools) for an example. -2. Your project should add the dependency - ```lean - require webeditor from git - "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 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. +To add new projects, add any Lean project in the folder `Projects/`, e.g. `Projects/my-cool-project/`. +You can either build your Lean project manually or you include a script +`Projects/my-cool-project/build.sh` for automatic builds. +Usually a build script looks like this: + +``` +#!/usr/bin/env bash + +# Operate in the directory where this file is located +cd $(dirname $0) + +# add code here to update the project correctly + +lake build +``` + +A project added this way can then be accessed online with `https://your.url.com/#project=my-cool-project`. +For the project to appear in the Settings, you need to update `client/config/config.json` by adding +a new entry `{folder: "my-cool-project", name: "My Cool Project"}` to `projects`; here `folder` is the +folder name inside `Projects/` and `name` is the free-text display name. + +If you want to add Examples, you should add them as valid Lean files to your project and then expand +the config entry of your project in `config.json` as follows: + +``` +{ "folder": "my-cool-project`", + "name": "My Cool Project", + "examples": [ + { "file": "MyCustomProject/Demo1.lean", + "name": "My Cool Example" } + ] +} +``` + +This will add an entry `My Cool Example` to the Example menu which loads +the file from `Projects/my-cool-project/MyCustomProject/Demo1.lean`. + +You might want to look at the provided `mathlib-demo` project for comparison. diff --git a/Projects/lean4web-tools b/Projects/lean4web-tools deleted file mode 160000 index c6997031..00000000 --- a/Projects/lean4web-tools +++ /dev/null @@ -1 +0,0 @@ -Subproject commit c69970315e29af067b8518995175f6195d4a8f6b diff --git a/Projects/mathlib-demo/lakefile.toml b/Projects/mathlib-demo/lakefile.toml index cdb7b388..7f8b742d 100644 --- a/Projects/mathlib-demo/lakefile.toml +++ b/Projects/mathlib-demo/lakefile.toml @@ -6,10 +6,5 @@ name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" rev = "master" -[[require]] -name = "webeditor" -git = "https://github.com/hhu-adam/lean4web-tools.git" -rev = "main" - [[lean_lib]] name = "MathlibLatest" diff --git a/Projects/stable/.gitignore b/Projects/stable/.gitignore new file mode 100644 index 00000000..bfb30ec8 --- /dev/null +++ b/Projects/stable/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/Projects/stable/Stable.lean b/Projects/stable/Stable.lean new file mode 100644 index 00000000..e69de29b diff --git a/Projects/stable/build.sh b/Projects/stable/build.sh new file mode 100755 index 00000000..34451d01 --- /dev/null +++ b/Projects/stable/build.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash + +# Operate in the directory where this file is located +cd $(dirname $0) + +lake update -R +lake build diff --git a/Projects/stable/lake-manifest.json b/Projects/stable/lake-manifest.json new file mode 100644 index 00000000..9de15084 --- /dev/null +++ b/Projects/stable/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": 7, + "packagesDir": ".lake/packages", + "packages": [], + "name": "stable", + "lakeDir": ".lake"} diff --git a/Projects/stable/lakefile.lean b/Projects/stable/lakefile.lean new file mode 100644 index 00000000..30239663 --- /dev/null +++ b/Projects/stable/lakefile.lean @@ -0,0 +1,9 @@ +import Lake +open Lake DSL + +package «stable» where + -- add package configuration options here + +@[default_target] +lean_lib «Stable» where + -- add library configuration options here diff --git a/Projects/stable/lean-toolchain b/Projects/stable/lean-toolchain new file mode 100644 index 00000000..7638861c --- /dev/null +++ b/Projects/stable/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:stable diff --git a/client/src/Popups/Tools.tsx b/client/src/Popups/Tools.tsx index bb01c4f5..51e2a0d8 100644 --- a/client/src/Popups/Tools.tsx +++ b/client/src/Popups/Tools.tsx @@ -101,6 +101,12 @@ const ToolsPopup: React.FC<{ } )} +

Tools

+

+ To see the actual Lean version implied by the toolchain above, the following can be pasted + into the editor: +

+
#eval Lean.versionString
} diff --git a/client/src/config/config.tsx b/client/src/config/config.tsx index 970756b0..7785477a 100644 --- a/client/src/config/config.tsx +++ b/client/src/config/config.tsx @@ -11,14 +11,8 @@ const lean4webConfig = { "name": "Ring" }, { "file": "MathlibLatest/Rational.lean", "name": "Rational" }]}, - { "folder": "lean4web-tools", - "name": "Stable Lean" }, - { "folder": "DuperDemo", - "name": "Duper", - "examples": [ - { "file": "DuperDemo.lean", - "name": "Duper" }] - } + { "folder": "stable", + "name": "Stable Lean" } ], "serverCountry": "Germany", "contactInformation": <> diff --git a/client/src/css/test.css b/client/src/css/test.css new file mode 100644 index 00000000..07294233 --- /dev/null +++ b/client/src/css/test.css @@ -0,0 +1,3 @@ +body { + background-color: lightgoldenrodyellow !important; +} \ No newline at end of file