From eed2d390e27f9aeb5f18ecb19f23ccd11a8a1e1e Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Sun, 13 Oct 2024 22:06:50 -0400
Subject: [PATCH] Update lean-auto

---
 Duper/Tests/temp.lean | 1 +
 lake-manifest.json    | 4 ++--
 lakefile.lean         | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/Duper/Tests/temp.lean b/Duper/Tests/temp.lean
index bd2be0a..6d97f20 100644
--- a/Duper/Tests/temp.lean
+++ b/Duper/Tests/temp.lean
@@ -13,6 +13,7 @@ open Lean Auto
 @[rebind Auto.Native.solverFunc]
 def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
   let formulas ← Duper.autoLemmasToFormulas lemmas
+  let formulas := formulas.map (fun f => (f.1, f.2.1, f.2.2.1, f.2.2.2, none))
   Duper.runDuperPortfolioMode formulas .none
     { portfolioMode := true,
       portfolioInstance := none,
diff --git a/lake-manifest.json b/lake-manifest.json
index 2931a0e..b5554af 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2b6ed7d9f86d558d94b8d9036a637395163c4fa6",
+   "rev": "6cd81c96800dc2d2741499e931f350f069ca74c7",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "2b6ed7d9f86d558d94b8d9036a637395163c4fa6",
+   "inputRev": "6cd81c96800dc2d2741499e931f350f069ca74c7",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
diff --git a/lakefile.lean b/lakefile.lean
index 12b68d4..5a6007e 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"2b6ed7d9f86d558d94b8d9036a637395163c4fa6"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"6cd81c96800dc2d2741499e931f350f069ca74c7"
 require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.11.0"
 
 package Duper {