chore: Version 0.3 #136

Open
aniva wants to merge 487 commits from dev into main
9 changed files with 128 additions and 39 deletions
Showing only changes of commit 431e81ca2f - Show all commits

View File

@ -7,14 +7,15 @@ open Pantograph
namespace Pantograph.Environment
def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
isLeanSymbol n (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) info.isUnsafe
def isNameInternal (n: Lean.Name): Bool :=
-- Returns true if the name is an implementation detail which should not be shown to the user.
isLeanSymbol n (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) n.isAuxLemma n.hasMacroScopes
where
isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
| .str _ name => name == "Lean"
| _ => true
def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String :=
let pref := match info with
| .axiomInfo _ => "a"
| .defnInfo _ => "d"
@ -26,14 +27,14 @@ def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
| .recInfo _ => "r"
s!"{pref}{toString n}"
def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
if is_symbol_unsafe_or_internal n info
def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
if isNameInternal n || info.isUnsafe
then Option.none
else Option.some <| to_compact_symbol_name n info
else Option.some <| toCompactSymbolName n info
def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := #[]) (λ acc name info =>
match to_filtered_symbol name info with
match toFilteredSymbol name info with
| .some x => acc.push x
| .none => acc)
return { symbols := names }
@ -58,8 +59,14 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
value? := ← value?.mapM (λ v => serialize_expression options v |>.run'),
publicName? := Lean.privateToUserName? name |>.map (·.toString),
-- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
typeDependency? := if args.dependency?.getD false
then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n)
else .none,
valueDependency? := ← if args.dependency?.getD false
then info.value?.mapM (λ e => do
let e ← (unfoldAuxLemmas e).run'
pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => name_to_ast n) )
else pure (.none),
module? := module?
}
let result := match info with

View File

@ -170,8 +170,10 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
let metaM := do
state.restoreMetaM
return {
root? := ← state.rootExpr?.mapM (λ expr => serialize_expression options expr),
parent? := ← state.parentExpr?.mapM (λ expr => serialize_expression options expr),
root? := ← state.rootExpr?.mapM (λ expr => do
serialize_expression options (← unfoldAuxLemmas expr)),
parent? := ← state.parentExpr?.mapM (λ expr => do
serialize_expression options (← unfoldAuxLemmas expr)),
}
runMetaM metaM

View File

@ -6,17 +6,20 @@ import Lean
import Pantograph.Protocol
import Pantograph.Goal
namespace Pantograph
open Lean
-- Symbol processing functions --
def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
namespace Pantograph
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
--- Input Functions ---
/-- Read a theorem from the environment -/
def expr_from_const (env: Environment) (name: Name): Except String Lean.Expr :=
match env.find? name with
| none => throw s!"Symbol not found: {name}"
| some cInfo => return cInfo.type
/-- Read syntax object from string -/
def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
Parser.runParserCategory

View File

@ -1,6 +1,6 @@
namespace Pantograph
@[export pantograph_version]
def version := "0.2.13"
def version := "0.2.14"
end Pantograph

View File

@ -1,8 +1,11 @@
import Pantograph.Goal
import Pantograph.Library
import Pantograph.Protocol
import Lean
import LSpec
open Lean
namespace Pantograph
namespace Protocol

View File

@ -2,25 +2,41 @@ import LSpec
import Pantograph.Serial
import Pantograph.Environment
import Test.Common
import Lean
open Lean
namespace Pantograph.Test.Environment
open Pantograph
open Lean
deriving instance DecidableEq, Repr for Protocol.InductInfo
deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
deriving instance DecidableEq, Repr for Protocol.RecursorInfo
deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do
def test_catalog: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
let inner: CoreM LSpec.TestSeq := do
let catalogResult ← Environment.catalog {}
let symbolsWithNum := env.constants.fold (init := #[]) (λ acc name info =>
match (Environment.toFilteredSymbol name info).isSome && (name matches .num _ _) with
| false => acc
| true => acc.push name
)
return LSpec.check "No num symbols" (symbolsWithNum.size == 0)
runCoreMSeq env inner
def test_symbol_visibility: IO LSpec.TestSeq := do
let entries: List (Name × Bool) := [
("Nat.add_comm".toName, false),
("Lean.Name".toName, true)
("Lean.Name".toName, true),
("Init.Data.Nat.Basic._auxLemma.4".toName, true),
]
let suite := entries.foldl (λ suites (symbol, target) =>
let constant := env.constants.find! symbol
let test := LSpec.check symbol.toString ((Environment.is_symbol_unsafe_or_internal symbol constant) == target)
let test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target)
LSpec.TestSeq.append suites test) LSpec.TestSeq.done
return suite
@ -29,7 +45,11 @@ inductive ConstantCat where
| ctor (info: Protocol.ConstructorInfo)
| recursor (info: Protocol.RecursorInfo)
def test_inspect (env: Environment): IO LSpec.TestSeq := do
def test_inspect: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
let testCases: List (String × ConstantCat) := [
("Or", ConstantCat.induct {
numParams := 2,
@ -75,14 +95,9 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
runCoreMSeq env inner
def suite: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #[`Init])
--(imports := #["Prelude"].map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
return LSpec.group "Environment" $
(LSpec.group "Symbol visibility" (← test_symbol_visibility env)) ++
(LSpec.group "Inspect" (← test_inspect env))
(LSpec.group "Catalog" (← test_catalog)) ++
(LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++
(LSpec.group "Inspect" (← test_inspect))
end Pantograph.Test.Environment

View File

@ -1,6 +1,6 @@
import LSpec
import Test.Environment
import Test.Holes
import Test.Metavar
import Test.Integration
import Test.Proofs
import Test.Serial
@ -11,7 +11,7 @@ def main := do
Lean.initSearchPath (← Lean.findSysroot)
let suites := [
Holes.suite,
Metavar.suite,
Integration.suite,
Proofs.suite,
Serial.suite,

View File

@ -2,8 +2,9 @@ import LSpec
import Pantograph.Goal
import Pantograph.Serial
import Test.Common
import Lean
namespace Pantograph.Test.Holes
namespace Pantograph.Test.Metavar
open Pantograph
open Lean
@ -85,6 +86,62 @@ def test_m_couple: TestM Unit := do
addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ 3", .some "3 ≤ 5"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
def test_m_couple_simp: TestM Unit := do
let state? ← startProof "(2: Nat) ≤ 5"
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 2") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
let state1b ← match state2.continue state1 with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ 2", .some "2 ≤ 5"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
let state3 ← match ← state1b.execute (goalId := 0) (tactic := "simp") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let state4 ← match state3.continue state1b with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
let state5 ← match ← state4.execute (goalId := 0) (tactic := "simp") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
state5.restoreMetaM
let root ← match state5.rootExpr? with
| .some e => pure e
| .none =>
addTest $ assertUnreachable "(5 root)"
return ()
let rootStr: String := toString (← Lean.Meta.ppExpr root)
addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
let rootStr: String := toString (← Lean.Meta.ppExpr (← unfoldAuxLemmas root))
addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
return ()
def test_proposition_generation: TestM Unit := do
@ -196,6 +253,7 @@ def suite: IO LSpec.TestSeq := do
(trustLevel := 1)
let tests := [
("2 < 5", test_m_couple),
("2 < 5", test_m_couple_simp),
("Proposition Generation", test_proposition_generation),
("Partial Continuation", test_partial_continuation)
]
@ -204,6 +262,6 @@ def suite: IO LSpec.TestSeq := do
let tests ← proofRunner env tests
return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
return LSpec.group "Holes" tests
return LSpec.group "Metavar" tests
end Pantograph.Test.Holes
end Pantograph.Test.Metavar

View File

@ -1,11 +1,12 @@
import LSpec
import Pantograph.Serial
import Test.Common
import Lean
open Lean
namespace Pantograph.Test.Serial
open Pantograph
open Lean
deriving instance Repr, DecidableEq for Protocol.BoundExpression