From d8855c267393efe1307ad967aa472cb0dab2becd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 6 Sep 2020 07:23:47 -0700 Subject: [PATCH] feat: elaborate all definitions using `elabMutualDef` --- src/Lean/Elab/Declaration.lean | 4 +- src/Lean/Elab/Definition.lean | 108 ------------------- src/Lean/Elab/MutualDef.lean | 3 + src/Lean/Elab/SyntheticMVars.lean | 25 ++--- src/Lean/Elab/Term.lean | 9 +- tests/lean/doSeqRightIssue.lean.expected.out | 48 +++++---- tests/lean/holes.lean.expected.out | 8 +- tests/lean/inductive1.lean.expected.out | 2 +- tests/lean/precissues.lean.expected.out | 2 +- tests/lean/protected.lean.expected.out | 4 +- tests/lean/server/diags.lean.expected.out | 2 +- tests/lean/server/edits.lean.expected.out | 4 +- 12 files changed, 62 insertions(+), 157 deletions(-) diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index eab58446d1..0e50b1b933 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -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" diff --git a/src/Lean/Elab/Definition.lean b/src/Lean/Elab/Definition.lean index d4db073b9f..3c40b4ed28 100644 --- a/src/Lean/Elab/Definition.lean +++ b/src/Lean/Elab/Definition.lean @@ -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 () diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 448a9815f0..261db49e29 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -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 diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index fab117838b..3310842bbc 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -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. diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 65e82a244b..29b04c7463 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -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 := diff --git a/tests/lean/doSeqRightIssue.lean.expected.out b/tests/lean/doSeqRightIssue.lean.expected.out index bbd2212f29..af31adc340 100644 --- a/tests/lean/doSeqRightIssue.lean.expected.out +++ b/tests/lean/doSeqRightIssue.lean.expected.out @@ -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 diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out index e3cc146423..15cb371b77 100644 --- a/tests/lean/holes.lean.expected.out +++ b/tests/lean/holes.lean.expected.out @@ -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 diff --git a/tests/lean/inductive1.lean.expected.out b/tests/lean/inductive1.lean.expected.out index 6ae05409a9..c4f31d7332 100644 --- a/tests/lean/inductive1.lean.expected.out +++ b/tests/lean/inductive1.lean.expected.out @@ -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 diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out index fcee8d0322..f8166c8247 100644 --- a/tests/lean/precissues.lean.expected.out +++ b/tests/lean/precissues.lean.expected.out @@ -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 diff --git a/tests/lean/protected.lean.expected.out b/tests/lean/protected.lean.expected.out index 4ccaee959f..c93d96ee3c 100644 --- a/tests/lean/protected.lean.expected.out +++ b/tests/lean/protected.lean.expected.out @@ -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 diff --git a/tests/lean/server/diags.lean.expected.out b/tests/lean/server/diags.lean.expected.out index 54c18939fd..555894a201 100644 --- a/tests/lean/server/diags.lean.expected.out +++ b/tests/lean/server/diags.lean.expected.out @@ -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} diff --git a/tests/lean/server/edits.lean.expected.out b/tests/lean/server/edits.lean.expected.out index 8f37c910a4..c29eac35f4 100644 --- a/tests/lean/server/edits.lean.expected.out +++ b/tests/lean/server/edits.lean.expected.out @@ -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