Get git describe working in gh actions

.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

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

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