feat: new setup to import projects (#95)

* wip

* mostly working

* cleanup

* hide hidden projects

* disable example API for non-lean files

* fix env vars

* fix build

* some adjustments from live deployment

* link

Author: joneugster

Projects/MathlibDemo/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "55aa437fb40b168305405301f173cf0cb2adfe94",
+   "rev": "be0a10d1f1d5c9434f47080fa0e2aa48b678ab3a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

Projects/MathlibDemo/build.sh Projects/MathlibDemo/leanweb-build.shProjects/MathlibDemo/build.sh renamed to Projects/MathlibDemo/leanweb-build.sh

@@ -0,0 +1,11 @@
+{
+  "name": "Latest Mathlib",
+  "default": true,
+  "hidden": false,
+  "examples": [
+    { "file": "MathlibDemo/Bijection.lean", "name": "Bijection" },
+    { "file": "MathlibDemo/Logic.lean", "name": "Logic" },
+    { "file": "MathlibDemo/Ring.lean", "name": "Ring" },
+    { "file": "MathlibDemo/Rational.lean", "name": "Rational" }
+  ]
+}

Projects/MathlibDemo/leanweb-config.json

@@ -0,0 +1,4 @@
+{
+  "name": "Stable Lean",
+  "hidden": false
+}

Projects/Stable/build.sh Projects/Stable/leanweb-build.shProjects/Stable/build.sh renamed to Projects/Stable/leanweb-build.sh

@@ -0,0 +1,7 @@
+import { LeanWebConfig } from "./src/api/config-types";
+
+export const lean4webConfig: LeanWebConfig = {
+  serverCountry: null,
+  contactDetails: null,
+  impressum: null,
+};

Projects/Stable/leanweb-config.json

@@ -17,7 +17,7 @@ import { Menu } from './navigation/Navigation'
 import { mobileAtom, settingsAtom } from './settings/settings-atoms'
 import { lightThemes } from './settings/settings-types'
 import { freshlyImportedCodeAtom } from './store/import-atoms'
-import { projectAtom } from './store/project-atoms'
+import { currentProjectAtom } from './store/project-atoms'
 import { screenWidthAtom } from './store/window-atoms'
 import { save } from './utils/SaveToFile'
 
@@ -35,7 +35,7 @@ function App() {
   const [settings] = useAtom(settingsAtom)
   const [mobile] = useAtom(mobileAtom)
   const [, setScreenWidth] = useAtom(screenWidthAtom)
-  const [project] = useAtom(projectAtom)
+  const [project] = useAtom(currentProjectAtom)
   const [code, setCode] = useAtom(codeAtom)
   const [freshlyImportedCode] = useAtom(freshlyImportedCodeAtom)
 
@@ -76,7 +76,7 @@ function App() {
       (window.location.protocol === 'https:' ? 'wss://' : 'ws://') +
       window.location.host +
       '/websocket/' +
-      project
+      project.folder
     console.log(`[Lean4web] Socket url is ${socketUrl}`)
     var _options: LeanMonacoOptions = {
       websocket: { url: socketUrl },
@@ -108,7 +108,7 @@ function App() {
 
   // Setting up the editor and infoview
   useEffect(() => {
-    if (project === undefined) return
+    if (!project) return
     console.debug('[Lean4web] Restarting editor')
     var _leanMonaco = new LeanMonaco()
     var leanMonacoEditor = new LeanMonacoEditor()
@@ -118,7 +118,7 @@ function App() {
       await _leanMonaco.start(options)
       await leanMonacoEditor.start(
         editorRef.current!,
-        path.join(project, `${project}.lean`),
+        path.join(project.folder, `${project.folder}.lean`),
         code ?? '',
       )
 

client/config.ts

@@ -1,4 +1,4 @@
-import lean4webConfig from '../config/config'
+import { lean4webConfig } from '../../config'
 import { Popup } from '../navigation/Popup'
 
 /** The popup with the privacy policy. */

client/src/App.tsx

@@ -1,4 +1,4 @@
-import lean4webConfig from '../config/config'
+import { lean4webConfig } from '../../config'
 import { Popup } from '../navigation/Popup'
 
 /** The popup with the privacy policy. */

client/src/Popups/Impressum.tsx

@@ -0,0 +1,16 @@
+import { JSX } from 'react'
+
+export type LeanWebConfig = {
+  /** Where the server is located. Use `null` to not display this information. */
+  serverCountry: string | null
+  /** Contact details of the server maintainer. Used in Privacy Policy and Impressum.
+   * Use `null` to not display this information.
+   * Note: This will be embedded inside a `<p>` tag! (example: `<>Hans Muster<br />hans@nowhere.com</>`)
+   */
+  contactDetails: JSX.Element | null
+  /** Additional legal information shown in impressum alongside the contact details.
+   * Use `null` to not display this information.
+   * (example: `<><p>vat number: 000</p><>`)
+   */
+  impressum: JSX.Element | null
+}