Merge pull request 'chore: Version bump' (#168) from chore/version into dev
Reviewed-on: #168
This commit is contained in:
commit
642bca42e9
|
@ -25,9 +25,9 @@ protected def Info.stx? : Info → Option Syntax
|
|||
| .ofCustomInfo info => info.stx
|
||||
| .ofFVarAliasInfo _ => none
|
||||
| .ofFieldRedeclInfo info => info.stx
|
||||
| .ofOmissionInfo info => info.stx
|
||||
| .ofChoiceInfo info => info.stx
|
||||
| .ofPartialTermInfo info => info.stx
|
||||
| .ofDelabTermInfo info => info.stx
|
||||
/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
|
||||
protected def Info.isOriginal (i : Info) : Bool :=
|
||||
match i.stx? with
|
||||
|
@ -142,9 +142,9 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
|
|||
| .ofCustomInfo _ => pure "[custom]"
|
||||
| .ofFVarAliasInfo _ => pure "[fvar]"
|
||||
| .ofFieldRedeclInfo _ => pure "[field_redecl]"
|
||||
| .ofOmissionInfo _ => pure "[omission]"
|
||||
| .ofChoiceInfo _ => pure "[choice]"
|
||||
| .ofPartialTermInfo _ => pure "[partial_term]"
|
||||
| .ofDelabTermInfo _ => pure "[delab_term]"
|
||||
let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx)
|
||||
return s!"{node}\n{children}"
|
||||
else throw <| IO.userError "No `ContextInfo` available."
|
||||
|
|
|
@ -28,15 +28,16 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
|
|||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do
|
||||
Meta.transform src λ
|
||||
| .app (.app (.const ``sorryAx ..) type) .. => do
|
||||
let type ← instantiateMVars type
|
||||
Meta.transform src λ expr =>
|
||||
if expr.isSorry then do
|
||||
let type ← instantiateMVars (expr.getArg! 0 |>.bindingBody!)
|
||||
if type.hasSorry then
|
||||
throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}"
|
||||
let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
|
||||
modify (mvar.mvarId! :: .)
|
||||
pure $ .done mvar
|
||||
| _ => pure .continue
|
||||
else
|
||||
pure .continue
|
||||
|
||||
-- Given a complete (no holes) expression, extract the sorry's from it and convert them into goals.
|
||||
def draft (goal : MVarId) (expr : Expr) : MetaM (List MVarId) := do
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
namespace Pantograph
|
||||
|
||||
@[export pantograph_version]
|
||||
def version := "0.2.25"
|
||||
def version := "0.3.0-rc.1"
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -192,7 +192,7 @@ def test_proposition_generation: TestM Unit := do
|
|||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
#[.some "?m.29 x"])
|
||||
#[.some "?m.30 x"])
|
||||
addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
|
||||
|
||||
let assign := "Eq.refl x"
|
||||
|
|
|
@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
|
|||
|
||||
addTest $ ← conduit.withContext do
|
||||
let t := toString (← Meta.ppExpr $ ← conduit.getType)
|
||||
return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.149 ?m.{majorId}) = (n + 0 = n)")
|
||||
return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.150 ?m.{majorId}) = (n + 0 = n)")
|
||||
|
||||
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
|
|
26
flake.lock
26
flake.lock
|
@ -5,11 +5,11 @@
|
|||
"nixpkgs-lib": "nixpkgs-lib"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1730504689,
|
||||
"narHash": "sha256-hgmguH29K2fvs9szpq2r3pz2/8cJd2LPS+b4tfNFCwE=",
|
||||
"lastModified": 1738453229,
|
||||
"narHash": "sha256-7H9XgNiGLKN1G1CgRh0vUL4AheZSYzPm+zmZ7vxbJdo=",
|
||||
"owner": "hercules-ci",
|
||||
"repo": "flake-parts",
|
||||
"rev": "506278e768c2a08bec68eb62932193e341f55c90",
|
||||
"rev": "32ea77a06711b758da0ad9bd6a844c5740a87abd",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
@ -42,11 +42,11 @@
|
|||
"nixpkgs": "nixpkgs"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1736388194,
|
||||
"narHash": "sha256-ymSrd/A8Pw+9FzbxUbR7CkFHLJK1b4SnFFWg/1e0JeE=",
|
||||
"lastModified": 1739073990,
|
||||
"narHash": "sha256-VmLkZf4+1HWrIDB/JUlPOAmOlutR6XTFRhDzDYJcYZM=",
|
||||
"owner": "lenianiva",
|
||||
"repo": "lean4-nix",
|
||||
"rev": "90f496bc0694fb97bdfa6adedfc2dc2c841a4cf2",
|
||||
"rev": "7a6faedc6c3ab35c42add15c354bf69542b9a6e6",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
@ -90,14 +90,14 @@
|
|||
},
|
||||
"nixpkgs-lib": {
|
||||
"locked": {
|
||||
"lastModified": 1730504152,
|
||||
"narHash": "sha256-lXvH/vOfb4aGYyvFmZK/HlsNsr/0CVWlwYvo2rxJk3s=",
|
||||
"lastModified": 1738452942,
|
||||
"narHash": "sha256-vJzFZGaCpnmo7I6i416HaBLpC+hvcURh/BQwROcGIp8=",
|
||||
"type": "tarball",
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz"
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/072a6db25e947df2f31aab9eccd0ab75d5b2da11.tar.gz"
|
||||
},
|
||||
"original": {
|
||||
"type": "tarball",
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz"
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/072a6db25e947df2f31aab9eccd0ab75d5b2da11.tar.gz"
|
||||
}
|
||||
},
|
||||
"nixpkgs-lib_2": {
|
||||
|
@ -114,11 +114,11 @@
|
|||
},
|
||||
"nixpkgs_2": {
|
||||
"locked": {
|
||||
"lastModified": 1731386116,
|
||||
"narHash": "sha256-lKA770aUmjPHdTaJWnP3yQ9OI1TigenUqVC3wweqZuI=",
|
||||
"lastModified": 1735563628,
|
||||
"narHash": "sha256-OnSAY7XDSx7CtDoqNh8jwVwh4xNL/2HaJxGjryLWzX8=",
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "689fed12a013f56d4c4d3f612489634267d86529",
|
||||
"rev": "b134951a4c9f3c995fd7be05f3243f8ecd65d798",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:v4.15.0
|
||||
leanprover/lean4:v4.16.0
|
||||
|
|
Loading…
Reference in New Issue