Merge branch 'dev' into frontend/env-init
This commit is contained in:
commit
0fea0b50c9
GPG Key ID:
4D9B1C8D10EA4C50
|
|
@ -122,7 +122,8 @@ partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
|
|||
return .visit (mkAppN assign args)
|
||||
else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
|
||||
if ← isTracingEnabledFor `Pantograph.Delate then
|
||||
let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
|
||||
let substTableStr := ",".intercalate $
|
||||
Array.zipWith (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") fvars args |>.toList
|
||||
trace[Pantograph.Delate]"MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
|
||||
|
||||
if args.size < fvars.size then
|
||||
|
|
|
|||
|
|
@ -91,7 +91,6 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
|
|||
isUnsafe := info.isUnsafe,
|
||||
value? := ← value?.mapM (λ v => serializeExpression 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 <| type.getUsedConstants.map (λ n => serializeName n)
|
||||
else .none,
|
||||
|
|
@ -169,7 +168,7 @@ def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) :
|
|||
let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with
|
||||
| .ok t => pure t
|
||||
| .error e => return .error $ Protocol.errorExpr e
|
||||
let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
|
||||
let decl := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
|
||||
(name := args.name.toName)
|
||||
(levelParams := [])
|
||||
(type := type)
|
||||
|
|
@ -177,13 +176,7 @@ def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) :
|
|||
(hints := Lean.mkReducibilityHintsRegularEx 1)
|
||||
(safety := Lean.DefinitionSafety.safe)
|
||||
(all := [])
|
||||
let env' ← match env.addDecl (← getOptions) constant with
|
||||
| .error e => do
|
||||
let options ← Lean.MonadOptions.getOptions
|
||||
let desc ← (e.toMessageData options).toString
|
||||
return .error $ { error := "kernel", desc }
|
||||
| .ok env' => pure env'
|
||||
Lean.MonadEnv.modifyEnv (λ _ => env')
|
||||
Lean.addDecl decl
|
||||
return .ok {}
|
||||
|
||||
end Pantograph.Environment
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
namespace Pantograph
|
||||
|
||||
@[export pantograph_version]
|
||||
def version := "0.3.0-rc.1"
|
||||
def version := "0.3.0"
|
||||
|
||||
end Pantograph
|
||||
|
|
|
|||
|
|
@ -47,12 +47,8 @@ def test_environment_pickling : TestM Unit := do
|
|||
(hints := Lean.mkReducibilityHintsRegularEx 1)
|
||||
(safety := Lean.DefinitionSafety.safe)
|
||||
(all := [])
|
||||
let env' ← match (← getEnv).addDecl (← getOptions) c with
|
||||
| .error e => do
|
||||
let error ← (e.toMessageData (← getOptions)).toString
|
||||
throwError error
|
||||
| .ok env' => pure env'
|
||||
environmentPickle env' envPicklePath
|
||||
addDecl c
|
||||
environmentPickle (← getEnv) envPicklePath
|
||||
|
||||
let _ ← runCoreM coreDst do
|
||||
let (env', _) ← environmentUnpickle envPicklePath
|
||||
|
|
|
|||
33
flake.lock
33
flake.lock
|
|
@ -5,11 +5,11 @@
|
|||
"nixpkgs-lib": "nixpkgs-lib"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1738453229,
|
||||
"narHash": "sha256-7H9XgNiGLKN1G1CgRh0vUL4AheZSYzPm+zmZ7vxbJdo=",
|
||||
"lastModified": 1741352980,
|
||||
"narHash": "sha256-+u2UunDA4Cl5Fci3m7S643HzKmIDAe+fiXrLqYsR2fs=",
|
||||
"owner": "hercules-ci",
|
||||
"repo": "flake-parts",
|
||||
"rev": "32ea77a06711b758da0ad9bd6a844c5740a87abd",
|
||||
"rev": "f4330d22f1c5d2ba72d3d22df5597d123fdb60a9",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
|
@ -44,11 +44,11 @@
|
|||
]
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1739073990,
|
||||
"narHash": "sha256-VmLkZf4+1HWrIDB/JUlPOAmOlutR6XTFRhDzDYJcYZM=",
|
||||
"lastModified": 1741472588,
|
||||
"narHash": "sha256-XnMeMZKuspEphP+fEq4soc3PY7Nz+gsMPjlsXbobyrA=",
|
||||
"owner": "lenianiva",
|
||||
"repo": "lean4-nix",
|
||||
"rev": "7a6faedc6c3ab35c42add15c354bf69542b9a6e6",
|
||||
"rev": "cffeb67d58e02b50ccb9acd51b0212dc653ed6ce",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
|
@ -59,11 +59,11 @@
|
|||
},
|
||||
"nixpkgs": {
|
||||
"locked": {
|
||||
"lastModified": 1741332913,
|
||||
"narHash": "sha256-ri1e8ZliWS3Jnp9yqpKApHaOo7KBN33W8ECAKA4teAQ=",
|
||||
"lastModified": 1742751704,
|
||||
"narHash": "sha256-rBfc+H1dDBUQ2mgVITMGBPI1PGuCznf9rcWX/XIULyE=",
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "20755fa05115c84be00b04690630cb38f0a203ad",
|
||||
"rev": "f0946fa5f1fb876a9dc2e1850d9d3a4e3f914092",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
|
@ -75,14 +75,17 @@
|
|||
},
|
||||
"nixpkgs-lib": {
|
||||
"locked": {
|
||||
"lastModified": 1738452942,
|
||||
"narHash": "sha256-vJzFZGaCpnmo7I6i416HaBLpC+hvcURh/BQwROcGIp8=",
|
||||
"type": "tarball",
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/072a6db25e947df2f31aab9eccd0ab75d5b2da11.tar.gz"
|
||||
"lastModified": 1740877520,
|
||||
"narHash": "sha256-oiwv/ZK/2FhGxrCkQkB83i7GnWXPPLzoqFHpDD3uYpk=",
|
||||
"owner": "nix-community",
|
||||
"repo": "nixpkgs.lib",
|
||||
"rev": "147dee35aab2193b174e4c0868bd80ead5ce755c",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"type": "tarball",
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/072a6db25e947df2f31aab9eccd0ab75d5b2da11.tar.gz"
|
||||
"owner": "nix-community",
|
||||
"repo": "nixpkgs.lib",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-lib_2": {
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:v4.16.0
|
||||
leanprover/lean4:v4.17.0
|
||||
|
|
|
|||
Loading…
Reference in New Issue