feat: add prettier code formatting and tailwindCSS

.editorconfig

@@ -0,0 +1,9 @@
+root = true
+
+[*]
+charset = utf-8
+indent_style = space
+indent_size = 2
+end_of_line = lf
+insert_final_newline = true
+trim_trailing_whitespace = true

.eslintrc.cjs

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

.vscode/settings.json

@@ -0,0 +1,4 @@
+{
+  "editor.formatOnSave": true,
+  "editor.defaultFormatter": "esbenp.prettier-vscode"
+}

Projects/MathlibDemo/lake-manifest.json

@@ -1,95 +1,116 @@
-{"version": "1.1.0",
- "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/leanprover-community/mathlib4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "d68c4dc09f5e000d3c968adae8def120a0758729",
-   "name": "mathlib",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/plausible",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
-   "name": "plausible",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
-   "name": "LeanSearchClient",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890",
-   "name": "importGraph",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
-   "name": "proofwidgets",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.84",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c",
-   "name": "aesop",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/quote4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72",
-   "name": "Qq",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/batteries",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "2e16f91af2a97975e5d2fac906494cd6c17ba255",
-   "name": "batteries",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
-   "inherited": true,
-   "configFile": "lakefile.toml"}],
- "name": "MathlibDemo",
- "lakeDir": ".lake"}
+{
+  "version": "1.1.0",
+  "packagesDir": ".lake/packages",
+  "packages": [
+    {
+      "url": "https://github.com/leanprover-community/mathlib4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "d68c4dc09f5e000d3c968adae8def120a0758729",
+      "name": "mathlib",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": false,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/plausible",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
+      "name": "plausible",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/LeanSearchClient",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+      "name": "LeanSearchClient",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/import-graph",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890",
+      "name": "importGraph",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/ProofWidgets4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
+      "name": "proofwidgets",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v0.0.84",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/aesop",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c",
+      "name": "aesop",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/quote4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72",
+      "name": "Qq",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/batteries",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "2e16f91af2a97975e5d2fac906494cd6c17ba255",
+      "name": "batteries",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover/lean4-cli",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover",
+      "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
+      "name": "Cli",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.27.0-rc1",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    }
+  ],
+  "name": "MathlibDemo",
+  "lakeDir": ".lake"
+}

Projects/README.md

@@ -39,11 +39,9 @@ the file from `Projects/MyCoolProject/MyCoolProject/Demo1.lean`.
 
 You might want to look at the provided `MathlibDemo` project for comparison.
 
-
 **Important**: In order for lake to use any "leanOptions" specified in the projects lakefile, you must make sure there is a file `Projects/MyCoolProject/MyCoolProject.lean`
 where folder name and file name coincide.
 
-
 ## Creating Lean Projects with Mathlib
 
 To create a Lean project with a specific version and mathlib dependencies, you can use the `create_project.sh` script:
@@ -53,13 +51,15 @@ To create a Lean project with a specific version and mathlib dependencies, you c
 ```
 
 The version should be in the format of `v4.x.x` or `4.x.x`. For example:
+
 ```bash
 ./create_project.sh v4.13.0
 # or
 ./create_project.sh 4.13.0
 ```
 
 This will:
+
 1. Create a new Lean project in `Projects/<version>/`
 2. Configure mathlib dependencies
 3. Build the project with cache

Projects/Stable/lake-manifest.json

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

README.md

@@ -1,7 +1,6 @@
 [![GitHub license](https://img.shields.io/badge/License-Apache_2.0-blue.svg)](https://github.com/leanprover-community/lean4web/blob/main/LICENSE)
 [![(Runtime) Build and Test](https://github.com/leanprover-community/lean4web/actions/workflows/build.yml/badge.svg)](https://github.com/leanprover-community/lean4web/actions/workflows/build.yml)
 
-
 # Lean 4 Web
 
 This is a web version of Lean 4. There is a playground hosted at [live.lean-lang.org](https://live.lean-lang.org) and one at [lean.math.hhu.de](https://lean.math.hhu.de).
@@ -11,11 +10,11 @@ running on a web server, and not in the browser.
 
 ## Scope of lean4web
 
-* Provide a clean, minimalistic and easily accessible way to run some (smallish) Lean snippets
-* Provide a simple way to run [MWEs](https://leanprover-community.github.io/mwe.html) from [Zulip](https://leanprover.zulipchat.com) with the latest [Mathlib](https://github.com/leanprover-community/mathlib4) installed.
-* Provide a easy way to demonstrate some Lean code in talks/lecutres.
-* Provide a easy way for newcomers to doodle with Lean before installing it.
-* Provide a way to run some Lean code in a mobile context.
+- Provide a clean, minimalistic and easily accessible way to run some (smallish) Lean snippets
+- Provide a simple way to run [MWEs](https://leanprover-community.github.io/mwe.html) from [Zulip](https://leanprover.zulipchat.com) with the latest [Mathlib](https://github.com/leanprover-community/mathlib4) installed.
+- Provide a easy way to demonstrate some Lean code in talks/lecutres.
+- Provide a easy way for newcomers to doodle with Lean before installing it.
+- Provide a way to run some Lean code in a mobile context.
 
 Currently, serious Lean code development and larger projects are considered out-of-scope. For these, it might be more suitable to look at a setup using Codespaces or Gitpot.
 
@@ -27,7 +26,7 @@ If you experience any problems, or have feature requests, please open an issue h
 
 PRs fixing issues are very welcome!
 
-For new features, it's best to write an issue first to discuss them: For example, some functionality might be better implemented in [lean4monaco](https://github.com/hhu-adam/lean4monaco) which provides the key features and a discussion might be helpful to figure this out. 
+For new features, it's best to write an issue first to discuss them: For example, some functionality might be better implemented in [lean4monaco](https://github.com/hhu-adam/lean4monaco) which provides the key features and a discussion might be helpful to figure this out.
 
 ## Documentation
 

client/src/.prettierrc.json

@@ -0,0 +1,14 @@
+{
+  "printWidth": 100,
+  "tabWidth": 2,
+  "useTabs": false,
+  "semi": true,
+  "singleQuote": true,
+  "quoteProps": "as-needed",
+  "jsxSingleQuote": false,
+  "trailingComma": "all",
+  "bracketSpacing": true,
+  "bracketSameLine": false,
+  "arrowParens": "always",
+  "endOfLine": "lf"
+}