From e1d15946f7862c02b2fa6325dada485abb7dc3da Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 14 Mar 2025 08:50:42 +0100 Subject: [PATCH] feat: elaborate theorem bodies in parallel (#7084) This PR enables the elaboration of theorem bodies, i.e. proofs, to happen in parallel to each other as well as to other elaboration tasks. Specifically, to be eligible for parallel proof elaboration, * the theorem must not be in a `mutual` block * `deprecated.oldSectionVars` must not be set * `Elab.async` must be set (currently defaults to `true` in the language server, `false` on the cmdline) To be activated for downstream projects (i.e. in stage 1) pending further Mathlib validation. --- src/Lean/Elab/Command.lean | 8 +- src/Lean/Elab/MutualDef.lean | 136 +++++++++++++++++------- src/Lean/Elab/PreDefinition/Main.lean | 29 +++-- src/Lean/Elab/Tactic/AsAuxLemma.lean | 21 ++-- src/Lean/Meta/CongrTheorems.lean | 4 +- src/Lean/Meta/Eqns.lean | 6 +- src/Lean/Meta/Match/MatchEqs.lean | 15 +++ src/Lean/MonadEnv.lean | 4 +- src/Lean/ReservedNameAction.lean | 8 +- src/Lean/Server/FileWorker.lean | 2 +- src/Lean/Structure.lean | 2 +- src/stdlib_flags.h | 3 + tests/lean/run/ack.lean | 9 ++ tests/lean/run/allGoals.lean | 42 ++++---- tests/lean/run/decideTacticKernel.lean | 5 +- tests/lean/run/eqnsReducible.lean | 2 +- tests/lean/run/grind_attrs.lean | 12 +-- tests/lean/run/info_trees.lean | 97 ++++++++--------- tests/lean/run/variable.lean | 20 ++-- tests/lean/shadow.lean.expected.out | 2 +- tests/lean/syntaxPrec.lean.expected.out | 14 +-- 21 files changed, 265 insertions(+), 176 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index e83c3f4d1e..5e2d598a1a 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -467,7 +467,12 @@ open Language in instance : ToSnapshotTree MacroExpandedSnapshot where toSnapshotTree s := ⟨s.toSnapshot, s.next.map (·.map (sync := true) toSnapshotTree)⟩ -partial def elabCommand (stx : Syntax) : CommandElabM Unit := do +partial def elabCommand (stx : Syntax) : CommandElabM Unit := + try + go + finally + addTraceAsMessages +where go := do withLogging <| withRef stx <| withIncRecDepth <| withFreshMacroScope do match stx with | Syntax.node _ k args => @@ -593,7 +598,6 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro messages := initMsgs ++ msgs infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees } } - addTraceAsMessages /-- Adapt a syntax transformation to a regular, command-producing elaborator. -/ def adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab := fun stx => do diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index fc022a777a..3058fa9241 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -135,12 +135,10 @@ private def cleanupOfNat (type : Expr) : MetaM Expr := do Elaborates only the declaration view headers. We have to elaborate the headers first because we support mutually recursive declarations in Lean 4. -/ -private def elabHeaders (views : Array DefView) +private def elabHeaders (views : Array DefView) (expandedDeclIds : Array ExpandDeclIdResult) (bodyPromises : Array (IO.Promise (Option BodyProcessedSnapshot))) (tacPromises : Array (IO.Promise Tactic.TacticParsedSnapshot)) : TermElabM (Array DefViewElabHeader) := do - let expandedDeclIds ← views.mapM fun view => withRef view.headerRef do - Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers withAutoBoundImplicitForbiddenPred (fun n => expandedDeclIds.any (·.shortName == n)) do let mut headers := #[] -- Can we reuse the result for a body? For starters, all headers (even those below the body) @@ -1019,6 +1017,9 @@ private def checkAllDeclNamesDistinct (preDefs : Array PreDefinition) : TermElab throwErrorAt preDef.ref errorMsg names := names.insert userName preDef.ref +structure AsyncBodyInfo where +deriving TypeName + def elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit := if isExample views then withoutModifyingEnv do @@ -1031,44 +1032,107 @@ where go := do let bodyPromises ← views.mapM fun _ => IO.Promise.new let tacPromises ← views.mapM fun _ => IO.Promise.new - let scopeLevelNames ← getLevelNames - let headers ← elabHeaders views bodyPromises tacPromises + let expandedDeclIds ← views.mapM fun view => withRef view.headerRef do + Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers + let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises let headers ← levelMVarToParamHeaders views headers - let allUserLevelNames := getAllUserLevelNames headers - withFunLocalDecls headers fun funFVars => do - for view in views, funFVar in funFVars do - addLocalVarInfo view.declId funFVar - let values ← - try - let values ← elabFunValues headers vars sc - Term.synthesizeSyntheticMVarsNoPostponing - values.mapM (instantiateMVarsProfiling ·) - catch ex => - logException ex - headers.mapM fun header => withRef header.declId <| mkLabeledSorry header.type (synthetic := true) (unique := true) - let headers ← headers.mapM instantiateMVarsAtHeader - let letRecsToLift ← getLetRecsToLift - let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift - checkLetRecsToLiftTypes funFVars letRecsToLift - (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc headers else withUsed vars headers values letRecsToLift) fun vars => do - let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift - checkAllDeclNamesDistinct preDefs - for preDef in preDefs do - trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}" - let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamTypesPreDecls preDefs - let preDefs ← instantiateMVarsAtPreDecls preDefs - let preDefs ← shareCommonPreDefs preDefs - let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames - for preDef in preDefs do - trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}" - addPreDefinitions preDefs - processDeriving headers - for view in views, header in headers do + -- elaborate body in parallel when all stars align + if let (#[view], #[declId]) := (views, expandedDeclIds) then + if Elab.async.get (← getOptions) && view.kind.isTheorem && + !deprecated.oldSectionVars.get (← getOptions) && + -- holes in theorem types is not a fatal error, but it does make parallelism impossible + !headers[0]!.type.hasMVar then + elabAsync headers[0]! view declId + else elabSync headers + else elabSync headers + for view in views, declId in expandedDeclIds do -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting -- that depends only on a part of the ref - addDeclarationRangesForBuiltin header.declName view.modifiers.stx view.ref + addDeclarationRangesForBuiltin declId.declName view.modifiers.stx view.ref + elabSync headers := do + finishElab headers + processDeriving headers + elabAsync header view declId := do + let env ← getEnv + let async ← env.addConstAsync declId.declName .thm + setEnv async.mainEnv + -- TODO: parallelize header elaboration as well? Would have to refactor auto implicits catch, + -- makes `@[simp]` etc harder? + let type ← withHeaderSecVars vars sc #[header] fun vars => do + mkForallFVars vars header.type >>= instantiateMVars + let allUserLevelNames := getAllUserLevelNames #[header] + let type ← withLevelNames allUserLevelNames <| levelMVarToParam type + -- in the case of theorems, the decl level params are those of the header + let mut s : CollectLevelParams.State := {} + s := collectLevelParams s type + let scopeLevelNames ← getLevelNames + let levelParams ← IO.ofExcept <| sortDeclLevelParams scopeLevelNames allUserLevelNames s.params + async.commitSignature { name := header.declName, levelParams, type } + + -- attributes should be applied on the main thread; see below + let header := { header with modifiers.attrs := #[] } + + -- insert a hole for the proof info trees in the main info tree + let infoHole ← mkFreshMVarId + let infoPromise ← IO.Promise.new + modifyInfoState fun s => { s with + trees := s.trees.push <| .hole infoHole + lazyAssignment := s.lazyAssignment.insert infoHole <| infoPromise.resultD default + } + + -- now start new thread for body elaboration, then nested thread for kernel checking + let cancelTk ← IO.CancelToken.new + let act ← wrapAsyncAsSnapshot (desc := s!"elaborating proof of {declId.declName}") + (cancelTk? := cancelTk) fun _ => do + setEnv async.asyncEnv + try + finishElab #[header] + finally + reportDiag + -- must introduce node to fill `infoHole` with multiple info trees + let info := .ofCustomInfo { stx := header.value, value := .mk (α := AsyncBodyInfo) {} } + infoPromise.resolve <| .node info (← getInfoTrees) + async.commitConst (← getEnv) + let cancelTk ← IO.CancelToken.new + let checkAct ← wrapAsyncAsSnapshot (desc := s!"finishing proof of {declId.declName}") + (cancelTk? := cancelTk) fun _ => do + processDeriving #[header] + async.commitCheckEnv (← getEnv) + let checkTask ← BaseIO.mapTask (t := (← getEnv).checked) checkAct + Core.logSnapshotTask { stx? := none, task := checkTask, cancelTk? := cancelTk } + Core.logSnapshotTask { stx? := none, task := (← BaseIO.asTask (act ())), cancelTk? := cancelTk } + applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking + applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation + finishElab headers := withFunLocalDecls headers fun funFVars => do + for view in views, funFVar in funFVars do + addLocalVarInfo view.declId funFVar + let values ← try + let values ← elabFunValues headers vars sc + Term.synthesizeSyntheticMVarsNoPostponing + values.mapM (instantiateMVarsProfiling ·) + catch ex => + logException ex + headers.mapM fun header => withRef header.declId <| mkLabeledSorry header.type (synthetic := true) (unique := true) + let headers ← headers.mapM instantiateMVarsAtHeader + let letRecsToLift ← getLetRecsToLift + let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift + checkLetRecsToLiftTypes funFVars letRecsToLift + (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc headers else withUsed vars headers values letRecsToLift) fun vars => do + let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift + checkAllDeclNamesDistinct preDefs + for preDef in preDefs do + trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}" + let allUserLevelNames := getAllUserLevelNames headers + let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamTypesPreDecls preDefs + let preDefs ← instantiateMVarsAtPreDecls preDefs + let preDefs ← shareCommonPreDefs preDefs + let scopeLevelNames ← getLevelNames + let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames + for preDef in preDefs do + trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}" + addPreDefinitions preDefs processDeriving (headers : Array DefViewElabHeader) := do for header in headers, view in views do if let some classNamesStx := view.deriving? then diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index 94c6ee45ce..c245c1740c 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -139,14 +139,25 @@ private def betaReduceLetRecApps (preDefs : Array PreDefinition) : MetaM (Array else return preDef -private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do +private def addSorried (preDefs : Array PreDefinition) : TermElabM Unit := do for preDef in preDefs do - let decl := Declaration.axiomDecl { - name := preDef.declName, - levelParams := preDef.levelParams, - type := preDef.type, - isUnsafe := preDef.modifiers.isUnsafe - } + let value ← mkSorry (synthetic := true) preDef.type + let decl := if preDef.kind.isTheorem then + Declaration.thmDecl { + name := preDef.declName, + levelParams := preDef.levelParams, + type := preDef.type, + value + } + else + Declaration.defnDecl { + name := preDef.declName, + levelParams := preDef.levelParams, + type := preDef.type, + hints := .abbrev + safety := .safe + value + } addDecl decl withSaveInfoContext do -- save new env addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true) @@ -306,9 +317,9 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC catch _ => -- Compilation failed try again just as axiom s.restore - addAsAxioms preDefs + addSorried preDefs else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then - addAsAxioms preDefs + addSorried preDefs catch _ => s.restore builtin_initialize diff --git a/src/Lean/Elab/Tactic/AsAuxLemma.lean b/src/Lean/Elab/Tactic/AsAuxLemma.lean index 4c15b42035..3a4370e1b3 100644 --- a/src/Lean/Elab/Tactic/AsAuxLemma.lean +++ b/src/Lean/Elab/Tactic/AsAuxLemma.lean @@ -14,15 +14,14 @@ open Lean Meta Elab Tactic Parser.Tactic @[builtin_tactic as_aux_lemma] def elabAsAuxLemma : Lean.Elab.Tactic.Tactic -| `(tactic| as_aux_lemma => $s) => - liftMetaTactic fun mvarId => do - let (mvars, _) ← runTactic mvarId s - unless mvars.isEmpty do - throwError "Cannot abstract term into auxiliary lemma because there are open goals." - let e ← instantiateMVars (mkMVar mvarId) - let env ← getEnv - -- TODO: this likely should share name creation code with `mkAuxLemma` - let e ← mkAuxTheorem (← mkFreshUserName <| env.asyncPrefix?.getD env.mainModule ++ `_auxLemma) (← mvarId.getType) e - mvarId.assign e - return [] +| `(tactic| as_aux_lemma => $s) => withMainContext do + let mvarId ← getMainGoal + let mvars ← Tactic.run mvarId (evalTactic s) + unless mvars.isEmpty do + throwError "Cannot abstract term into auxiliary lemma because there are open goals." + let e ← instantiateMVars (mkMVar mvarId) + let env ← getEnv + -- TODO: this likely should share name creation code with `mkAuxLemma` + let e ← mkAuxTheorem (← mkFreshUserName <| env.asyncPrefix?.getD env.mainModule ++ `_auxLemma) (← mvarId.getType) e + mvarId.assign e | _ => throwError "Invalid as_aux_lemma syntax" diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index cfeebf2feb..4298ad4b6a 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/src/Lean/Meta/CongrTheorems.lean @@ -414,7 +414,7 @@ def mkHCongrWithArityForConst? (declName : Name) (levels : List Level) (numArgs let suffix := hcongrThmSuffixBasePrefix ++ toString numArgs let thmName := Name.str declName suffix unless (← getEnv).contains thmName do - executeReservedNameAction thmName + let _ ← executeReservedNameAction thmName let proof := mkConst thmName levels let type ← inferType proof let some argKinds := congrKindsExt.find? (← getEnv) thmName @@ -431,7 +431,7 @@ def mkCongrSimpForConst? (declName : Name) (levels : List Level) : MetaM (Option try let thmName := Name.str declName congrSimpSuffix unless (← getEnv).contains thmName do - executeReservedNameAction thmName + let _ ← executeReservedNameAction thmName let proof := mkConst thmName levels let type ← inferType proof let some argKinds := congrKindsExt.find? (← getEnv) thmName diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean index 3784f0abfa..e7cc5c4b08 100644 --- a/src/Lean/Meta/Eqns.lean +++ b/src/Lean/Meta/Eqns.lean @@ -86,9 +86,7 @@ builtin_initialize registerReservedNamePredicate fun env n => | .str p s => (isEqnReservedNameSuffix s || s == unfoldThmSuffix || s == eqUnfoldThmSuffix) && env.isSafeDefinition p - -- Remark: `f.match_.eq_` are private definitions and are not treated as reserved names - -- Reason: `f.match_.splitter is generated at the same time, and can eliminate into type. - -- Thus, it cannot be defined in different modules since it is not a theorem, and is used to generate code. + -- Remark: `f.match_.eq_` are handled separately in `Lean.Meta.Match.MatchEqs`. && !isMatcherCore env p | _ => false @@ -289,7 +287,7 @@ def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) : builtin_initialize registerReservedNameAction fun name => do let .str p s := name | return false - unless (← getEnv).isSafeDefinition p do return false + unless (← getEnv).isSafeDefinition p && !isMatcherCore (← getEnv) p do return false if isEqnReservedNameSuffix s then return (← MetaM.run' <| getEqnsFor? p).isSome if s == unfoldThmSuffix then diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index ffdbfa055b..0aad1a62c6 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -769,4 +769,19 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no builtin_initialize registerTraceClass `Meta.Match.matchEqs +private def isMatchEqName? (env : Environment) (n : Name) : Option Name := do + let .str p s := n | failure + guard <| isEqnReservedNameSuffix s || s == "splitter" + let p ← privateToUserName? p + guard <| isMatcherCore env p + return p + +builtin_initialize registerReservedNamePredicate (isMatchEqName? · · |>.isSome) + +builtin_initialize registerReservedNameAction fun name => do + let some p := isMatchEqName? (← getEnv) name | + return false + let _ ← MetaM.run' <| getEquationsFor p + return true + end Lean.Meta.Match diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index 1f4072644d..aef9006b6c 100644 --- a/src/Lean/MonadEnv.lean +++ b/src/Lean/MonadEnv.lean @@ -78,8 +78,8 @@ def isRec [Monad m] [MonadEnv m] (declName : Name) : m Bool := | ConstantInfo.recInfo val => k val us | _ => failK () -def hasConst [Monad m] [MonadEnv m] (constName : Name) : m Bool := do - return (← getEnv).contains constName +def hasConst [Monad m] [MonadEnv m] (constName : Name) (skipRealize := true) : m Bool := do + return (← getEnv).contains (skipRealize := skipRealize) constName private partial def mkAuxNameAux (env : Environment) (base : Name) (i : Nat) : Name := let candidate := base.appendIndexAfter i diff --git a/src/Lean/ReservedNameAction.lean b/src/Lean/ReservedNameAction.lean index 030891de04..a11e5afbd6 100644 --- a/src/Lean/ReservedNameAction.lean +++ b/src/Lean/ReservedNameAction.lean @@ -31,9 +31,7 @@ Execute a registered reserved action for the given reserved name. Note that the handler can throw an exception. -/ def executeReservedNameAction (name : Name) : CoreM Unit := do - for act in (← reservedNameActionsRef.get) do - if (← act name) then - return () + let _ ← (← reservedNameActionsRef.get).anyM (· name) /-- Similar to `resolveGlobalName`, but also executes reserved name actions. @@ -46,7 +44,9 @@ def realizeGlobalName (id : Name) : CoreM (List (Name × List String)) := do else try executeReservedNameAction c - return (← getEnv).contains c + -- note that even if an action "handled" a name, it may still be undefined, e.g. with an + -- out-of-bounds equation index + return (← getEnv).containsOnBranch c catch ex => -- We record the error produced by the reserved name action generator logError m!"Failed to realize constant {id}:{indentD ex.toMessageData}" diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 8486dcbe9d..9992f4b3f2 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -393,7 +393,7 @@ def setupImports (meta : DocumentMeta) (cmdlineOpts : Options) (chanOut : Std.Ch let opts := cmdlineOpts.mergeBy (fun _ _ fileOpt => fileOpt) fileSetupResult.fileOptions -- default to async elaboration; see also `Elab.async` docs - let opts := Elab.async.setIfNotSet opts true + --let opts := Elab.async.setIfNotSet opts true return .ok { mainModuleName diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index 00fe3b994c..0ab8c071b0 100644 --- a/src/Lean/Structure.lean +++ b/src/Lean/Structure.lean @@ -343,7 +343,7 @@ We use an environment extension to cache resolution orders. These are not expensive to compute, but worth caching, and we save olean storage space. -/ builtin_initialize structureResolutionExt : EnvExtension StructureResolutionState ← - registerEnvExtension (pure {}) + registerEnvExtension (pure {}) (asyncMode := .local) -- mere cache /-- Gets the resolution order if it has already been cached. -/ private def getStructureResolutionOrder? (env : Environment) (structName : Name) : Option (Array Name) := diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h index ee225c1734..923e75e26b 100644 --- a/src/stdlib_flags.h +++ b/src/stdlib_flags.h @@ -22,6 +22,9 @@ options get_default_options() { opts = opts.update({"quotPrecheck"}, true); opts = opts.update({"pp", "rawOnError"}, true); + + // temporarily restrict async to language server used in core, i.e. stage 0 + opts = opts.update({"Elab", "async"}, true); #endif return opts; } diff --git a/tests/lean/run/ack.lean b/tests/lean/run/ack.lean index 11e7f393ea..9143a721a4 100644 --- a/tests/lean/run/ack.lean +++ b/tests/lean/run/ack.lean @@ -5,6 +5,15 @@ def ack : Nat → Nat → Nat termination_by a b => (a, b) /-- +info: [diag] Diagnostics + [kernel] unfolded declarations (max: 1193, num: 5): + [kernel] Nat.casesOn ↦ 1193 + [kernel] Nat.rec ↦ 1065 + [kernel] Eq.ndrec ↦ 973 + [kernel] Eq.rec ↦ 973 + [kernel] Acc.rec ↦ 754 + use `set_option diagnostics.threshold ` to control threshold for reporting counters +--- info: [diag] Diagnostics [reduction] unfolded declarations (max: 2567, num: 5): [reduction] Nat.rec ↦ 2567 diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean index 1d60fef423..82f54483d4 100644 --- a/tests/lean/run/allGoals.lean +++ b/tests/lean/run/allGoals.lean @@ -301,46 +301,46 @@ theorem idEq (a : α) : id a = a := /-- info: case sunday -⊢ Weekday.sunday.previous.next = id Weekday.sunday +⊢ sunday.previous.next = id sunday case monday -⊢ Weekday.monday.previous.next = id Weekday.monday +⊢ monday.previous.next = id monday case tuesday -⊢ Weekday.tuesday.previous.next = id Weekday.tuesday +⊢ tuesday.previous.next = id tuesday case wednesday -⊢ Weekday.wednesday.previous.next = id Weekday.wednesday +⊢ wednesday.previous.next = id wednesday case thursday -⊢ Weekday.thursday.previous.next = id Weekday.thursday +⊢ thursday.previous.next = id thursday case friday -⊢ Weekday.friday.previous.next = id Weekday.friday +⊢ friday.previous.next = id friday case saturday -⊢ Weekday.saturday.previous.next = id Weekday.saturday +⊢ saturday.previous.next = id saturday --- info: case sunday -⊢ Weekday.sunday.previous.next = Weekday.sunday +⊢ sunday.previous.next = sunday case monday -⊢ Weekday.monday.previous.next = Weekday.monday +⊢ monday.previous.next = monday case tuesday -⊢ Weekday.tuesday.previous.next = Weekday.tuesday +⊢ tuesday.previous.next = tuesday case wednesday -⊢ Weekday.wednesday.previous.next = Weekday.wednesday +⊢ wednesday.previous.next = wednesday case thursday -⊢ Weekday.thursday.previous.next = Weekday.thursday +⊢ thursday.previous.next = thursday case friday -⊢ Weekday.friday.previous.next = Weekday.friday +⊢ friday.previous.next = friday case saturday -⊢ Weekday.saturday.previous.next = Weekday.saturday +⊢ saturday.previous.next = saturday -/ #guard_msgs in theorem Weekday.test (d : Weekday) : next (previous d) = id d := by @@ -352,25 +352,25 @@ theorem Weekday.test (d : Weekday) : next (previous d) = id d := by /-- info: case sunday -⊢ Weekday.sunday.previous.next = Weekday.sunday +⊢ sunday.previous.next = sunday case monday -⊢ Weekday.monday.previous.next = Weekday.monday +⊢ monday.previous.next = monday case tuesday -⊢ Weekday.tuesday.previous.next = Weekday.tuesday +⊢ tuesday.previous.next = tuesday case wednesday -⊢ Weekday.wednesday.previous.next = Weekday.wednesday +⊢ wednesday.previous.next = wednesday case thursday -⊢ Weekday.thursday.previous.next = Weekday.thursday +⊢ thursday.previous.next = thursday case friday -⊢ Weekday.friday.previous.next = Weekday.friday +⊢ friday.previous.next = friday case saturday -⊢ Weekday.saturday.previous.next = Weekday.saturday +⊢ saturday.previous.next = saturday -/ #guard_msgs in theorem Weekday.test2 (d : Weekday) : next (previous d) = id d := by diff --git a/tests/lean/run/decideTacticKernel.lean b/tests/lean/run/decideTacticKernel.lean index 4daf8df3f1..ad3756ad30 100644 --- a/tests/lean/run/decideTacticKernel.lean +++ b/tests/lean/run/decideTacticKernel.lean @@ -58,15 +58,14 @@ theorem thm1 : ∀ x < 100, x * x ≤ 10000 := by decide +kernel theorem thm1' : ∀ x < 100, x * x ≤ 10000 := by decide +kernel --- (Note: when run within VS Code, these tests fail since the auxLemmas have a `lean.run` prefix.) /-- info: theorem thm1 : ∀ (x : Nat), x < 100 → x * x ≤ 10000 := -decideTacticKernel._auxLemma.3 +thm1._auxLemma.1 -/ #guard_msgs in #print thm1 /-- info: theorem thm1' : ∀ (x : Nat), x < 100 → x * x ≤ 10000 := -decideTacticKernel._auxLemma.3 +thm1'._auxLemma.1 -/ #guard_msgs in #print thm1' diff --git a/tests/lean/run/eqnsReducible.lean b/tests/lean/run/eqnsReducible.lean index 802683a893..273ce38013 100644 --- a/tests/lean/run/eqnsReducible.lean +++ b/tests/lean/run/eqnsReducible.lean @@ -77,7 +77,7 @@ theorem ex2 : P (semired o) := by simp [semired]; fail /-- info: true -/ #guard_msgs in -run_meta Lean.logInfo m!"{← Lean.hasConst `semired.eq_1}" +run_meta Lean.logInfo m!"{← Lean.hasConst (skipRealize := false) `semired.eq_1}" def semired2 : Option α → Bool | .some _ => true diff --git a/tests/lean/run/grind_attrs.lean b/tests/lean/run/grind_attrs.lean index 67938973f0..5eb965cc8b 100644 --- a/tests/lean/run/grind_attrs.lean +++ b/tests/lean/run/grind_attrs.lean @@ -27,25 +27,19 @@ opaque Expr.eval : Expr → State → Nat axiom Expr.constProp : Expr → State → Expr -/-- -info: [grind.ematch.pattern] Expr.eval_constProp_of_sub: [State.le #3 #2, Expr.constProp #1 #3] --/ +/-- info: [grind.ematch.pattern] eval_constProp_of_sub: [State.le #3 #2, constProp #1 #3] -/ #guard_msgs (info) in set_option trace.grind.ematch.pattern true in @[grind =>] theorem Expr.eval_constProp_of_sub (e : Expr) (h : State.le σ' σ) : (e.constProp σ').eval σ = e.eval σ := sorry -/-- -info: [grind.ematch.pattern] Expr.eval_constProp_of_eq_of_sub: [State.le #3 #2, Expr.constProp #1 #3] --/ +/-- info: [grind.ematch.pattern] eval_constProp_of_eq_of_sub: [State.le #3 #2, constProp #1 #3] -/ #guard_msgs (info) in set_option trace.grind.ematch.pattern true in @[grind =>] theorem Expr.eval_constProp_of_eq_of_sub {e : Expr} (h₂ : State.le σ' σ) : (e.constProp σ').eval σ = e.eval σ := sorry -/-- -info: [grind.ematch.pattern] State.update_le_update: [State.le #4 #3, State.update #4 #2 #1] --/ +/-- info: [grind.ematch.pattern] update_le_update: [le #4 #3, update #4 #2 #1] -/ #guard_msgs (info) in set_option trace.grind.ematch.pattern true in @[grind =>] theorem State.update_le_update (h : State.le σ' σ) : State.le (σ'.update x v) (σ.update x v) := diff --git a/tests/lean/run/info_trees.lean b/tests/lean/run/info_trees.lean index 2ef75ea014..beee048cf9 100644 --- a/tests/lean/run/info_trees.lean +++ b/tests/lean/run/info_trees.lean @@ -3,78 +3,79 @@ -- it is fine to simply remove the `#guard_msgs` and expected output. /-- -info: Try this: exact Nat.zero_le n ---- -info: • command @ ⟨81, 0⟩-⟨81, 40⟩ @ Lean.Elab.Command.elabDeclaration - • Nat : Type @ ⟨81, 15⟩-⟨81, 18⟩ @ Lean.Elab.Term.elabIdent - • [.] Nat : some Sort.{?_uniq.1} @ ⟨81, 15⟩-⟨81, 18⟩ - • Nat : Type @ ⟨81, 15⟩-⟨81, 18⟩ - • n (isBinder := true) : Nat @ ⟨81, 11⟩-⟨81, 12⟩ - • 0 ≤ n : Prop @ ⟨81, 22⟩-⟨81, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2» +info: • command @ ⟨82, 0⟩-⟨82, 40⟩ @ Lean.Elab.Command.elabDeclaration + • Nat : Type @ ⟨82, 15⟩-⟨82, 18⟩ @ Lean.Elab.Term.elabIdent + • [.] Nat : some Sort.{?_uniq.1} @ ⟨82, 15⟩-⟨82, 18⟩ + • Nat : Type @ ⟨82, 15⟩-⟨82, 18⟩ + • n (isBinder := true) : Nat @ ⟨82, 11⟩-⟨82, 12⟩ + • 0 ≤ n : Prop @ ⟨82, 22⟩-⟨82, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2» • Macro expansion 0 ≤ n ===> binrel% LE.le✝ 0 n - • 0 ≤ n : Prop @ ⟨81, 22⟩†-⟨81, 27⟩† @ Lean.Elab.Term.Op.elabBinRel - • 0 ≤ n : Prop @ ⟨81, 22⟩†-⟨81, 27⟩† - • [.] LE.le✝ : none @ ⟨81, 22⟩†-⟨81, 27⟩† - • 0 : Nat @ ⟨81, 22⟩-⟨81, 23⟩ @ Lean.Elab.Term.elabNumLit - • n : Nat @ ⟨81, 26⟩-⟨81, 27⟩ @ Lean.Elab.Term.elabIdent - • [.] n : none @ ⟨81, 26⟩-⟨81, 27⟩ - • n : Nat @ ⟨81, 26⟩-⟨81, 27⟩ - • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨81, 8⟩-⟨81, 9⟩ - • n (isBinder := true) : Nat @ ⟨81, 11⟩-⟨81, 12⟩ - • CustomInfo(Lean.Elab.Term.BodyInfo) - • Tactic @ ⟨81, 31⟩-⟨81, 40⟩ - (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]))) - before ⏎ - n : Nat - ⊢ 0 ≤ n - after no goals - • Tactic @ ⟨81, 31⟩-⟨81, 33⟩ - "by" + • 0 ≤ n : Prop @ ⟨82, 22⟩†-⟨82, 27⟩† @ Lean.Elab.Term.Op.elabBinRel + • 0 ≤ n : Prop @ ⟨82, 22⟩†-⟨82, 27⟩† + • [.] LE.le✝ : none @ ⟨82, 22⟩†-⟨82, 27⟩† + • 0 : Nat @ ⟨82, 22⟩-⟨82, 23⟩ @ Lean.Elab.Term.elabNumLit + • n : Nat @ ⟨82, 26⟩-⟨82, 27⟩ @ Lean.Elab.Term.elabIdent + • [.] n : none @ ⟨82, 26⟩-⟨82, 27⟩ + • n : Nat @ ⟨82, 26⟩-⟨82, 27⟩ + • CustomInfo(Lean.Elab.Term.AsyncBodyInfo) + • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨82, 8⟩-⟨82, 9⟩ + • n (isBinder := true) : Nat @ ⟨82, 11⟩-⟨82, 12⟩ + • CustomInfo(Lean.Elab.Term.BodyInfo) + • Tactic @ ⟨82, 31⟩-⟨82, 40⟩ + (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]))) before ⏎ n : Nat ⊢ 0 ≤ n after no goals - • Tactic @ ⟨81, 34⟩-⟨81, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq - (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])) + • Tactic @ ⟨82, 31⟩-⟨82, 33⟩ + "by" before ⏎ n : Nat ⊢ 0 ≤ n after no goals - • Tactic @ ⟨81, 34⟩-⟨81, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented - (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]) + • Tactic @ ⟨82, 34⟩-⟨82, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq + (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])) before ⏎ n : Nat ⊢ 0 ≤ n after no goals - • Tactic @ ⟨81, 34⟩-⟨81, 40⟩ @ Lean.Elab.LibrarySearch.evalExact - (Tactic.exact? "exact?" []) + • Tactic @ ⟨82, 34⟩-⟨82, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented + (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]) before ⏎ n : Nat ⊢ 0 ≤ n after no goals - • Tactic @ ⟨81, 34⟩†-⟨81, 40⟩† @ Lean.Elab.Tactic.evalExact - (Tactic.exact "exact" (Term.app `Nat.zero_le [`n])) + • Tactic @ ⟨82, 34⟩-⟨82, 40⟩ @ Lean.Elab.LibrarySearch.evalExact + (Tactic.exact? "exact?" []) before ⏎ n : Nat ⊢ 0 ≤ n after no goals - • Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp - • [.] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.36 @ ⟨1, 0⟩†-⟨1, 0⟩† - • Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩† - • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent - • [.] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩† - • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† - • CustomInfo(Lean.Meta.Tactic.TryThis.TryThisInfo) - • UserWidget Lean.Meta.Tactic.TryThis.tryThisWidget - {"suggestions": [{"suggestion": "exact Nat.zero_le n"}], - "style": null, - "range": - {"start": {"line": 80, "character": 34}, "end": {"line": 80, "character": 40}}, - "isInline": true, - "header": "Try this: "} • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨81, 8⟩-⟨81, 9⟩ + • Tactic @ ⟨82, 34⟩†-⟨82, 40⟩† @ Lean.Elab.Tactic.evalExact + (Tactic.exact "exact" (Term.app `Nat.zero_le [`n])) + before ⏎ + n : Nat + ⊢ 0 ≤ n + after no goals + • Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp + • [.] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.37 @ ⟨1, 0⟩†-⟨1, 0⟩† + • Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩† + • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent + • [.] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩† + • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† + • CustomInfo(Lean.Meta.Tactic.TryThis.TryThisInfo) + • UserWidget Lean.Meta.Tactic.TryThis.tryThisWidget + {"suggestions": [{"suggestion": "exact Nat.zero_le n"}], + "style": null, + "range": + {"start": {"line": 81, "character": 34}, "end": {"line": 81, "character": 40}}, + "isInline": true, + "header": "Try this: "} • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨82, 8⟩-⟨82, 9⟩ +--- +info: Try this: exact Nat.zero_le n -/ #guard_msgs in #info_trees in diff --git a/tests/lean/run/variable.lean b/tests/lean/run/variable.lean index c5d12180b2..300d8af97e 100644 --- a/tests/lean/run/variable.lean +++ b/tests/lean/run/variable.lean @@ -122,21 +122,13 @@ variable (a : α) in omit α in theorem t11 (a : α) : True := trivial -/-- -error: cannot omit referenced section variable 'α' ---- -error: cannot omit referenced section variable 'α' --/ +/-- error: cannot omit referenced section variable 'α' -/ #guard_msgs in variable (α : Type) in omit α in theorem t12 (a : α) : True := trivial -/-- -error: cannot omit referenced section variable 'inst✝' ---- -error: cannot omit referenced section variable 'inst✝' --/ +/-- error: cannot omit referenced section variable 'inst✝' -/ #guard_msgs in variable [ToString α] in omit [ToString α] in @@ -165,10 +157,10 @@ omit [ToString Nat] variable (α : Type) in include α in omit α in -theorem t13 : True := trivial +theorem t14 : True := trivial /-- -warning: automatically included section variable(s) unused in theorem 't14': +warning: automatically included section variable(s) unused in theorem 't15': α consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit α in theorem ... @@ -179,7 +171,7 @@ variable (α : Type) in include α in omit α in include α in -theorem t14 : True := trivial +theorem t15 : True := trivial /-! But you probably shouldn't use it -/ @@ -192,4 +184,4 @@ note: this linter can be disabled with `set_option linter.omit false` variable (α : Type) in include α in omit α in -theorem t15 : True := trivial +theorem t16 : True := trivial diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out index db3cdf24fc..c5fa1de371 100644 --- a/tests/lean/shadow.lean.expected.out +++ b/tests/lean/shadow.lean.expected.out @@ -19,7 +19,7 @@ inst✝ inst : α shadow.lean:17:0-17:1: error: don't know how to synthesize placeholder context: α : Type u_1 -inst.78 : Inhabited α +inst.74 : Inhabited α inst inst : α ⊢ {β δ : Type} → α → β → δ → α × β × δ shadow.lean:20:0-20:1: error: don't know how to synthesize placeholder diff --git a/tests/lean/syntaxPrec.lean.expected.out b/tests/lean/syntaxPrec.lean.expected.out index d5bc121d47..98fd14c4eb 100644 --- a/tests/lean/syntaxPrec.lean.expected.out +++ b/tests/lean/syntaxPrec.lean.expected.out @@ -1,10 +1,10 @@ syntaxPrec.lean:1:17-1:21: error: unexpected token '<|>'; expected ':' +[Elab.command] @[term_parser 1000] + def «termFoo*_» : Lean.ParserDescr✝ := + ParserDescr.node✝ `«termFoo*_» 1022 + (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo") + (ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "*" `token.«*» (ParserDescr.symbol✝ "*")) + ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) "," + (ParserDescr.symbol✝ ", ") Bool.false✝))) [Elab.command] syntax "foo" ("*" <|> term,+) : term - [Elab.command] @[term_parser 1000] - def «termFoo*_» : Lean.ParserDescr✝ := - ParserDescr.node✝ `«termFoo*_» 1022 - (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo") - (ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "*" `token.«*» (ParserDescr.symbol✝ "*")) - ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) "," - (ParserDescr.symbol✝ ", ") Bool.false✝))) [Elab.command]