From 8dfd7fccfce64015f1fefed07d200afa3ef1a86d Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Fri, 5 Nov 2021 16:22:11 -0400
Subject: [PATCH] feat: use `lean --githash` for Lean version checking

---
 Lake/Cli.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/Lake/Cli.lean b/Lake/Cli.lean
index 936b37f008..cc81e1da27 100644
--- a/Lake/Cli.lean
+++ b/Lake/Cli.lean
@@ -219,13 +219,14 @@ def verifyLeanVersion : CliM PUnit := do
   let leanInstall ← getLeanInstall
   let out ← IO.Process.output {
     cmd := leanInstall.lean.toString,
-    args := #["--version"]
+    args := #["--githash"]
   }
   if out.exitCode == 0 then
-    unless out.stdout.drop 14 |>.startsWith uiLeanVersionString do
-      error s!"expected {uiLeanVersionString}, but got {out.stdout.trim}"
+    let githash := out.stdout.trim
+    unless githash == Lean.githash do
+      error s!"expected Lean commit {Lean.githash}, but got {githash}"
   else
-    error s!"running `lean --version` exited with code {out.exitCode}"
+    error s!"running `lean --githash` exited with code {out.exitCode}"
 
 /-- Output the detected installs and verify the Lean version. -/
 def verifyInstall : CliM PUnit := do