feat: add command to verify Lean version

Lake/Cli.lean

@@ -42,6 +42,7 @@ def cli : (cmd : String) → (lakeArgs pkgArgs : List String) → IO Unit
 | "build-bin",    [],       pkgArgs => do buildBin (← getCwdPkg pkgArgs)
 | "clean",        [],       pkgArgs => do (← getCwdPkg pkgArgs).clean
 | "help",         [cmd],    _       => IO.println <| help cmd
+| "self-check",   [],       _       => verifyLeanVersion
 | _,              _,        _       => throw <| IO.userError usage
 
 private def splitCmdlineArgsCore : List String → List String × List String

Lake/LeanVersion.lean

@@ -12,16 +12,28 @@ def origin := "leanprover/lean4"
 
 def leanVersionString :=
   if Lean.version.isRelease then
-      s!"{origin}:{leanVersionStringCore}"
+    s!"{origin}:{leanVersionStringCore}"
   else if Lean.version.specialDesc ≠ "" then
-      s!"{origin}:{Lean.version.specialDesc}"
+    s!"{origin}:{Lean.version.specialDesc}"
   else
-      s!"{origin}:master"
+    s!"{origin}:master"
 
 def uiLeanVersionString :=
 if Lean.version.isRelease then
-    leanVersionStringCore
+  leanVersionStringCore
 else if Lean.version.specialDesc ≠ "" then
-    Lean.version.specialDesc
+  s!"{leanVersionStringCore}-{Lean.version.specialDesc}"
 else
-    s!"master ({leanVersionStringCore})"
+  s!"master ({leanVersionStringCore})"
+
+def verifyLeanVersion : IO PUnit := do
+  let out ← IO.Process.output {
+    cmd := "lean",
+    args := #["--version"]
+  }
+  if out.exitCode == 0 then
+    unless out.stdout.drop 14 |>.startsWith uiLeanVersionString do
+      throw <| IO.userError <|
+        s!"expected {uiLeanVersionString}, but got {out.stdout.trim}"
+  else
+    throw <| IO.userError <| "missing lean!"

examples/test.sh

@@ -1,3 +1,6 @@
+echo 'verifying lake'
+../build/bin/lake self-check
+
 echo 'testing init'
 cd init
 ./test.sh
@@ -32,6 +35,7 @@ echo "testing bootstrap"
 cd bootstrap
 ./test.sh
 cd ..
+echo "testing bootstrapped hello"
 cd hello
 ./bootstrap-test.sh
 cd ..