Merge branch 'dev'

.eslintrc.cjs

@@ -0,0 +1,18 @@
+module.exports = {
+  root: true,
+  env: { browser: true, es2020: true },
+  extends: [
+    'eslint:recommended',
+    'plugin:@typescript-eslint/recommended',
+    'plugin:react-hooks/recommended',
+  ],
+  ignorePatterns: ['dist', '.eslintrc.cjs'],
+  parser: '@typescript-eslint/parser',
+  plugins: ['react-refresh'],
+  rules: {
+    'react-refresh/only-export-components': [
+      'warn',
+      { allowConstantExport: true },
+    ],
+  },
+}

.gitignore

@@ -1,7 +1,26 @@
+# Logs
+logs
+*.log
+npm-debug.log*
+yarn-debug.log*
+yarn-error.log*
+pnpm-debug.log*
+lerna-debug.log*
+
 node_modules
-client/dist
-server/build
-client/public/package_versions.json
 dist
-**/.DS_Store
+dist-ssr
+*.local
+
 **/.lake
+
+# Editor directories and files
+.vscode/*
+!.vscode/extensions.json
+.idea
+.DS_Store
+*.suo
+*.ntvs*
+*.njsproj
+*.sln
+*.sw?

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.

Projects/mathlib-demo/MathlibLatest.lean

@@ -1,4 +1,3 @@
-import Webeditor
 import Mathlib
 import ProofWidgets
 

Projects/mathlib-demo/lake-manifest.json

@@ -1,10 +1,11 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "7110da53bf6da84198dba69ca90221c4798ade35",
+   "scope": "leanprover-community",
+   "rev": "41bc768e2224d6c75128a877f1d6e198859b3178",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +14,8 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "scope": "leanprover-community",
+   "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "d68b34fabd37681e6732be752b7e90aaac7aa0e0",
+   "scope": "leanprover-community",
+   "rev": "6058ab8d938c5104eace7d0fb5ac17b21cb067b1",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "scope": "leanprover-community",
+   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.40",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "b167323652ab59a5d1b91e906ca4172d1c0474b7",
+   "scope": "leanprover-community",
+   "rev": "e7e90d90a62e6d12cbb27cbbfc31c094ee4ecc58",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,20 +64,12 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "5795dea5a47ba1d4735896548b96dd0bb38cf248",
+   "scope": "",
+   "rev": "7669be18c4affa2e4909d4edc9d3c81c03d5e3ed",
    "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": "8be7734dfa9a686d3a1329651e2a1a690e1123b6",
-   "name": "webeditor",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "mathlibLatest",
  "lakeDir": ".lake"}

Projects/mathlib-demo/lakefile.toml

@@ -0,0 +1,10 @@
+name = "mathlibLatest"
+defaultTargets = ["MathlibLatest"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "master"
+
+[[lean_lib]]
+name = "MathlibLatest"

Projects/mathlib-demo/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc2
+leanprover/lean4:v4.10.0

Projects/stable/.gitignore

@@ -0,0 +1 @@
+/.lake

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

Projects/stable/lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "stable",
+ "lakeDir": ".lake"}

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

Projects/stable/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:stable