From 81a84d21de80063ad2adbca133b8ae01a5b65c8a Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Tue, 17 Aug 2021 11:24:32 -0400
Subject: [PATCH] feat: add command to verify Lean version

---
 Lake/Cli.lean         |  1 +
 Lake/LeanVersion.lean | 24 ++++++++++++++++++------
 examples/test.sh      |  4 ++++
 3 files changed, 23 insertions(+), 6 deletions(-)

diff --git a/Lake/Cli.lean b/Lake/Cli.lean
index 5e3ca32988..6ec82ea9ae 100644
--- a/Lake/Cli.lean
+++ b/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
diff --git a/Lake/LeanVersion.lean b/Lake/LeanVersion.lean
index b8dd8df778..de5633a10b 100644
--- a/Lake/LeanVersion.lean
+++ b/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!"
diff --git a/examples/test.sh b/examples/test.sh
index dfcedaae58..1e12506b49 100644
--- a/examples/test.sh
+++ b/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 ..