From 7bd6a98b186852fed547a5ec9aa32676ec857524 Mon Sep 17 00:00:00 2001
From: James Sully <sullyj3@gmail.com>
Date: Sat, 3 Aug 2024 14:38:21 +1000
Subject: [PATCH] Get git describe working in gh actions

---
 .github/workflows/ci.yml | 6 ++++++
 src/Main.lean            | 5 +++++
 src/Sand/Basic.lean      | 8 ++++++--
 3 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index fa3971c..8a5161d 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -12,8 +12,13 @@ jobs:
     steps:
       - name: Checkout code
         uses: actions/checkout@v4
+      - name: Git describe
+        id: ghd
+        uses: proudust/gh-describe@v2
       - name: Run Lean Action
         uses: leanprover/lean-action@v1
+        env:
+          GIT_DESCRIBE: ${{ steps.ghd.outputs.describe }}
         with:
           auto-config: "false"
           use-mathlib-cache: "false"
@@ -25,6 +30,7 @@ jobs:
           python-version: '3.x'
       - name: Run integration tests
         run: |
+          echo "Testing $(.lake/build/bin/sand version)"
           python -m pip install --upgrade pip
           pip install pytest
           pytest test_daemon.py
diff --git a/src/Main.lean b/src/Main.lean
index fc691a9..4ee4aa7 100644
--- a/src/Main.lean
+++ b/src/Main.lean
@@ -1,6 +1,11 @@
 import Sand
 
+def version : IO UInt32 := do
+  println! "Sand version {Sand.version}"
+  return 0
+
 def main (args : List String) : IO UInt32 := do
   match args with
+  | ("version" :: _) => version
   | ("daemon" :: rest) => SandDaemon.main rest
   | _                  => SandClient.main args
diff --git a/src/Sand/Basic.lean b/src/Sand/Basic.lean
index 945c348..d819c46 100644
--- a/src/Sand/Basic.lean
+++ b/src/Sand/Basic.lean
@@ -14,8 +14,12 @@ def Batteries.HashMap.values [BEq α] [Hashable α] (hashMap : HashMap α β) :
 namespace Sand
 
 elab "get_version" : term => do
-  let version ←
-    String.trimRight <$> IO.Process.run { cmd := "git", args := #["describe"] }
+  let version ← do
+    -- this is necessary in CI
+    if let some version ← IO.getEnv "GIT_DESCRIBE" then
+      pure version
+    else
+      String.trimRight <$> IO.Process.run { cmd := "git", args := #["describe"] }
   return .lit <| .strVal version
 
 def version : String := get_version