From b3452429793889750b027e132df31d365915eef5 Mon Sep 17 00:00:00 2001
From: Mathieu Fehr <mathieu.fehr@gmail.com>
Date: Sun, 18 Jan 2026 19:45:59 +0000
Subject: [PATCH 1/3] Add simple veir-opt tool

`veir-opt` now parses then prints MLIR files.
---
 Main.lean | 51 ++++++++++++++++++++-------------------------------
 1 file changed, 20 insertions(+), 31 deletions(-)

diff --git a/Main.lean b/Main.lean
index de9455f..e75b1dd 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,34 +1,23 @@
-import Veir
+import Veir.Parser.MlirParser
+import Veir.Printer
+import Veir.IR.Basic
 
-def count := 50_000
-
-def getCountFrom (c : Option String) :=
-  match c with
-  | none => count
-  | some s =>
-    match s.toNat? with
-    | none => count
-    | some n => n
-
-def getPCFrom (c : Option String) :=
-  match c with
-  | none => 100
-  | some s =>
-    match s.toNat? with
-    | none => 100
-    | some n => n
-
-def bench (f: IO Unit) (count : Nat) : IO Unit := do
-  let startTime ← IO.monoMsNow
-  f
-  let endTime ← IO.monoMsNow
-  let elapsedTime := endTime - startTime
-  IO.println s!"Elapsed time: {elapsedTime} miliseconds"
-  IO.println s!"ns per op : {(elapsedTime * 1000 * 1000) / count}"
+open Veir.Parser
+open Veir
 
 def main (args : List String) : IO Unit := do
-  IO.println s!"Buffed Benchmark ({args})"
-  let count := getCountFrom args[1]?
-  match args[0]? with
-  | some bench => Veir.Benchmarks.runBenchmark bench count (getPCFrom args[2]?)
-  | _ => IO.println "Please provide a benchmark name"
+  match args with
+  | [filename] =>
+    let fileContent ← IO.FS.readBinFile filename
+    let some (ctx, _) := IRContext.create | IO.println "Failed to create IR context"; return
+    match ParserState.fromInput fileContent with
+    | .ok parser =>
+      match (parseOp none).run (MlirParserState.fromContext ctx) parser with
+      | .ok (op, state, _) =>
+        IO.println "Parsed Operation:"
+        Veir.Printer.printOperation state.ctx op
+      | .error errMsg => IO.eprintln s!"Error parsing operation: {errMsg}"
+    | .error errMsg => IO.eprintln s!"Error reading file: {errMsg}"; return
+  | _ =>
+    IO.eprintln "Wrong number of arguments."
+    IO.eprintln "Usage: veir_parser <filename>"

From 21521ba5928911989797811502396ac969a4e7a8 Mon Sep 17 00:00:00 2001
From: Mathieu Fehr <mathieu.fehr@gmail.com>
Date: Mon, 19 Jan 2026 23:57:24 +0000
Subject: [PATCH 2/3] Split Main into VeirOpt and RunBenchmarks

---
 RunBenchmarks.lean        | 34 ++++++++++++++++++++++++++++++++++
 Main.lean => VeirOpt.lean |  0
 lakefile.toml             |  6 +++++-
 3 files changed, 39 insertions(+), 1 deletion(-)
 create mode 100644 RunBenchmarks.lean
 rename Main.lean => VeirOpt.lean (100%)

diff --git a/RunBenchmarks.lean b/RunBenchmarks.lean
new file mode 100644
index 0000000..de9455f
--- /dev/null
+++ b/RunBenchmarks.lean
@@ -0,0 +1,34 @@
+import Veir
+
+def count := 50_000
+
+def getCountFrom (c : Option String) :=
+  match c with
+  | none => count
+  | some s =>
+    match s.toNat? with
+    | none => count
+    | some n => n
+
+def getPCFrom (c : Option String) :=
+  match c with
+  | none => 100
+  | some s =>
+    match s.toNat? with
+    | none => 100
+    | some n => n
+
+def bench (f: IO Unit) (count : Nat) : IO Unit := do
+  let startTime ← IO.monoMsNow
+  f
+  let endTime ← IO.monoMsNow
+  let elapsedTime := endTime - startTime
+  IO.println s!"Elapsed time: {elapsedTime} miliseconds"
+  IO.println s!"ns per op : {(elapsedTime * 1000 * 1000) / count}"
+
+def main (args : List String) : IO Unit := do
+  IO.println s!"Buffed Benchmark ({args})"
+  let count := getCountFrom args[1]?
+  match args[0]? with
+  | some bench => Veir.Benchmarks.runBenchmark bench count (getPCFrom args[2]?)
+  | _ => IO.println "Please provide a benchmark name"
diff --git a/Main.lean b/VeirOpt.lean
similarity index 100%
rename from Main.lean
rename to VeirOpt.lean
diff --git a/lakefile.toml b/lakefile.toml
index 1235804..04d88ab 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -16,4 +16,8 @@ root = "Test"
 
 [[lean_exe]]
 name = "veir-opt"
-root = "Main"
+root = "VeirOpt"
+
+[[lean_exe]]
+name = "run-benchmarks"
+root = "RunBenchmarks"

From a11d7b202d96102ee01a7c402a9ffa1fc5036d16 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Tue, 20 Jan 2026 06:20:31 +0000
Subject: [PATCH 3/3] add 'run-benchmarks' and 'Veir' to default targets

---
 lakefile.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lakefile.toml b/lakefile.toml
index 04d88ab..2e47d5c 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,6 +1,6 @@
 name = "VeIR"
 version = "0.1.0"
-defaultTargets = ["veir-opt"]
+defaultTargets = ["veir-opt", "run-benchmarks", "Veir"]
 testRunner = "Test"
 
 [leanOptions]