From 2eb2857a5f4e05555d99b03360ac2bef3b6ad692 Mon Sep 17 00:00:00 2001
From: Gavin Zhao <git@gzgz.dev>
Date: Thu, 15 Jan 2026 21:08:12 -0500
Subject: [PATCH] ci: add linter

---
 .github/workflows/lean_action_ci.yml |  1 +
 lake-manifest.json                   | 12 +++++++++++-
 lakefile.toml                        |  6 ++++++
 3 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index e984e9a..33a057d 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -16,3 +16,4 @@ jobs:
         with:
           build-args: "--iofail"
           test: true
+          lint: true
diff --git a/lake-manifest.json b/lake-manifest.json
index 2229924..5f52672 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,5 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5ba0380f2fb45c69448d80429ef6c22bf5973cfa",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.toml"}],
  "name": "VeIR",
  "lakeDir": ".lake"}
diff --git a/lakefile.toml b/lakefile.toml
index 1235804..a0c8af9 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -2,10 +2,16 @@ name = "VeIR"
 version = "0.1.0"
 defaultTargets = ["veir-opt"]
 testRunner = "Test"
+lintDriver = "batteries/runLinter"
 
 [leanOptions]
 experimental.module = true
 
+[[require]]
+name = "batteries"
+scope = "leanprover-community"
+rev = "main"
+
 [[lean_lib]]
 name = "Veir"
 root = "Veir"