Skip to content

Commit d103408

Browse files
volodeykaVexobendipeshkaphle
authored
Remove velvet (#43)
* spec DSL * minor changes: use := in def_pre instead of : * disallow recursion by default * manually improve specification example quality for RAG * add loomAbstractionSimp by default * capture section Specs to enter specDSL. Capture def precondition instead of using def_pre * update rag examples * Add assert_same_evaluation macro, spec command, forbid usage of spec in velvet body * add velvetSpecHelper * remove debug info * do not add velvetSpecHelper by default * Add invariant naming mechanism for easy tagging * save experiment result * Add verina basic programs with verina_basic.json for stats * add spec equiv proof * some progress * simplify proofs * minimize programs dafy and lean * syntax error fix dafny files * refactiring * refactiring * refactiring * refactiring * refactiring * refactiring * improve exampels * refactiring * refactiring * refactiring * improve advanced 11 * refactiring * refactiring * Remove unused imports and useless tactics * Rename, add async version and benchmark scripts * Restructure stuffs * line-counting scripts * add IsNonPrime * fix auto version * minor change to isNonPrime. remove unnecessary import * Remove needs refactoring * add back isPrime * collecting bench programs * minor change * some rollback * fix bug * remove velvet * remove velvet from CI --------- Co-authored-by: Vexoben <Vexoben@gmail.com> Co-authored-by: Dipesh Kafle <dipesh.kaphle111@gmail.com> Co-authored-by: YueyangFeng <vexoben.gmail>
1 parent 2c7dbe7 commit d103408

28 files changed

+56
-4369
lines changed

‎.github/workflows/lean_action_ci.yml‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,4 @@ jobs:
1515
with:
1616
use-github-cache: false
1717
- name: Build Cashmere
18-
run: lake build Cashmere
19-
- name: Build Velvet
20-
run: lake build Velvet
18+
run: lake build Cashmere

‎.vscode/settings.json‎

Lines changed: 0 additions & 6 deletions
This file was deleted.

‎CaseStudies/Cashmere/Syntax_Cashmere.lean‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -217,16 +217,22 @@ macro_rules
217217
try simp at *
218218
try aesop))
219219

220+
/-- Helper to wrap an invariant with the appropriate name elaborator for Cashmere -/
221+
def mkNamedInvariantCashmere (balance : Ident) (balanceType : Term) (invName? : Option (TSyntax `str)) (inv : TSyntax `term) : MacroM (TSyntax `term) :=
222+
match invName? with
223+
| some name => `(fun ($balance : $balanceType) => with_custom_name `invariant $name $inv)
224+
| none => `(fun ($balance : $balanceType) => with_name_prefix `invariant $inv)
225+
220226
macro_rules
221227
| `(doElem| while $t
222-
$[invariant $inv:term
228+
$[invariant $[$invName:str]? $inv:term
223229
]*
224230
$[done_with $inv_done]?
225231
$[decreasing $measure]?
226232
do $seq:doSeq) => do
227233
let balance := mkIdent `balance_name
228234
let balanceType <- `(term| Bal)
229-
let inv : Array Term <- inv.mapM fun (inv : Term) => withRef inv ``(fun ($(balance):ident : $balanceType)=> with_name_prefix `inv $inv)
235+
let inv : Array Term <- (invName.zip inv).mapM fun (n?, i) => mkNamedInvariantCashmere balance balanceType n? i
230236
let invd_some <- match inv_done with
231237
| some invd_some => withRef invd_some ``(fun ($(balance):ident : $balanceType) => with_name_prefix `done $invd_some)
232238
| none => ``(fun ($(balance):ident : $balanceType) => with_name_prefix `done ¬$t:term)

‎CaseStudies/Macro.lean‎

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ declare_syntax_cat doneWith
5151
declare_syntax_cat decreasingTerm
5252
declare_syntax_cat invariantClause
5353
declare_syntax_cat invariantClauses
54-
syntax "invariant" termBeforeDo linebreak : invariantClause
54+
syntax "invariant" (str)? termBeforeDo linebreak : invariantClause
5555
syntax "done_with" termBeforeDo : doneWith
5656
syntax "decreasing" termBeforeDo : decreasingTerm
5757
syntax (invariantClause linebreak)* : invariantClauses
@@ -100,6 +100,12 @@ This measure elaborates to a term of type `β → Option ℕ` where `β` is a re
100100
correctness semantics.
101101
If `decreasing` is unspecified, measure is assumed to be `none`.
102102
-/
103+
/-- Helper to wrap an invariant with the appropriate name elaborator -/
104+
def mkNamedInvariant (invName? : Option (TSyntax `str)) (inv : TSyntax `term) : MacroM (TSyntax `term) :=
105+
match invName? with
106+
| some name => `(with_custom_name `invariant $name $inv)
107+
| none => `(with_name_prefix `invariant $inv)
108+
103109
macro_rules
104110
| `(doElem| while $t do $seq:doSeq) => do
105111
let decr <- withRef (<- getRef) `(decreasing none)
@@ -113,12 +119,13 @@ macro_rules
113119
$seq:doSeq
114120
else break)
115121
| `(doElem| while $t
116-
$[invariant $inv:term
122+
$[invariant $[$invName:str]? $inv:term
117123
]*
118124
$[done_with $inv_done]?
119125
$[decreasing $measure]?
120126
do $seq:doSeq) => do
121-
let invs <- `(invariants [ $[(with_name_prefix `invariant $inv:term)],* ])
127+
let namedInvs ← (invName.zip inv).mapM fun (n?, i) => mkNamedInvariant n? i
128+
let invs <- `(invariants [ $[$namedInvs:term],* ])
122129
let invd_some ← match inv_done with
123130
| some invd_some => withRef invd_some ``($invd_some)
124131
| none => ``(¬$t:term)
@@ -135,7 +142,6 @@ macro_rules
135142
else break)
136143
| none => do
137144
let decr <- withRef (<- getRef) `(decreasing none)
138-
let invs <- `(invariants [ $[(with_name_prefix `invariant $inv:term)],* ])
139145
`(doElem|
140146
for _ in Lean.Loop.mk do
141147
$invs:term
@@ -155,11 +161,12 @@ macro_rules
155161
$[$seq:doElem]*)
156162
| _ => Lean.Macro.throwError "while_some expects a sequence of do-elements"
157163
| `(doElem| while_some $x:ident :| $t
158-
$[invariant $inv:term
164+
$[invariant $[$invName:str]? $inv:term
159165
]*
160166
$[done_with $inv_done]? do
161167
$seq:doSeq) => do
162-
let invs <- `(invariants [ $[(with_name_prefix `invariant $inv:term)],* ])
168+
let namedInvs ← (invName.zip inv).mapM fun (n?, i) => mkNamedInvariant n? i
169+
let invs <- `(invariants [ $[$namedInvs:term],* ])
163170
let invd_some ← match inv_done with
164171
| some invd_some => withRef invd_some ``($invd_some)
165172
| none => ``(¬$t:term)
@@ -179,10 +186,11 @@ macro_rules
179186
else break)
180187
| _ => Lean.Macro.throwError "while_some expects a sequence of do-elements"
181188
| `(doElem| for $x:ident in $t
182-
$[invariant $inv:term
189+
$[invariant $[$invName:str]? $inv:term
183190
]*
184191
do $seq:doSeq) => do
185-
let invs <- `(invariants [ $[(with_name_prefix `invariant $inv:term)],* ])
192+
let namedInvs ← (invName.zip inv).mapM fun (n?, i) => mkNamedInvariant n? i
193+
let invs <- `(invariants [ $[$namedInvs:term],* ])
186194
match seq with
187195
| `(doSeq| $[$seq:doElem]*)
188196
| `(doSeq| $[$seq:doElem;]*)

‎CaseStudies/Tactic.lean‎

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,8 @@ private def _root_.Lean.SimplePersistentEnvExtension.get [Inhabited σ] (ext : S
3030
[Monad m] [MonadEnv m] : m σ := do
3131
return ext.getState (<- getEnv)
3232

33-
def getAssertionStx : TacticM (Option Term) := withMainContext do
33+
/-- Get assertion info: returns (name, syntax) pair for case tagging -/
34+
def getAssertionInfo : TacticM (Option (Name × Term)) := withMainContext do
3435
let goal <- getMainTarget
3536
let goalStx <- ppExpr goal
3637
let ⟨_, ss, ns, _⟩ <- loomAssertionsMap.get
@@ -41,7 +42,7 @@ def getAssertionStx : TacticM (Option Term) := withMainContext do
4142
let sname <- nname.getName
4243
let some id1 := ns[sname]?
4344
| throwError s!"typeWithName {sname} not registered: {typeWithNameExpr}"
44-
return some ss[id1]!
45+
return some (sname, ss[id1]!)
4546
match_expr withNameExpr with
4647
| WithName exp name =>
4748
let name <- name.getName
@@ -52,10 +53,13 @@ def getAssertionStx : TacticM (Option Term) := withMainContext do
5253
let sname <- nname.getName
5354
let some id1 := ns[sname]?
5455
| throwError s!"typeWithName {sname} not registered: {typeWithNameExpr}"
55-
return some ss[id1]!
56-
return some ss[id]!
56+
return some (sname, ss[id1]!)
57+
return some (name, ss[id]!)
5758
| _ => throwError s!"Failed to prove assertion which is not registered4: {goalStx}"
58-
--let ⟨maxId, ss, ns⟩ <- loomAssertionsMap.get
59+
60+
def getAssertionStx : TacticM (Option Term) := do
61+
let info? <- getAssertionInfo
62+
return info?.map (·.2)
5963

6064
declare_syntax_cat loom_solve_tactic
6165
syntax "loom_solve" : loom_solve_tactic
@@ -143,10 +147,13 @@ elab_rules : tactic
143147
let mut unsolved := #[]
144148
for mvarId in <- getUnsolvedGoals do
145149
setGoals [mvarId]
146-
let stx <- getAssertionStx
150+
let info? <- getAssertionInfo
147151
evalTactic vlsUnfold
148-
if let some stx := stx then
149-
(<- getMainGoal).setTag <| .mkSimple stx.raw.prettyPrint.pretty
152+
if let some (name, stx) := info? then
153+
-- Combine the internal name with the expression for readable case tags
154+
let exprStr := stx.raw.prettyPrint.pretty
155+
let caseTag := s!"{name}: {exprStr}"
156+
(<- getMainGoal).setTag <| .mkSimple caseTag
150157
if loomSolveIsReporting vls then
151158
logErrorAt stx $ m!"Failed to prove assertion\n{mvarId}"
152159
else if loomSolveIsReporting vls then

‎CaseStudies/Velvet/Std.lean‎

Lines changed: 0 additions & 76 deletions
This file was deleted.

0 commit comments

Comments
 (0)