Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: bump Lean to v4.9.0 #119

Merged
merged 5 commits into from
Jul 8, 2024
Merged

chore: bump Lean to v4.9.0 #119

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7c078b3
bump Lean to v4.9.0
joewatt95 Jul 6, 2024
10f0a80
Fix compilation of Smt.Real
joewatt95 Jul 6, 2024
18e5094
Fix expected outputs of most test cases
joewatt95 Jul 6, 2024
23723c1
import Real.Star instead of Real.Basic
joewatt95 Jul 6, 2024
dff5fb8
Revert import Real.Star -> Real.Basic, update test case to reflect fa…
joewatt95 Jul 7, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Smt/Data/Sexp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,9 +83,9 @@ partial def parseOneAux : List Substring → Except ParseError (Sexp × List Sub
return (atom tk.toString, tks)
| [] => throw <| .incomplete "expected a token, got none"

partial def parseManyAux :=
partial def parseManyAux : List Substring → Except ParseError (Array Sexp × List Substring) :=
abdoo8080 marked this conversation as resolved.
Show resolved Hide resolved
go #[]
where go (stk : Array Sexp) : List Substring → Except ParseError (Array Sexp × List Substring)
where go (stk : Array Sexp)
| tk :: tks => do
if tk.front == ')' then .ok (stk, tk :: tks)
else
Expand Down
3 changes: 2 additions & 1 deletion Smt/Reconstruct/Real/Polynorm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Abdalrhman Mohamed
-/

import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Star
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This change is needed as Real.Basic as per 4.8.0 has been split up to Real.Basic and Real.Star as per 4.9.0. Reverting this results in the following error when tests are run:

Test/linarith.lean:146:2: error: [arithPolyNorm]: could not prove x - y = -x + y

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the error above the only one caused by the version change? If so, then let's keep import Mathlib.Data.Real.Basic. This error message is an instance of a bigger issue that will be resolved with once cvc5/#10911 is merged.

Copy link
Contributor Author

@joewatt95 joewatt95 Jul 7, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yep, this is the only failing test case caused by the version change. As per your suggestion, I have in dff5fb8 reverted import Mathlib.Data.Real.Star to import Mathlib.Data.Real.Basic, and updated the aforementioned test case to account for that error.

Also, thank you for mentioning the related cvc5 issue. I found this test case breakage to be rather puzzling, and suspected that there may be something deeper going on here.

import Mathlib.Tactic.Ring.RingNF
abdoo8080 marked this conversation as resolved.
Show resolved Hide resolved

namespace Smt.Reconstruct.Real

Expand Down
2 changes: 1 addition & 1 deletion Test/BitVec/Shift.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ Test/BitVec/Shift.lean:5:8: warning: declaration uses 'sorry'
goal: x ++ y = zeroExtend 6 x <<< 3#2 ||| zeroExtend 6 y

query:
(declare-const y (_ BitVec 3))
(declare-const x (_ BitVec 3))
(declare-const y (_ BitVec 3))
(assert (distinct (concat x y) (bvor (bvshl ((_ zero_extend 3) x) #b11) ((_ zero_extend 3) y))))
(check-sat)
Test/BitVec/Shift.lean:10:8: warning: declaration uses 'sorry'
8 changes: 4 additions & 4 deletions Test/Int/Binders.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
goal: curryAdd a b = curryAdd b a

query:
(define-fun curryAdd (([email protected]._hyg.3 Int) ([email protected]._hyg.5 Int)) Int (+ [email protected]._hyg.3 [email protected]._hyg.5))
(define-fun curryAdd (([email protected]._hyg.4 Int) ([email protected]._hyg.6 Int)) Int (+ [email protected]._hyg.4 [email protected]._hyg.6))
(declare-const b Int)
(declare-const a Int)
(assert (distinct (curryAdd a b) (curryAdd b a)))
Expand All @@ -10,7 +10,7 @@ Test/Int/Binders.lean:5:0: warning: declaration uses 'sorry'
goal: partCurryAdd a b = partCurryAdd b a

query:
(define-fun partCurryAdd ((a Int) ([email protected]._hyg.33 Int)) Int (+ a [email protected]._hyg.33))
(define-fun partCurryAdd ((a Int) ([email protected]._hyg.36 Int)) Int (+ a [email protected]._hyg.36))
(declare-const b Int)
(declare-const a Int)
(assert (distinct (partCurryAdd a b) (partCurryAdd b a)))
Expand All @@ -19,7 +19,7 @@ Test/Int/Binders.lean:11:0: warning: declaration uses 'sorry'
goal: partCurryAdd' a b = partCurryAdd' b a

query:
(define-fun |partCurryAdd'| ((a Int) ([email protected]._hyg.2347 Int)) Int (+ a [email protected]._hyg.2347))
(define-fun |partCurryAdd'| ((a Int) ([email protected]._hyg.2495 Int)) Int (+ a [email protected]._hyg.2495))
(declare-const b Int)
(declare-const a Int)
(assert (distinct (+ a b) (+ b a)))
Expand All @@ -29,8 +29,8 @@ goal: mismatchNamesAdd a b = mismatchNamesAdd b a

query:
(define-fun mismatchNamesAdd ((a Int) (b Int)) Int (+ a b))
(declare-const a Int)
(declare-const b Int)
(declare-const a Int)
(assert (distinct (mismatchNamesAdd a b) (mismatchNamesAdd b a)))
(check-sat)
Test/Int/Binders.lean:25:0: warning: declaration uses 'sorry'
2 changes: 1 addition & 1 deletion Test/Int/Let.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ goal: z 3 = 10

query:
(declare-fun f (Int) Int)
(define-fun z (([email protected]._hyg.295 Int)) Int (f 10))
(define-fun z (([email protected]._hyg.300 Int)) Int (f 10))
(assert (= (f 10) 10))
(assert (distinct (z 3) 10))
(check-sat)
2 changes: 1 addition & 1 deletion Test/Nat/Cong.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ goal: x = y → f x = f y
query:
(define-sort Nat () Int)
(declare-fun f (Nat) Nat)
(assert (forall ((_uniq.1521 Nat)) (=> (>= _uniq.1521 0) (>= (f _uniq.1521) 0))))
(assert (forall ((_uniq.1520 Nat)) (=> (>= _uniq.1520 0) (>= (f _uniq.1520) 0))))
(declare-const x Nat)
(assert (>= x 0))
(declare-const y Nat)
Expand Down
4 changes: 2 additions & 2 deletions Test/Nat/Sum'.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Test/Nat/Sum'.lean:7:12: error: tactic 'assumption' failed
case zero.a
_uniq✝¹¹⁶⁰³⁻⁰ :
_uniq✝⁹⁹³⁹⁻⁰ :
¬((∀ (n : Int), sum n = if n = 0 then 0 else n + sum (if 1 ≤ n then n - 1 else 0)) ∧
(∀ («_uniq.4976» : Int), «_uniq.4976» ≥ 0 → sum «_uniq.4976» ≥ 0) ∧ Smt.Reconstruct.Builtin.distinct [sum 0, 0])
⊢ ¬Smt.Reconstruct.andN' [Nat → Nat] ¬sum 0 = 0 * (0 + 1) / 2
Expand All @@ -11,7 +11,7 @@ query:
(declare-const n Nat)
(assert (>= n 0))
(define-fun-rec sum ((n Nat)) Nat (ite (= n 0) 0 (+ n (sum (ite (<= 1 n) (- n 1) 0)))))
(assert (forall ((_uniq.13678 Nat)) (=> (>= _uniq.13678 0) (>= (sum _uniq.13678) 0))))
(assert (forall ((_uniq.12014 Nat)) (=> (>= _uniq.12014 0) (>= (sum _uniq.12014) 0))))
(assert (= (sum n) (div (* n (+ n 1)) 2)))
(assert (distinct (sum (+ n 1)) (div (* (+ n 1) (+ (+ n 1) 1)) 2)))
(check-sat)
2 changes: 2 additions & 0 deletions Test/Real/Density.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,3 +6,5 @@ query:
(assert (not (=> (< x z) (exists ((y Real)) (and (< x y) (< y z))))))
(check-sat)
Test/Real/Density.lean:4:8: warning: declaration uses 'sorry'
Test/Real/Density.lean:5:2: warning: 'smt_show' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
2 changes: 2 additions & 0 deletions Test/Real/Inverse.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,5 @@ query:
(assert (not (=> (distinct x 0.0) (exists ((y Real)) (= (* x y) 1.0)))))
(check-sat)
Test/Real/Inverse.lean:4:8: warning: declaration uses 'sorry'
Test/Real/Inverse.lean:5:2: warning: 'smt_show' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
18 changes: 9 additions & 9 deletions lake-manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
{"version": 7,
{"version": "1.0.0",
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/abdoo8080/lean-cvc5.git",
Expand All @@ -13,7 +13,7 @@
{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"rev": "551ff2d7dffd7af914cdbd01abbd449fe3e3d428",
"rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -22,7 +22,7 @@
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
"rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
"rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
Expand All @@ -31,7 +31,7 @@
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"rev": "53ba96ad7666d4a2515292974631629b5ea5dfee",
"rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
Expand All @@ -40,10 +40,10 @@
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
"rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
"rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "v0.0.36",
"inputRev": "v0.0.38",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
Expand All @@ -58,7 +58,7 @@
{"url": "https://github.com/leanprover-community/import-graph.git",
"type": "git",
"subDir": null,
"rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404",
"rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -67,10 +67,10 @@
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"rev": "b5eba595428809e96f3ed113bc7ba776c5f801ac",
"rev": "f0957a7575317490107578ebaee9efaf8e62a4ab",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.8.0",
"inputRev": "v4.9.0",
"inherited": false,
"configFile": "lakefile.lean"}],
"name": "smt",
Expand Down
2 changes: 1 addition & 1 deletion lakefile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ require cvc5 from
git "https://github.com/abdoo8080/lean-cvc5.git" @ "main"

require mathlib from
git "https://github.com/leanprover-community/mathlib4.git" @ "v4.8.0"
git "https://github.com/leanprover-community/mathlib4.git" @ "v4.9.0"

def libcpp : String :=
if System.Platform.isWindows then "libstdc++-6.dll"
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.8.0
leanprover/lean4:v4.9.0