From 1e4571e56d6a405940dfd2231e861ab7261b43e0 Mon Sep 17 00:00:00 2001 From: joneugster Date: Mon, 20 Nov 2023 15:25:50 +0100 Subject: [PATCH] reimplement version display --- client/src/App.tsx | 4 +- client/src/Tools.tsx | 35 ++++++++ client/src/Version.tsx | 84 ------------------- server/LeanProject/LeanProject.lean | 1 - server/LeanProject/Webeditor.lean | 2 + server/LeanProject/Webeditor/Tools.lean | 1 + .../Webeditor/Tools/PackageVersion.lean | 50 +++++++++++ server/LeanProject/lake-manifest.json | 4 +- server/LeanProject/lakefile.lean | 4 +- server/copy_versions.sh | 14 ---- 10 files changed, 94 insertions(+), 105 deletions(-) create mode 100644 client/src/Tools.tsx delete mode 100644 client/src/Version.tsx delete mode 100644 server/LeanProject/LeanProject.lean create mode 100644 server/LeanProject/Webeditor.lean create mode 100644 server/LeanProject/Webeditor/Tools.lean create mode 100644 server/LeanProject/Webeditor/Tools/PackageVersion.lean delete mode 100755 server/copy_versions.sh diff --git a/client/src/App.tsx b/client/src/App.tsx index a24afd41..f793aaea 100644 --- a/client/src/App.tsx +++ b/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 = () => { Restart server - {/* */} + Save file diff --git a/client/src/Tools.tsx b/client/src/Tools.tsx new file mode 100644 index 00000000..672d50a5 --- /dev/null +++ b/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 ( + + + Tools: Version + + {open? +
+
+
+
+

Tools

+ + Add the following import to access the built-in Lean tools of the webeditor: +

import Webeditor.Tools

+ +

Versions

+ The following command prints the current Lean version plus all available packages + and their current commit sha: +

#package_version

+
+
: null} + + ) +} + +export default Tools diff --git a/client/src/Version.tsx b/client/src/Version.tsx deleted file mode 100644 index 49fea0ec..00000000 --- a/client/src/Version.tsx +++ /dev/null @@ -1,84 +0,0 @@ -import { faCodeMerge} from '@fortawesome/free-solid-svg-icons'; -import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'; -import { faArrowUpRightFromSquare } from '@fortawesome/free-solid-svg-icons' -import * as React from 'react' -import { useEffect } from 'react' - -/* -Display the versions of Lean and all packages. This is done by copying the -`lake-manifest.json` over to the client while building the server. The copied -JSON file is called `package_versions.json`. - -The Lean version is read from `lean-toolchain` and manually added to `package_versions.json`. -*/ - -var moment = require('moment-timezone'); -var tz = Intl.DateTimeFormat().resolvedOptions().timeZone; - -const Version: React.FC = () => { - const [open, setOpen] = React.useState(false); - const handleOpen = () => setOpen(true); - const handleClose = () => setOpen(false); - - const [packageVersions, setPackageVersions] = React.useState(null); - - // TODO: this is hacky - useEffect(() => { - try { - fetch('package_versions.json').then(function (r) {r.ok ? r.text().then(function (r) { - if (r) { - setPackageVersions(JSON.parse(r)) - } else { - setPackageVersions({time : "error" , packages : [] }) - } - - }) : setPackageVersions({time : "error" , packages : [] })}); - } catch { - console.log('rip, something with the versions file failed') - } - - }, []) - - const readVersions = (x) => { - let pac = x.git; - return ( - - {pac.name} - - -   - { (pac.name == "Lean") ? pac.rev : pac.rev.substring(0,7) } - - - ) - } - - return ( - - - Version - - {open? -
-
-
-
-

Version

-

- Lean and the available dependencies are updated automatically on a regular basis.
- Last update: { moment.unix(packageVersions.time).tz(tz).format("DD MMM. YYYY, HH:mm (z / Z)") } -

- - - - - - { packageVersions.packages.map(readVersions) } -
PackageCommit
-
-
: null} - - ) -} - -export default Version diff --git a/server/LeanProject/LeanProject.lean b/server/LeanProject/LeanProject.lean deleted file mode 100644 index 0b4be76b..00000000 --- a/server/LeanProject/LeanProject.lean +++ /dev/null @@ -1 +0,0 @@ -import Mathlib diff --git a/server/LeanProject/Webeditor.lean b/server/LeanProject/Webeditor.lean new file mode 100644 index 00000000..36ff3f3d --- /dev/null +++ b/server/LeanProject/Webeditor.lean @@ -0,0 +1,2 @@ +import Mathlib +import Webeditor.Tools diff --git a/server/LeanProject/Webeditor/Tools.lean b/server/LeanProject/Webeditor/Tools.lean new file mode 100644 index 00000000..1ad9d913 --- /dev/null +++ b/server/LeanProject/Webeditor/Tools.lean @@ -0,0 +1 @@ +import Webeditor.Tools.PackageVersion diff --git a/server/LeanProject/Webeditor/Tools/PackageVersion.lean b/server/LeanProject/Webeditor/Tools/PackageVersion.lean new file mode 100644 index 00000000..713e7056 --- /dev/null +++ b/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 diff --git a/server/LeanProject/lake-manifest.json b/server/LeanProject/lake-manifest.json index 9db3cdc5..497c09e7 100644 --- a/server/LeanProject/lake-manifest.json +++ b/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"} diff --git a/server/LeanProject/lakefile.lean b/server/LeanProject/lakefile.lean index 30c8abaa..b31aadab 100644 --- a/server/LeanProject/lakefile.lean +++ b/server/LeanProject/lakefile.lean @@ -1,7 +1,7 @@ import Lake open Lake DSL -package leanProject { +package webeditor { -- add package configuration options here } @@ -9,6 +9,6 @@ require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master" @[default_target] -lean_lib LeanProject { +lean_lib Webeditor { -- add library configuration options here } diff --git a/server/copy_versions.sh b/server/copy_versions.sh deleted file mode 100755 index 94b993e3..00000000 --- a/server/copy_versions.sh +++ /dev/null @@ -1,14 +0,0 @@ -#!/usr/bin/env sh - -# Operate in the directory where this file is located -cd $(dirname $0) - -# Copy relevant version info to the client to display Lean & mathlib version -# TODO: This is a bit hacky... -leanV=$( cat LeanProject/lean-toolchain | sed 's/.*://' ) -currDate=$( date +"%s" ) - -cat LeanProject/lake-manifest.json | jq --arg d "$currDate" '. |= . + {time: $d}' | jq --arg leanV "$leanV" '.packages |= [{git: {name: "Lean", url: "https://github.com/leanprover/lean4-nightly/", rev: $leanV}}] + .' > ../client/public/package_versions.json - -mkdir -p "../client/dist" -cp ../client/public/package_versions.json ../client/dist/package_versions.json