reimplement version display

client/src/App.tsx

@@ -10,7 +10,7 @@ const Editor = React.lazy(() => import('./Editor'))
 import { ReactComponent as Logo } from './assets/logo.svg'
 import { saveAs } from 'file-saver';
 import Settings from './Settings'
-import Version from './Version'
+import Tools from './Tools'
 import Examples from './Examples'
 import LoadingMenu from './LoadingMenu'
 import { config } from './config/config'
@@ -146,7 +146,7 @@ const App: React.FC = () => {
             <span className="nav-link" onClick={restart}>
               <FontAwesomeIcon icon={faArrowRotateRight} /> Restart server
             </span>
-            {/* <Version /> */}
+            <Tools />
             <span className="nav-link" onClick={save}>
               <FontAwesomeIcon icon={faDownload} /> Save file
             </span>

client/src/Tools.tsx

@@ -0,0 +1,35 @@
+import { faHammer } from '@fortawesome/free-solid-svg-icons';
+import { FontAwesomeIcon } from '@fortawesome/react-fontawesome';
+import * as React from 'react'
+
+const Tools: React.FC = () => {
+  const [open, setOpen] = React.useState(false);
+  const handleOpen = () => setOpen(true);
+  const handleClose = () => setOpen(false);
+
+  return (
+    <span>
+      <span className="nav-link" onClick={handleOpen}>
+        <FontAwesomeIcon icon={faHammer} /> Tools: Version
+      </span>
+      {open?
+        <div className="modal-wrapper">
+          <div className="modal-backdrop" onClick={handleClose} />
+          <div className="modal">
+            <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
+            <h2>Tools</h2>
+
+            Add the following import to access the built-in Lean tools of the webeditor:
+            <p><code>import Webeditor.Tools</code></p>
+
+            <h3>Versions</h3>
+            The following command prints the current Lean version plus all available packages
+            and their current commit sha:
+            <p><code>#package_version</code></p>
+          </div>
+        </div> : null}
+    </span>
+  )
+}
+
+export default Tools

server/LeanProject/Webeditor.lean

@@ -0,0 +1,2 @@
+import Mathlib
+import Webeditor.Tools

server/LeanProject/Webeditor/Tools.lean

@@ -0,0 +1 @@
+import Webeditor.Tools.PackageVersion

server/LeanProject/Webeditor/Tools/PackageVersion.lean

@@ -0,0 +1,50 @@
+import Lean
+import Lake.Load.Manifest
+
+/-! # Print packages
+
+This file contains a helper tool for the webeditor, `#package_version`, which
+prints the current lean version together with a list of packages and their current
+commit hashes.
+
+-/
+
+open Lean
+
+namespace String
+
+/-- Allows us to write `⟨s, 0, 7⟩` for a `Substring` instead of `⟨s, ⟨0⟩, ⟨7⟩⟩`. -/
+instance : OfNat String.Pos x := ⟨⟨x⟩⟩
+
+/-- A slice of a string. The index `start` is included `stop` excluded.
+Note that this copies the string. Use `Substring` to get a slice without copying. -/
+def slice (s : String) (start := 0) (stop := s.length) : String := Substring.toString ⟨s, ⟨start⟩, ⟨stop⟩⟩
+
+end String
+
+/-- Read the `lake-manifest.jsoin` -/
+def getPackageVersions : IO String := do
+
+  -- Get the Lean version
+  let out := [s!"Lean: v{Lean.versionString}"]
+
+  match (← Lake.Manifest.load? ⟨"lake-manifest.json"⟩) with
+  | none =>
+    let out := out.append ["(could not read lake-manifest.json!)"]
+    return "\n\n".intercalate out
+  | some manifest =>
+    let out := out.append <| Array.toList <| manifest.packages.map (fun p =>
+      match p with
+      | .path name _ _ _ _ =>
+        s!"{name}:\nlocal package"
+      | .git name _ _ _ url rev _ _ =>
+        let rev := rev.slice 0 7
+        s!"{name}:\n{rev} ({url}/commit/{rev})")
+    return "\n\n".intercalate out
+
+/-- Print the lean version and all available packages. -/
+elab "#package_version" : command => do
+  match getPackageVersions.run' () with
+| none => panic ""
+| some s =>
+  logInfo s

server/LeanProject/lake-manifest.json

@@ -49,11 +49,11 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "cf21ac04014fcbc2d8c5954e4c869f0b014e0793",
+   "rev": "1a0131642c3b466586c8a9045d5e2c3c24672b19",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"}],
- "name": "leanProject",
+ "name": "webeditor",
  "lakeDir": ".lake"}

server/LeanProject/lakefile.lean

@@ -1,14 +1,14 @@
 import Lake
 open Lake DSL
 
-package leanProject {
+package webeditor {
   -- add package configuration options here
 }
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4"@"master"
 
 @[default_target]
-lean_lib LeanProject {
+lean_lib Webeditor {
   -- add library configuration options here
 }