Skip to content

Commit ac30f27

Browse files
dranovdranov
authored
Merge pull request #104 from verse-lab/bump-v4.20.0
chore: bump to Lean v4.20.0
2 parents 2c7e570 + 2bade82 commit ac30f27

File tree

8 files changed

+42
-41
lines changed

8 files changed

+42
-41
lines changed

‎Examples/SuzukiKasami/SuzukiKasamiInts.lean‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,6 @@ type node
99
notation "seq_t" => Nat
1010
immutable individual init_node : node
1111

12-
notation (priority := high) t₁ "+" t₂ => Nat.add t₁ t₂
13-
1412
@[actSimp, invSimp] abbrev next : seq_t → seq_t → Prop := λ x y => (x + 1) = y
1513

1614

@@ -124,7 +122,6 @@ sat trace {
124122
exit
125123
} by bmc_sat
126124

127-
128125
unsat trace {
129126
enter
130127
enter

‎Test/SautoSyntax.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
import Veil
2+
3+
#guard_msgs(drop warning) in
4+
theorem foo : ∀ (p q : Prop), p → (p → q) → q := by intro p q hp hpq; sauto [hp, hpq]
5+
6+
set_option veil.smt.reconstructProofs true
7+
#guard_msgs in
8+
theorem foo_recon : ∀ (p q : Prop), p → (p → q) → q := by intro p q hp hpq; sauto [hp, hpq]

‎Veil/SMT/Main.lean‎

Lines changed: 11 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -15,22 +15,15 @@ import Veil.SMT.Model
1515
namespace Veil.SMT
1616

1717
-- /-- Our own version of the `smt` & `auto` tactics. -/
18-
syntax (name := sauto) "sauto" Smt.Tactic.smtHints Smt.Tactic.smtTimeout : tactic
18+
syntax (name := sauto) "sauto" Smt.Tactic.smtHints : tactic
1919

2020
open Lean Elab Tactic
2121

2222
/-- Converts `smtHints` into those understood by `lean-auto`. -/
2323
def parseAutoHints : TSyntax `smtHints → TacticM (TSyntax `Auto.hints)
24-
| `(Smt.Tactic.smtHints| [ $[$hs],* ]) => `(Auto.hints| [$[$hs:term],*])
24+
| `(Smt.Tactic.smtHints| [ $[$hs:term],* ]) => `(Auto.hints| [$[$hs:term],*])
2525
| `(Smt.Tactic.smtHints| ) => `(Auto.hints| [])
26-
| _ => throwUnsupportedSyntax
27-
28-
/- We use our own `parseTimeout` because the one in `lean-smt` has a
29-
hard-coded `5` as default if no timeout is specified. -/
30-
def parseTimeout : TSyntax `smtTimeout → CoreM Nat
31-
| `(Smt.Tactic.smtTimeout| (timeout := $n)) => return n.getNat
32-
| `(Smt.Tactic.smtTimeout| ) => return (veil.smt.timeout.get (← getOptions))
33-
| _ => throwUnsupportedSyntax
26+
| _ => do throwError s!"Failure in parseAutoHints on {← getRef}"
3427

3528
private def solverStr (solver : Option SmtSolver := none) : String :=
3629
match solver with
@@ -45,21 +38,25 @@ def unknownGoalStr (solver : Option SmtSolver := none) : String := s!"{solverStr
4538
def failureGoalStr (solver : Option SmtSolver := none) : String := s!"{solverStr solver}solver invocation failed"
4639

4740
@[tactic sauto] def elabSauto : Tactic := fun stx => withMainContext do
41+
let hints : TSyntax `smtHints := ⟨stx[1]⟩
4842
let mv ← Tactic.getMainGoal
49-
let withTimeout ← parseTimeout ⟨stx[2]⟩
43+
let withTimeout := veil.smt.timeout.get (← getOptions)
5044
-- If the user wants proof reconstruction, we simply call the `smt`
5145
-- tactic provided by `lean-smt`.
5246
let opts ← getOptions
5347
if veil.smt.reconstructProofs.get opts then
5448
let chosenTranslator := veil.smt.translator.get opts
5549
-- if chosenTranslator != .leanSmt then
5650
-- logInfo s!"Proof reconstruction is only supported with `lean-smt`, but `veil.smt.translator = {chosenTranslator}`. Falling back to `lean-smt`."
57-
Smt.Tactic.evalSmt stx
51+
let hints : TSyntax ``Smt.Tactic.smtHints := ⟨stx[1]⟩
52+
let smtSyntax ← `(tactic| smt $(hints):smtHints)
53+
trace[veil.smt] s!"proof reconstruction is on, so evaluating {smtSyntax}"
54+
Smt.Tactic.evalSmt smtSyntax
5855
else
5956
let cmdString := fun (translator : SmtTranslator) => do
6057
match translator with
61-
| .leanAuto => Veil.SMT.prepareLeanAutoQuery mv (← Veil.SMT.parseAutoHints ⟨stx[1]⟩)
62-
| .leanSmt => Veil.SMT.prepareLeanSmtQuery mv (← Smt.Tactic.parseHints ⟨stx[1]⟩)
58+
| .leanAuto => Veil.SMT.prepareLeanAutoQuery mv (← Veil.SMT.parseAutoHints hints)
59+
| .leanSmt => Veil.SMT.prepareLeanSmtQuery mv (← Smt.Tactic.elabHints hints)
6360
-- Due to [ufmg-smite#126](https://github.com/ufmg-smite/lean-smt/issues/126),
6461
-- we first use `lean-auto` to generate the query, and call `lean-smt` only
6562
-- if the query is satisfiable and we want to print a model,

‎Veil/Tactic/Main.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -415,7 +415,7 @@ where
415415
let mv ← Tactic.getMainGoal
416416
let idents ← getPropsInContext
417417
let hints ← `(Smt.Tactic.smtHints|[$[$idents:ident],*])
418-
let hs ← Smt.Tactic.parseHints ⟨hints⟩
418+
let hs ← Smt.Tactic.elabHints ⟨hints⟩
419419
let withTimeout := veil.smt.timeout.get opts
420420
-- IMPORTANT: `prepareLeanSmtQuery` (in `Smt.prepareSmtQuery`) negates
421421
-- the goal (it's designed for validity checking), so we negate it here

‎Veil/Util/SMT.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ def getQueryForGoal : TacticM String := withMainContext do
4646
let cmdString ←
4747
match translatorToUse with
4848
| .leanAuto => Veil.SMT.prepareLeanAutoQuery mv (← Veil.SMT.parseAutoHints ⟨stx[1]⟩)
49-
| .leanSmt => Veil.SMT.prepareLeanSmtQuery mv (← Smt.Tactic.parseHints ⟨stx[1]⟩)
49+
| .leanSmt => Veil.SMT.prepareLeanSmtQuery mv (← Smt.Tactic.elabHints ⟨stx[1]⟩)
5050
return cmdString
5151

5252
open Lean Elab Command Term Meta Tactic

‎lake-manifest.json‎

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -5,47 +5,47 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "de301cb5f7037073a48f055e284b6ee0ea39e1b4",
8+
"rev": "69860d889d74e90820fdb632457cc15bc8924e11",
99
"name": "smt",
1010
"manifestFile": "lake-manifest.json",
11-
"inputRev": "bump-v4.20.0-rc3",
11+
"inputRev": "v4.20.0",
1212
"inherited": false,
1313
"configFile": "lakefile.lean"},
14-
{"url": "https://github.com/dranov/lean-auto.git",
14+
{"url": "https://github.com/leanprover-community/lean-auto.git",
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "",
18-
"rev": "9f7714ebb2c2f6965921c9e53f8db702bf147dc1",
18+
"rev": "ec89836a79a3266ebd840fb0df59ca4c972a4c25",
1919
"name": "auto",
2020
"manifestFile": "lake-manifest.json",
21-
"inputRev": "bump-v4.20.0-rc3",
21+
"inputRev": "ec89836a79a3266ebd840fb0df59ca4c972a4c25",
2222
"inherited": false,
2323
"configFile": "lakefile.lean"},
2424
{"url": "https://github.com/leanprover-community/mathlib4.git",
2525
"type": "git",
2626
"subDir": null,
2727
"scope": "",
28-
"rev": "1755c0ff6d14a8b7818003c6f277a4410c2683bd",
28+
"rev": "c211948581bde9846a99e32d97a03f0d5307c31e",
2929
"name": "mathlib",
3030
"manifestFile": "lake-manifest.json",
31-
"inputRev": "1755c0ff6d14a8b7818003c6f277a4410c2683bd",
31+
"inputRev": "v4.20.0",
3232
"inherited": true,
3333
"configFile": "lakefile.lean"},
3434
{"url": "https://github.com/dranov/lean-cvc5.git",
3535
"type": "git",
3636
"subDir": null,
3737
"scope": "",
38-
"rev": "d1c21185af4d577e78b90dd4a69a16a3ee11f822",
38+
"rev": "f2e89994c90db3fc1546559d016054e7b54834b3",
3939
"name": "cvc5",
4040
"manifestFile": "lake-manifest.json",
41-
"inputRev": "v4.20.0-rc3-unofficial",
41+
"inputRev": "v4.20.0",
4242
"inherited": true,
4343
"configFile": "lakefile.lean"},
4444
{"url": "https://github.com/leanprover-community/plausible",
4545
"type": "git",
4646
"subDir": null,
4747
"scope": "leanprover-community",
48-
"rev": "304c5e2f490d546134c06bf8919e13b175272084",
48+
"rev": "2ac43674e92a695e96caac19f4002b25434636da",
4949
"name": "plausible",
5050
"manifestFile": "lake-manifest.json",
5151
"inputRev": "main",
@@ -55,7 +55,7 @@
5555
"type": "git",
5656
"subDir": null,
5757
"scope": "leanprover-community",
58-
"rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c",
58+
"rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
5959
"name": "LeanSearchClient",
6060
"manifestFile": "lake-manifest.json",
6161
"inputRev": "main",
@@ -65,7 +65,7 @@
6565
"type": "git",
6666
"subDir": null,
6767
"scope": "leanprover-community",
68-
"rev": "f5e58ef1f58fc0cbd92296d18951f45216309e48",
68+
"rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d",
6969
"name": "importGraph",
7070
"manifestFile": "lake-manifest.json",
7171
"inputRev": "main",
@@ -75,17 +75,17 @@
7575
"type": "git",
7676
"subDir": null,
7777
"scope": "leanprover-community",
78-
"rev": "632ca63a94f47dbd5694cac3fd991354b82b8f7a",
78+
"rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306",
7979
"name": "proofwidgets",
8080
"manifestFile": "lake-manifest.json",
81-
"inputRev": "v0.0.59",
81+
"inputRev": "v0.0.60",
8282
"inherited": true,
8383
"configFile": "lakefile.lean"},
8484
{"url": "https://github.com/leanprover-community/aesop",
8585
"type": "git",
8686
"subDir": null,
8787
"scope": "leanprover-community",
88-
"rev": "9264d548cf1ccf0ba454b82f931f44c37c299fc1",
88+
"rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a",
8989
"name": "aesop",
9090
"manifestFile": "lake-manifest.json",
9191
"inputRev": "master",
@@ -95,7 +95,7 @@
9595
"type": "git",
9696
"subDir": null,
9797
"scope": "leanprover-community",
98-
"rev": "36ce5e17d6ab3c881e0cb1bb727982507e708130",
98+
"rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a",
9999
"name": "Qq",
100100
"manifestFile": "lake-manifest.json",
101101
"inputRev": "master",
@@ -105,7 +105,7 @@
105105
"type": "git",
106106
"subDir": null,
107107
"scope": "leanprover-community",
108-
"rev": "78e1181c4752c7e10874d2ed5a6a15063f4a35b6",
108+
"rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
109109
"name": "batteries",
110110
"manifestFile": "lake-manifest.json",
111111
"inputRev": "main",
@@ -115,7 +115,7 @@
115115
"type": "git",
116116
"subDir": null,
117117
"scope": "leanprover",
118-
"rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664",
118+
"rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4",
119119
"name": "Cli",
120120
"manifestFile": "lake-manifest.json",
121121
"inputRev": "main",

‎lakefile.lean‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
11
import Lake
22
open Lake DSL System
33

4-
-- FIXME: change to "https://github.com/leanprover-community/lean-auto.git" once they bump to v4.16.0 upstream
5-
require auto from git "https://github.com/dranov/lean-auto.git" @ "bump-v4.20.0-rc3"
6-
require smt from git "https://github.com/dranov/lean-smt.git" @ "bump-v4.20.0-rc3"
4+
require auto from git "https://github.com/leanprover-community/lean-auto.git" @ "ec89836a79a3266ebd840fb0df59ca4c972a4c25"
5+
require smt from git "https://github.com/dranov/lean-smt.git" @ "v4.20.0"
76

87
package veil
98

‎lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.20.0-rc3
1+
leanprover/lean4:v4.20.0

0 commit comments

Comments
 (0)