feat: new setup to import projects

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/leanweb-config.json

@@ -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/Stable/leanweb-config.json

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

client/config.ts

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

client/src/App.tsx

@@ -17,12 +17,12 @@
 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'
 
 /** Returns true if the browser wants dark mode */
 function isBrowserDefaultDark() {
   return window.matchMedia('(prefers-color-scheme: dark)').matches
 }
 
@@ -35,7 +35,7 @@
   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 @@
       (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 @@
 
   // 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 @@
       await _leanMonaco.start(options)
       await leanMonacoEditor.start(
         editorRef.current!,
-        path.join(project, `${project}.lean`),
+        path.join(project.folder, `${project.folder}.lean`),
         code ?? '',
       )
 
@@ -207,7 +207,7 @@
       leanMonacoEditor.dispose()
       _leanMonaco.dispose()
     }
   }, [infoviewRef, editorRef, options, project, settings])
 
   /** Set editor content to the code loaded from the URL */
   useEffect(() => {

client/src/Popups/Impressum.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/PrivacyPolicy.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/api/config-types.ts

@@ -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
+}

client/src/api/project-types.ts

@@ -0,0 +1,28 @@
+/** An example can be any Lean file which belongs to the project.
+ * The editor just reads the file content, but it makes sense for maintainability
+ * that you ensure the Lean project actually builds the file. */
+export type LeanWebExample = {
+  /** File to load; relative path in `lean4web/Projects/<project_folder>/` */
+  file: string
+  /** Display name used in the `Examples` menu */
+  name: string
+}
+
+/** Configuration from a project's `leanweb-config.json` file. */
+export type LeanWebProjectConfig = {
+  /** Display name; shown in selection menu */
+  name: string
+  /** Hidden projects do not appear in the dropdown and are only accessible through the direct link */
+  hidden: boolean
+  /** The default project. There must be exactly one project marked as default */
+  default: boolean
+  /** A list of examples which are added under the menu `Examples` */
+  examples: LeanWebExample[]
+}
+
+/* A project */
+export type LeanWebProject = {
+  /* The folder name of the project. */
+  folder: string
+  config: LeanWebProjectConfig
+}

client/src/navigation/NavButton.tsx

@@ -7,19 +7,21 @@ export function NavButton({
   icon,
   iconElement,
   text,
+  title,
   onClick = () => {},
   href = undefined,
 }: {
   icon?: IconDefinition
   iconElement?: JSX.Element
   text: string
+  title?: string
   onClick?: MouseEventHandler<HTMLAnchorElement>
   href?: string
 }) {
   // note: it seems that we can just leave the `target="_blank"` and it has no
   // effect on links without a `href`. If not, add `if (href)` statement here...
   return (
-    <a className="nav-link" onClick={onClick} href={href!} target="_blank">
+    <a className="nav-link" title={title} onClick={onClick} href={href!} target="_blank">
       {iconElement ?? <FontAwesomeIcon icon={icon!} />}&nbsp;{text}
     </a>
   )

client/src/navigation/Navigation.tsx

@@ -18,8 +18,8 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { useAtom } from 'jotai'
 import { ChangeEvent, Dispatch, SetStateAction, useState } from 'react'
 
+import { lean4webConfig } from '../../config'
 import ZulipIcon from '../assets/zulip.svg'
-import lean4webConfig from '../config/config'
 import { codeAtom } from '../editor/code-atoms'
 import ImpressumPopup from '../Popups/Impressum'
 import LoadUrlPopup from '../Popups/LoadUrl'
@@ -29,7 +29,7 @@ import ToolsPopup from '../Popups/Tools'
 import { mobileAtom } from '../settings/settings-atoms'
 import { SettingsPopup } from '../settings/SettingsPopup'
 import { setImportUrlAndProjectAtom } from '../store/import-atoms'
-import { projectAtom } from '../store/project-atoms'
+import { currentProjectAtom, projectsAtom, visibleProjectsAtom } from '../store/project-atoms'
 import { save } from '../utils/SaveToFile'
 import { Dropdown } from './Dropdown'
 import { NavButton } from './NavButton'
@@ -57,6 +57,7 @@ function FlexibleMenu({
   setLoadZulipOpen: Dispatch<SetStateAction<boolean>>
 }) {
   const [, setImportUrlAndProject] = useAtom(setImportUrlAndProjectAtom)
+  const [{ data: projects }] = useAtom(projectsAtom)
   const loadFileFromDisk = (event: ChangeEvent<HTMLInputElement>) => {
     console.debug('Loading file from disk')
     const fileToLoad = event.target.files![0]
@@ -83,16 +84,17 @@ function FlexibleMenu({
           !isInDropdown && setOpenNav(false)
         }}
       >
-        {lean4webConfig.projects.map((proj) =>
-          proj.examples?.map((example) => (
+        {projects.map((it) =>
+          it.config.examples?.map((example) => (
             <NavButton
-              key={`${proj.name}-${example.name}`}
+              key={`${it.config.name}-${example.name}`}
               icon={faStar}
               text={example.name}
+              title={`${it.config.name}: ${example.name}`}
               onClick={() => {
                 setImportUrlAndProject({
-                  url: `${window.location.origin}/api/example/${proj.folder}/${example.file}`,
-                  project: proj.folder,
+                  url: `${window.location.origin}/api/example/${it.folder}/${example.file}`,
+                  project: it.folder,
                 })
                 setOpenExample(false)
               }}
@@ -153,7 +155,8 @@ export function Menu({
   codeMirror: boolean
   setCodeMirror: Dispatch<SetStateAction<boolean>>
 }) {
-  const [project, setProject] = useAtom(projectAtom)
+  const [visibleProjects] = useAtom(visibleProjectsAtom)
+  const [project, setProject] = useAtom(currentProjectAtom)
   const [code] = useAtom(codeAtom)
 
   // state for handling the dropdown menus
@@ -175,20 +178,23 @@ export function Menu({
 
   return (
     <div className="menu">
-      <select
-        name="leanVersion"
-        value={project}
-        onChange={(ev) => {
-          setProject(ev.target.value)
-          console.log(`set Lean project to: ${ev.target.value}`)
-        }}
-      >
-        {lean4webConfig.projects.map((proj) => (
-          <option key={proj.folder} value={proj.folder}>
-            {proj.name ?? proj.folder}
-          </option>
-        ))}
-      </select>
+      {project && (
+        <select
+          name="leanVersion"
+          value={project.folder}
+          onChange={(ev) => {
+            setProject(ev.target.value)
+            console.log(`set Lean project to: ${ev.target.value}`)
+          }}
+        >
+          {project.folder}
+          {visibleProjects.map((proj) => (
+            <option key={proj.folder} value={proj.folder}>
+              {proj.config.name}
+            </option>
+          ))}
+        </select>
+      )}
       {mobile && (
         <NavButton
           icon={faCode}
@@ -270,22 +276,24 @@ export function Menu({
           text="Lean community"
           href="https://leanprover-community.github.io/"
         />
-        <NavButton
-          icon={faArrowUpRightFromSquare}
-          text="Lean documentation"
-          href="https://leanprover.github.io/lean4/doc/"
-        />
+        <NavButton icon={faArrowUpRightFromSquare} text="Lean FRO" href="https://lean-lang.org" />
         <NavButton
           icon={faArrowUpRightFromSquare}
           text="GitHub"
-          href="https://github.com/hhu-adam/lean4web"
+          href="https://github.com/leanprover-community/lean4web"
         />
       </Dropdown>
       <PrivacyPopup open={privacyOpen} handleClose={() => setPrivacyOpen(false)} />
       {hasImpressum && (
         <ImpressumPopup open={impressumOpen} handleClose={() => setImpressumOpen(false)} />
       )}
-      <ToolsPopup open={toolsOpen} handleClose={() => setToolsOpen(false)} project={project} />
+      {project && (
+        <ToolsPopup
+          open={toolsOpen}
+          handleClose={() => setToolsOpen(false)}
+          project={project.folder}
+        />
+      )}
       <SettingsPopup
         open={settingsOpen}
         handleClose={() => setSettingsOpen(false)}