feat: elaborate all definitions using elabMutualDef
This commit is contained in:
Leonardo de Moura
parent
102d2ae57d
commit
d8855c2673
12 changed files with 62 additions and 157 deletions
|
|
@ -157,9 +157,7 @@ fun stx => match expandDeclNamespace? stx with
|
|||
else if declKind == `Lean.Parser.Command.structure then
|
||||
elabStructure modifiers decl
|
||||
else if isDefLike decl then do
|
||||
-- TODO: use `elabMutualDef #[stx]`
|
||||
view ← mkDefView modifiers decl;
|
||||
elabDefLike view
|
||||
elabMutualDef #[stx]
|
||||
else
|
||||
throwError "unexpected declaration"
|
||||
|
||||
|
|
|
|||
|
|
@ -134,114 +134,6 @@ else if declKind == `Lean.Parser.Command.«example» then
|
|||
else
|
||||
throwError "unexpected kind of definition"
|
||||
|
||||
/- TODO Remove the rest of the file after we finish `MutualDef.lean`, and rename it to `DefView.lean` -/
|
||||
|
||||
private def removeUnused (vars : Array Expr) (xs : Array Expr) (e : Expr) (eType : Expr)
|
||||
: TermElabM (LocalContext × LocalInstances × Array Expr) := do
|
||||
let used : CollectFVars.State := {};
|
||||
(_, used) ← (Term.collectUsedFVars eType).run used;
|
||||
(_, used) ← (Term.collectUsedFVars e).run used;
|
||||
(_, used) ← (Term.collectUsedFVarsAtFVars xs).run used;
|
||||
Term.removeUnused vars used
|
||||
|
||||
private def withUsedWhen {α} (vars : Array Expr) (xs : Array Expr) (e : Expr) (eType : Expr) (cond : Bool) (k : Array Expr → TermElabM α) : TermElabM α :=
|
||||
if cond then do
|
||||
(lctx, localInsts, vars) ← removeUnused vars xs e eType;
|
||||
withLCtx lctx localInsts $ k vars
|
||||
else
|
||||
k vars
|
||||
|
||||
private def withUsedWhen' {α} (vars : Array Expr) (xs : Array Expr) (e : Expr) (cond : Bool) (k : Array Expr → TermElabM α) : TermElabM α :=
|
||||
let dummyExpr := mkSort levelOne;
|
||||
withUsedWhen vars xs e dummyExpr cond k
|
||||
|
||||
def mkDef? (view : DefView) (declName : Name) (scopeLevelNames allUserLevelNames : List Name) (vars : Array Expr) (xs : Array Expr) (type : Expr) (val : Expr)
|
||||
: TermElabM (Option Declaration) := do
|
||||
withRef view.ref do
|
||||
Term.synthesizeSyntheticMVars;
|
||||
val ← withRef view.value $ Term.ensureHasType type val;
|
||||
Term.synthesizeSyntheticMVarsNoPostponing;
|
||||
type ← instantiateMVars type;
|
||||
val ← instantiateMVars val;
|
||||
if view.kind.isExample then pure none
|
||||
else withUsedWhen vars xs val type view.kind.isDefOrAbbrevOrOpaque $ fun vars => do
|
||||
type ← mkForallFVars xs type;
|
||||
type ← mkForallFVars vars type;
|
||||
val ← mkLambdaFVars xs val;
|
||||
val ← mkLambdaFVars vars val;
|
||||
(type, nextParamIdx) ← Term.levelMVarToParam type;
|
||||
(val, _) ← Term.levelMVarToParam val nextParamIdx;
|
||||
type ← instantiateMVars type;
|
||||
val ← instantiateMVars val;
|
||||
let shareCommonTypeVal : Std.ShareCommonM (Expr × Expr) := do {
|
||||
type ← Std.withShareCommon type;
|
||||
val ← Std.withShareCommon val;
|
||||
pure (type, val)
|
||||
};
|
||||
let (type, val) := shareCommonTypeVal.run;
|
||||
trace `Elab.definition.body fun _ => declName ++ " : " ++ type ++ " :=" ++ Format.line ++ val;
|
||||
let usedParams : CollectLevelParams.State := {};
|
||||
let usedParams := collectLevelParams usedParams type;
|
||||
let usedParams := collectLevelParams usedParams val;
|
||||
match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams.params with
|
||||
| Except.error msg => throwError msg
|
||||
| Except.ok levelParams =>
|
||||
match view.kind with
|
||||
| DefKind.theorem =>
|
||||
pure $ some $ Declaration.thmDecl { name := declName, lparams := levelParams, type := type, value := val }
|
||||
| DefKind.opaque =>
|
||||
pure $ some $ Declaration.opaqueDecl { name := declName, lparams := levelParams, type := type, value := val, isUnsafe := view.modifiers.isUnsafe }
|
||||
| DefKind.abbrev =>
|
||||
pure $ some $ Declaration.defnDecl {
|
||||
name := declName, lparams := levelParams, type := type, value := val,
|
||||
hints := ReducibilityHints.abbrev,
|
||||
isUnsafe := view.modifiers.isUnsafe }
|
||||
| DefKind.def => do
|
||||
env ← getEnv;
|
||||
pure $ some $ Declaration.defnDecl {
|
||||
name := declName, lparams := levelParams, type := type, value := val,
|
||||
hints := ReducibilityHints.regular (getMaxHeight env val + 1),
|
||||
isUnsafe := view.modifiers.isUnsafe }
|
||||
| _ => unreachable!
|
||||
|
||||
def elabDefVal (defVal : Syntax) (expectedType : Expr) : TermElabM Expr := do
|
||||
let kind := defVal.getKind;
|
||||
if kind == `Lean.Parser.Command.declValSimple then
|
||||
-- parser! " := " >> termParser
|
||||
Term.elabTerm (defVal.getArg 1) expectedType
|
||||
else if kind == `Lean.Parser.Command.declValEqns then
|
||||
throwErrorAt defVal "equations have not been implemented yet"
|
||||
else
|
||||
throwUnsupportedSyntax
|
||||
|
||||
def elabDefLike (view : DefView) : CommandElabM Unit :=
|
||||
withRef view.ref do
|
||||
scopeLevelNames ← getLevelNames;
|
||||
⟨name, declName, allUserLevelNames⟩ ← expandDeclId view.declId view.modifiers;
|
||||
runTermElabM declName $ fun vars => Term.withLevelNames allUserLevelNames $ Term.elabBinders view.binders.getArgs fun xs => do
|
||||
applyAttributes declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration;
|
||||
decl? ← match view.type? with
|
||||
| some typeStx => do
|
||||
type ← Term.elabType typeStx;
|
||||
Term.synthesizeSyntheticMVarsNoPostponing;
|
||||
type ← instantiateMVars type;
|
||||
withUsedWhen' vars xs type view.kind.isTheorem $ fun vars => do
|
||||
val ← elabDefVal view.value type;
|
||||
mkDef? view declName scopeLevelNames allUserLevelNames vars xs type val
|
||||
| none => do {
|
||||
type ← withRef view.binders $ mkFreshTypeMVar;
|
||||
val ← elabDefVal view.value type;
|
||||
mkDef? view declName scopeLevelNames allUserLevelNames vars xs type val
|
||||
};
|
||||
match decl? with
|
||||
| none => pure ()
|
||||
| some decl => do
|
||||
Term.ensureNoUnassignedMVars decl;
|
||||
addDecl decl;
|
||||
applyAttributes declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
|
||||
compileDecl decl;
|
||||
applyAttributes declName view.modifiers.attrs AttributeApplicationTime.afterCompilation
|
||||
|
||||
@[init] private def regTraceClasses : IO Unit := do
|
||||
registerTraceClass `Elab.definition;
|
||||
pure ()
|
||||
|
|
|
|||
|
|
@ -646,6 +646,7 @@ let decl :=
|
|||
Declaration.defnDecl { name := preDecl.declName, lparams := preDecl.lparams, type := preDecl.type, value := preDecl.value,
|
||||
hints := ReducibilityHints.regular (getMaxHeight env preDecl.value + 1),
|
||||
isUnsafe := preDecl.modifiers.isUnsafe };
|
||||
ensureNoUnassignedMVars decl;
|
||||
addDecl decl;
|
||||
applyAttributesOf #[preDecl] AttributeApplicationTime.afterTypeChecking;
|
||||
compileDecl decl;
|
||||
|
|
@ -661,6 +662,7 @@ let decl := Declaration.mutualDefnDecl $ preDecls.toList.map fun preDecl => {
|
|||
isUnsafe := true,
|
||||
hints := ReducibilityHints.opaque
|
||||
};
|
||||
ensureNoUnassignedMVars decl;
|
||||
addDecl decl;
|
||||
applyAttributesOf preDecls AttributeApplicationTime.afterTypeChecking;
|
||||
compileDecl decl;
|
||||
|
|
@ -692,6 +694,7 @@ withFunLocalDecls headers fun funFVars => do
|
|||
preDecls ← levelMVarToParamPreDecls preDecls;
|
||||
preDecls ← instantiateMVarsAtPreDecls preDecls;
|
||||
preDecls ← fixLevelParams preDecls scopeLevelNames allUserLevelNames;
|
||||
preDecls.forM fun preDecl => trace `Elab.definition.body fun _ => preDecl.declName ++ " : " ++ preDecl.type ++ " :=" ++ Format.line ++ preDecl.value;
|
||||
let (preDeclsNonRec, preDecls) := partitionNonRec preDecls;
|
||||
preDeclsNonRec.forM addAndCompileNonRec;
|
||||
-- TODO
|
||||
|
|
|
|||
|
|
@ -45,11 +45,11 @@ adaptReader (fun (ctx : Context) => { ctx with errToSorry := ctx.errToSorry && e
|
|||
Try to elaborate `stx` that was postponed by an elaboration method using `Expection.postpone`.
|
||||
It returns `true` if it succeeded, and `false` otherwise.
|
||||
It is used to implement `synthesizeSyntheticMVars`. -/
|
||||
private def resumePostponed (macroStack : MacroStack) (stx : Syntax) (mvarId : MVarId) (postponeOnError : Bool) : TermElabM Bool := do
|
||||
private def resumePostponed (macroStack : MacroStack) (declName? : Option Name) (stx : Syntax) (mvarId : MVarId) (postponeOnError : Bool) : TermElabM Bool := do
|
||||
withRef stx $ withMVarContext mvarId $ do
|
||||
s ← get;
|
||||
catch
|
||||
(adaptReader (fun (ctx : Context) => { ctx with macroStack := macroStack }) $ do
|
||||
(adaptReader (fun (ctx : Context) => { ctx with macroStack := macroStack, declName? := declName? }) $ do
|
||||
mvarDecl ← getMVarDecl mvarId;
|
||||
expectedType ← instantiateMVars mvarDecl.type;
|
||||
result ← resumeElabTerm stx expectedType (!postponeOnError);
|
||||
|
|
@ -102,17 +102,18 @@ pure $ !val.getAppFn.isMVar
|
|||
private def synthesizeSyntheticMVar (mvarSyntheticDecl : SyntheticMVarDecl) (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool :=
|
||||
withRef mvarSyntheticDecl.stx $
|
||||
match mvarSyntheticDecl.kind with
|
||||
| SyntheticMVarKind.typeClass => synthesizePendingInstMVar mvarSyntheticDecl.mvarId
|
||||
| SyntheticMVarKind.coe expectedType eType e f? => synthesizePendingCoeInstMVar mvarSyntheticDecl.mvarId expectedType eType e f?
|
||||
| SyntheticMVarKind.typeClass => synthesizePendingInstMVar mvarSyntheticDecl.mvarId
|
||||
| SyntheticMVarKind.coe expectedType eType e f? => synthesizePendingCoeInstMVar mvarSyntheticDecl.mvarId expectedType eType e f?
|
||||
-- NOTE: actual processing at `synthesizeSyntheticMVarsAux`
|
||||
| SyntheticMVarKind.withDefault _ => checkWithDefault mvarSyntheticDecl.mvarId
|
||||
| SyntheticMVarKind.postponed macroStack => resumePostponed macroStack mvarSyntheticDecl.stx mvarSyntheticDecl.mvarId postponeOnError
|
||||
| SyntheticMVarKind.tactic tacticCode =>
|
||||
if runTactics then do
|
||||
runTactic mvarSyntheticDecl.mvarId tacticCode;
|
||||
pure true
|
||||
else
|
||||
pure false
|
||||
| SyntheticMVarKind.withDefault _ => checkWithDefault mvarSyntheticDecl.mvarId
|
||||
| SyntheticMVarKind.postponed macroStack declName? => resumePostponed macroStack declName? mvarSyntheticDecl.stx mvarSyntheticDecl.mvarId postponeOnError
|
||||
| SyntheticMVarKind.tactic declName? tacticCode =>
|
||||
adaptReader (fun (ctx : Context) => { ctx with declName? := declName? }) $
|
||||
if runTactics then do
|
||||
runTactic mvarSyntheticDecl.mvarId tacticCode;
|
||||
pure true
|
||||
else
|
||||
pure false
|
||||
|
||||
/--
|
||||
Try to synthesize the current list of pending synthetic metavariables.
|
||||
|
|
|
|||
|
|
@ -54,9 +54,9 @@ inductive SyntheticMVarKind
|
|||
-- we use "type mismatch" or "application type mismatch" (when `f?` is some) instead of "failed to synthesize"
|
||||
| coe (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr)
|
||||
-- tactic block execution
|
||||
| tactic (tacticCode : Syntax)
|
||||
| tactic (declName? : Option Name) (tacticCode : Syntax)
|
||||
-- `elabTerm` call that threw `Exception.postpone` (input is stored at `SyntheticMVarDecl.ref`)
|
||||
| postponed (macroStack : MacroStack)
|
||||
| postponed (macroStack : MacroStack) (declName? : Option Name)
|
||||
-- type defaulting (currently: defaulting numeric literals to `Nat`)
|
||||
| withDefault (defaultVal : Expr)
|
||||
|
||||
|
|
@ -731,7 +731,7 @@ private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : Term
|
|||
trace `Elab.postpone $ fun _ => stx ++ " : " ++ expectedType?;
|
||||
mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque;
|
||||
ctx ← read;
|
||||
registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed ctx.macroStack);
|
||||
registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed ctx.macroStack ctx.declName?);
|
||||
pure mvar
|
||||
|
||||
/-
|
||||
|
|
@ -995,7 +995,8 @@ def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
|
|||
mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque `main;
|
||||
let mvarId := mvar.mvarId!;
|
||||
ref ← getRef;
|
||||
registerSyntheticMVar ref mvarId $ SyntheticMVarKind.tactic tacticCode;
|
||||
declName? ← getDeclName?;
|
||||
registerSyntheticMVar ref mvarId $ SyntheticMVarKind.tactic declName? tacticCode;
|
||||
pure mvar
|
||||
|
||||
@[builtinTermElab byTactic] def elabByTactic : TermElab :=
|
||||
|
|
|
|||
|
|
@ -2,39 +2,45 @@ doSeqRightIssue.lean:5:24: error: unknown universe level v
|
|||
doSeqRightIssue.lean:5:24: error: unknown universe level v
|
||||
doSeqRightIssue.lean:7:0: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
p₁ p₂ : (sorryAx (Sort u_1))
|
||||
h₁ : (sorryAx ?m.319)=(sorryAx ?m.319)
|
||||
h : (sorryAx (?m.320 _))≅_
|
||||
_a_1 _a_2 : (sorryAx (Sort u_1))
|
||||
_a_3 : (sorryAx ?m.319)=(sorryAx ?m.319)
|
||||
α : Type u
|
||||
β : α → (sorryAx (Sort u_1))
|
||||
ex : ∀ {p₁p₂ : (sorryAx (Sort u_2))} (h₁ : (sorryAx ?m.335)=(sorryAx ?m.335)), (sorryAx (?m.336 h₁))≅_ → p₁=p₂
|
||||
p₁ p₂ : (sorryAx (Sort u_2))
|
||||
h₁ : (sorryAx ?m.335)=(sorryAx ?m.335)
|
||||
h : (sorryAx (?m.336 _))≅_
|
||||
_a_1 _a_2 : (sorryAx (Sort u_2))
|
||||
_a_3 : (sorryAx ?m.335)=(sorryAx ?m.335)
|
||||
⊢ Prop
|
||||
doSeqRightIssue.lean:7:0: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
p₁ p₂ : (sorryAx (Sort u_1))
|
||||
h₁ : (sorryAx ?m.319)=(sorryAx ?m.319)
|
||||
h : (sorryAx (?m.320 _))≅_
|
||||
_a_1 _a_2 : (sorryAx (Sort u_1))
|
||||
α : Type u
|
||||
β : α → (sorryAx (Sort u_1))
|
||||
ex : ∀ {p₁p₂ : (sorryAx (Sort u_2))} (h₁ : (sorryAx ?m.335)=(sorryAx ?m.335)), (sorryAx (?m.336 h₁))≅_ → p₁=p₂
|
||||
p₁ p₂ : (sorryAx (Sort u_2))
|
||||
h₁ : (sorryAx ?m.335)=(sorryAx ?m.335)
|
||||
h : (sorryAx (?m.336 _))≅_
|
||||
_a_1 _a_2 : (sorryAx (Sort u_2))
|
||||
⊢ Prop
|
||||
doSeqRightIssue.lean:7:66: error: don't know how to synthesize placeholder
|
||||
@HEq ?m.320 … … …
|
||||
@HEq ?m.336 … … …
|
||||
context:
|
||||
α : Type u
|
||||
β : α → (sorryAx (Sort ?))
|
||||
p₁ p₂ : (sorryAx (Sort u_1))
|
||||
h₁ : (sorryAx ?m.319)=(sorryAx ?m.319)
|
||||
β : α → (sorryAx (Sort u_1))
|
||||
p₁ p₂ : (sorryAx (Sort u_2))
|
||||
h₁ : (sorryAx ?m.335)=(sorryAx ?m.335)
|
||||
⊢ Prop
|
||||
doSeqRightIssue.lean:7:66: error: don't know how to synthesize placeholder
|
||||
@HEq ?m.320 … … …
|
||||
@HEq ?m.336 … … …
|
||||
context:
|
||||
α : Type u
|
||||
β : α → (sorryAx (Sort ?))
|
||||
p₁ p₂ : (sorryAx (Sort u_1))
|
||||
h₁ : (sorryAx ?m.319)=(sorryAx ?m.319)
|
||||
β : α → (sorryAx (Sort u_1))
|
||||
p₁ p₂ : (sorryAx (Sort u_2))
|
||||
h₁ : (sorryAx ?m.335)=(sorryAx ?m.335)
|
||||
⊢ Prop
|
||||
doSeqRightIssue.lean:7:48: error: don't know how to synthesize placeholder
|
||||
@Eq ?m.319 … …
|
||||
@Eq ?m.335 … …
|
||||
context:
|
||||
α : Type u
|
||||
β : α → (sorryAx (Sort ?))
|
||||
p₁ p₂ : (sorryAx (Sort u_1))
|
||||
⊢ Sort u_2
|
||||
β : α → (sorryAx (Sort u_1))
|
||||
p₁ p₂ : (sorryAx (Sort u_2))
|
||||
⊢ Sort u_3
|
||||
|
|
|
|||
|
|
@ -2,21 +2,25 @@ holes.lean:4:4: error: placeholders '_' cannot be used where a function is expec
|
|||
holes.lean:11:8: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
case hole
|
||||
f3 : Nat → Nat
|
||||
x : Nat
|
||||
y : Nat := g x+g x
|
||||
⊢ Nat
|
||||
holes.lean:11:4: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
f3 : Nat → Nat
|
||||
x : Nat
|
||||
y : Nat := g x+g x
|
||||
⊢ Nat
|
||||
holes.lean:10:15: error: don't know how to synthesize placeholder
|
||||
@g … ?m.39 …
|
||||
@g … ?m.49 …
|
||||
context:
|
||||
f3 : Nat → Nat
|
||||
x : Nat
|
||||
⊢ Type
|
||||
holes.lean:10:9: error: don't know how to synthesize placeholder
|
||||
@g … ?m.38 …
|
||||
@g … ?m.48 …
|
||||
context:
|
||||
f3 : Nat → Nat
|
||||
x : Nat
|
||||
⊢ Type
|
||||
|
|
|
|||
|
|
@ -27,4 +27,4 @@ inductive1.lean:105:0: error: unexpected constructor resulting type, type expect
|
|||
inductive1.lean:108:0: error: unexpected constructor resulting type
|
||||
Nat
|
||||
inductive1.lean:118:7: error: unknown identifier 'cons'
|
||||
(sorryAx ?m.139) : ?m.139
|
||||
(sorryAx ?m.137) : ?m.137
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ id (fun (x : ?m.4) => x) : ?m.4 → ?m.4
|
|||
f 1 (fun (x : Nat) => x) : Nat
|
||||
0 : Nat
|
||||
f 1 (fun (x : Nat) => x) : Nat
|
||||
id : ?m.73 → ?m.73
|
||||
id : ?m.84 → ?m.84
|
||||
precissues.lean:15:10: error: expected command
|
||||
1 : Nat
|
||||
id ((fun (this : True) => this) True.intro) : True
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
protected.lean:10:7: error: unknown identifier 'x'
|
||||
(sorryAx ?m.24) : ?m.24
|
||||
(sorryAx ?m.23) : ?m.23
|
||||
Foo.x : Nat
|
||||
Bla.Foo.y : Nat
|
||||
protected.lean:22:7: error: unknown identifier 'y'
|
||||
(sorryAx ?m.70) : ?m.70
|
||||
(sorryAx ?m.67) : ?m.67
|
||||
Bla.Foo.z : Nat
|
||||
|
|
|
|||
|
|
@ -2,6 +2,6 @@ Content-Length: 221
|
|||
|
||||
{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1020
|
||||
|
||||
{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":28},"end":{"line":14,"character":28}},"message":"type mismatch\n \"NotANat\"\nhas type\n String\nbut it is expected to have type\n Nat\nfailed to synthesize instance\n CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 38
|
||||
{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":31},"end":{"line":14,"character":31}},"message":"type mismatch\n \"NotANat\"\nhas type\n String\nbut it is expected to have type\n Nat\nfailed to synthesize instance\n CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 38
|
||||
|
||||
{"result":null,"jsonrpc":"2.0","id":1}
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@ Content-Length: 221
|
|||
|
||||
{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1020
|
||||
|
||||
{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":28},"end":{"line":14,"character":28}},"message":"type mismatch\n \"NotANat\"\nhas type\n String\nbut it is expected to have type\n Nat\nfailed to synthesize instance\n CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 184
|
||||
{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":31},"end":{"line":14,"character":31}},"message":"type mismatch\n \"NotANat\"\nhas type\n String\nbut it is expected to have type\n Nat\nfailed to synthesize instance\n CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 184
|
||||
|
||||
{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 883
|
||||
|
||||
|
|
@ -38,7 +38,7 @@ Content-Length: 221
|
|||
|
||||
{"params":{"version":9,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 1211
|
||||
|
||||
{"params":{"version":10,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":16,"character":0},"end":{"line":16,"character":0}},"message":"expected term"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":20,"character":0},"end":{"line":20,"character":0}},"message":"invalid 'end', insufficient scopes"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":22,"character":7},"end":{"line":22,"character":7}},"message":"unknown identifier 'MyNs.u'"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"(sorryAx ?m.37) : ?m.37"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 185
|
||||
{"params":{"version":10,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":16,"character":0},"end":{"line":16,"character":0}},"message":"expected term"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":20,"character":0},"end":{"line":20,"character":0}},"message":"invalid 'end', insufficient scopes"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":22,"character":7},"end":{"line":22,"character":7}},"message":"unknown identifier 'MyNs.u'"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"(sorryAx ?m.41) : ?m.41"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 185
|
||||
|
||||
{"params":{"version":10,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 740
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue