chore: update toolchain to nightly-2024-08-02 (#57)

### Description: Update the toolchain to the latest nightly used by LeanSAT. This should include a fix for a memory leak we encountered with symbolic evaluation. ### Testing: `make all` succeeds locally. I've not ran conformance testing, since I've not made any significant changes to the code itself. ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. Co-authored-by: Shilpi Goel <[email protected]>
leanprover · Aug 5, 2024 · 7d9c50e · 7d9c50e
1 parent e4a289d
commit 7d9c50e
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 5 deletions.
diff --git a/Arm/Map.lean b/Arm/Map.lean
@@ -137,11 +137,10 @@ def Map.size (m : Map α β) : Nat :=
           -- leanprover/lean4:nightly-2024-02-24, but not in
           -- leanprover/lean4:nightly-2024-03-01.
           exact Nat.lt_succ_of_le this
-  next he => simp [he] at h; simp [h] at ih; simp;
+  next he => simp [he] at h; simpa [h] using ih
           -- (FIXME) This could be discharged by omega in
           -- leanprover/lean4:nightly-2024-02-24, but not in
           -- leanprover/lean4:nightly-2024-03-01.
-             exact Nat.succ_lt_succ ih
 
 -------------------------------------------------------------------------------
 

diff --git a/Tests/ELFParser/SymbolContents.lean b/Tests/ELFParser/SymbolContents.lean
@@ -8,6 +8,7 @@ def getELFFile (elfFile : System.FilePath) : IO RawELFFile := do
   | .error warn => throw (IO.userError warn)
   | .ok elffile => return elffile
 
+open RawELFFile (symbolNameByLinkAndOffset) in
 /- Get the name and symbol table entry of the `symidx`-th symbol, given the
 symbol table's section header `shte` and section `sec`. -/
 def getSymbolTableEntryInSection

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9906580a44cd2334f385abcf4db6787efdc39bd1",
+   "rev": "f48d7ffe08ed9e1c30bb1698604eab206eeea4b0",
    "name": "LeanSAT",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "aaaddfb0985ebcb91770b65d4347160b1a1435c6",
+   "rev": "fe0f8de78184002b0f9ec7271f2e80280b74776e",
    "name": "ELFSage",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-07-25
+leanprover/lean4:nightly-2024-08-02
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2024-07-25
		leanprover/lean4:nightly-2024-08-02