From 9ee49e00e227232aee7ec4f6720d1da2bc89db51 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Thu, 26 Dec 2024 21:57:39 +0530 Subject: [PATCH 1/6] chore: update nightly-testing-2024-12-23 (#908) WIP. integrating changes from #907 too - cc @tobiasgrosser: sorry i did not see #907 existed already when i started working on this --------- Co-authored-by: Siddharth Bhat Co-authored-by: Tobias Grosser --- SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean | 3 +-- lake-manifest.json | 6 +++--- lakefile.toml | 2 +- lean-toolchain | 2 +- 4 files changed, 6 insertions(+), 7 deletions(-) diff --git a/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean b/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean index 79d918eeb..1bb1bea14 100644 --- a/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean +++ b/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean @@ -20,8 +20,7 @@ open AutoStructs open Mathlib @[simp] theorem Language.mem_setOf_eq {x : List α} {p : List α → Prop} : - @Membership.mem (List α) (Language α) instMembershipListLanguage {y | p y} x = p x := by - rfl + @Membership.mem (List α) (Language α) Language.instMembershipList {y | p y} x = p x := rfl @[simp] theorem Language.trivial : x ∈ (⊤ : Language α) := by trivial diff --git a/lake-manifest.json b/lake-manifest.json index f0838b743..8060d2c2a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "63618639886f3bea1260812a0e5b81aebdc8cc60", + "rev": "ed546d89ba3b9fa2c93b3501b9f6aac3593c930d", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing-2024-12-22", + "inputRev": "nightly-testing-2024-12-23", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1a278069eda32a2dc0ce4d59eeb77d318373d10e", + "rev": "6b16a9378726331e9f4b1a044dbda82261b2cfef", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/lakefile.toml b/lakefile.toml index 2fc8eaf9c..71f519add 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,7 +4,7 @@ defaultTargets = ["SSA"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "nightly-testing-2024-12-22" +rev = "nightly-testing-2024-12-23" [[require]] name = "Cli" diff --git a/lean-toolchain b/lean-toolchain index ce85f8691..c0d8a978e 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-12-22 +leanprover/lean4:nightly-2024-12-23 From a17d9acfc56e77ca6263d37be80d9a07d87690fa Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Thu, 26 Dec 2024 19:24:30 +0100 Subject: [PATCH 2/6] chore: do not fail in case some test cases time out (#917) --- .github/workflows/performance.yml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/performance.yml b/.github/workflows/performance.yml index 7618b3513..90ae87ac0 100644 --- a/.github/workflows/performance.yml +++ b/.github/workflows/performance.yml @@ -45,9 +45,13 @@ jobs: lake -R build - name: Run LLVM + continue-on-error: true run: | (cd bv-evaluation; python3 ./compare-leansat-vs-bitwuzla-llvm-sym.py -j128) - echo "Symbolic" + + - name: Run LLVM Symbolic + continue-on-error: true + run: | (cd bv-evaluation; python3 ./compare-leansat-vs-bitwuzla-llvm.py -j128) - name: Run Alive Symbolic From d91f626d1801351bcfb96ccd704a1e7c61515aee Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Thu, 26 Dec 2024 22:11:19 +0100 Subject: [PATCH 3/6] chore: update to nightly-testing-2024-12-24 (#914) --- lake-manifest.json | 6 +++--- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 8060d2c2a..c47dfee4e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ed546d89ba3b9fa2c93b3501b9f6aac3593c930d", + "rev": "9a6b101b298066238b15e3fbd66618c2088cc693", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing-2024-12-23", + "inputRev": "nightly-testing-2024-12-24", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6b16a9378726331e9f4b1a044dbda82261b2cfef", + "rev": "03373e3b951d03e216837a5b14f28b5ab9664a98", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/lakefile.toml b/lakefile.toml index 71f519add..c4c99cf44 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,7 +4,7 @@ defaultTargets = ["SSA"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "nightly-testing-2024-12-23" +rev = "nightly-testing-2024-12-24" [[require]] name = "Cli" diff --git a/lean-toolchain b/lean-toolchain index c0d8a978e..6f7dca929 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-12-23 +leanprover/lean4:nightly-2024-12-24 From 7797db8c72834a52c226cc27c64c1b917c7cb9bd Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Thu, 26 Dec 2024 22:27:18 +0100 Subject: [PATCH 4/6] chore: update to nightly-testing-2024-12-25 (#915) --- lake-manifest.json | 8 ++++---- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index c47dfee4e..6a2b06f3d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9a6b101b298066238b15e3fbd66618c2088cc693", + "rev": "8157db740f7cbf298fb4839f6b1b81b03f76d44e", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing-2024-12-24", + "inputRev": "nightly-testing-2024-12-25", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", + "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "03373e3b951d03e216837a5b14f28b5ab9664a98", + "rev": "7f9e7a655e6602b674657a3be7eabcf84c905446", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/lakefile.toml b/lakefile.toml index c4c99cf44..6b61ec9ce 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,7 +4,7 @@ defaultTargets = ["SSA"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "nightly-testing-2024-12-24" +rev = "nightly-testing-2024-12-25" [[require]] name = "Cli" diff --git a/lean-toolchain b/lean-toolchain index 6f7dca929..62b3dc2fb 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-12-24 +leanprover/lean4:nightly-2024-12-25 From b34a6c9c83ab686ad222471169c55a76d8b301b5 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Thu, 26 Dec 2024 23:54:02 +0100 Subject: [PATCH 5/6] chore: update to nightly-testing-2024-12-26 (#916) --- lake-manifest.json | 6 +++--- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 6a2b06f3d..e81c4e02b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8157db740f7cbf298fb4839f6b1b81b03f76d44e", + "rev": "d97af69f33c3a73efddc6db118bf4ffdb0ff78cd", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing-2024-12-25", + "inputRev": "nightly-testing-2024-12-26", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7f9e7a655e6602b674657a3be7eabcf84c905446", + "rev": "181555dcc86ea0d9147988f6fec8c18061300868", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/lakefile.toml b/lakefile.toml index 6b61ec9ce..748f0b418 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,7 +4,7 @@ defaultTargets = ["SSA"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "nightly-testing-2024-12-25" +rev = "nightly-testing-2024-12-26" [[require]] name = "Cli" diff --git a/lean-toolchain b/lean-toolchain index 62b3dc2fb..d8b844b91 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-12-25 +leanprover/lean4:nightly-2024-12-26 From 0aef1c2ec851cbdb07e6f62db07f03aede5edeee Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 27 Dec 2024 00:23:37 +0100 Subject: [PATCH 6/6] chore: do not hide LLVM output when collecting data (#919) --- .github/workflows/performance.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/performance.yml b/.github/workflows/performance.yml index 90ae87ac0..aff22515a 100644 --- a/.github/workflows/performance.yml +++ b/.github/workflows/performance.yml @@ -76,7 +76,7 @@ jobs: - name: Compare LLVM run: | - (cd bv-evaluation; python3 ./collect-data-llvm.py > /dev/null) + (cd bv-evaluation; python3 ./collect-data-llvm.py) - name: Compare HDEl run: |