From f47dfe9e7fe203caa1977b2bf41b7c0f30eb2d32 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 16 Jan 2026 10:03:40 +0100 Subject: [PATCH] perf: `Options.hasTrace` (#12001) Drastically speeds up `isTracingEnabledFor` in the common case, which has evolved from "no options set" to "`Elab.async` and probably some linter options set but no `trace`". ## Breaking changes `Lean.Options` is now an opaque type. The basic but not all of the `KVMap` API has been redefined on top of it. --- src/Lean/Compiler/IR/CompilerM.lean | 2 +- src/Lean/Compiler/LCNF/Main.lean | 2 +- src/Lean/Data/Options.lean | 86 ++++++++++++-- src/Lean/DocString/Parser.lean | 2 +- src/Lean/Elab/BuiltinCommand.lean | 2 +- src/Lean/Elab/Deriving/Basic.lean | 2 +- src/Lean/Elab/DocString/Builtin.lean | 2 +- src/Lean/Elab/MutualInductive.lean | 4 +- src/Lean/Elab/SetOption.lean | 2 +- .../Tactic/BVDecide/Frontend/BVDecide.lean | 2 +- src/Lean/Elab/Tactic/Do/Spec.lean | 4 +- src/Lean/Language/Lean.lean | 10 +- src/Lean/Message.lean | 2 +- src/Lean/MetavarContext.lean | 3 - src/Lean/Parser/Extension.lean | 4 +- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 4 +- .../PrettyPrinter/Delaborator/Builtins.lean | 2 +- .../PrettyPrinter/Delaborator/SubExpr.lean | 4 +- .../Delaborator/TopDownAnalyze.lean | 2 +- src/Lean/Shell.lean | 2 +- src/Lean/Util/LeanOptions.lean | 4 +- src/Lean/Util/Trace.lean | 20 +++- src/kernel/trace.cpp | 109 +----------------- src/kernel/trace.h | 9 +- src/util/options.cpp | 21 ++-- src/util/options.h | 68 +---------- stage0/src/stdlib_flags.h | 4 +- tests/lean/625.lean | 2 +- tests/lean/PPRoundtrip.lean | 2 +- tests/lean/run/PPTopDownAnalyze.lean | 2 +- tests/lean/run/Reparen.lean | 2 +- tests/lean/run/meta3.lean | 4 +- tests/lean/run/trace.lean | 8 +- tests/lean/sym/perf_meta_apply.lean | 2 +- tests/lean/sym/perf_sym_apply.lean | 2 +- 35 files changed, 158 insertions(+), 244 deletions(-) diff --git a/src/Lean/Compiler/IR/CompilerM.lean b/src/Lean/Compiler/IR/CompilerM.lean index 975d9bd0bf..5f483682c2 100644 --- a/src/Lean/Compiler/IR/CompilerM.lean +++ b/src/Lean/Compiler/IR/CompilerM.lean @@ -44,7 +44,7 @@ def log (entry : LogEntry) : CompilerM Unit := def tracePrefixOptionName := `trace.compiler.ir private def isLogEnabledFor (opts : Options) (optName : Name) : Bool := - match opts.find optName with + match opts.get? optName with | some (DataValue.ofBool v) => v | _ => opts.getBool tracePrefixOptionName diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean index 52824870e1..dfc963ab9a 100644 --- a/src/Lean/Compiler/LCNF/Main.lean +++ b/src/Lean/Compiler/LCNF/Main.lean @@ -51,7 +51,7 @@ The trace can be viewed with `set_option trace.Compiler.step true`. def checkpoint (stepName : Name) (decls : Array Decl) (shouldCheck : Bool) : CompilerM Unit := do for decl in decls do trace[Compiler.stat] "{decl.name} : {decl.size}" - withOptions (fun opts => opts.setBool `pp.motives.pi false) do + withOptions (fun opts => opts.set `pp.motives.pi false) do let clsName := `Compiler ++ stepName if (← Lean.isTracingEnabledFor clsName) then Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl' decl}" diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean index 57fec1fda6..09edb4239f 100644 --- a/src/Lean/Data/Options.lean +++ b/src/Lean/Data/Options.lean @@ -14,14 +14,72 @@ public section namespace Lean -@[expose] def Options := KVMap +structure Options where + private map : NameMap DataValue + /-- + Whether any option with prefix `trace` is set. This does *not* imply that any of such option is + set to `true` but it does capture the most common case that no such option has ever been touched. + -/ + hasTrace : Bool + +namespace Options + +def empty : Options where + map := {} + hasTrace := false + +@[export lean_options_get_empty] +private def getEmpty (_ : Unit) : Options := .empty -def Options.empty : Options := {} instance : Inhabited Options where - default := {} -instance : ToString Options := inferInstanceAs (ToString KVMap) -instance [Monad m] : ForIn m Options (Name × DataValue) := inferInstanceAs (ForIn _ KVMap _) -instance : BEq Options := inferInstanceAs (BEq KVMap) + default := .empty +instance : ToString Options where + toString o := private toString o.map.toList +instance [Monad m] : ForIn m Options (Name × DataValue) where + forIn o init f := private forIn o.map init f +instance : BEq Options where + beq o1 o2 := private o1.map.beq o2.map +instance : EmptyCollection Options where + emptyCollection := .empty + +@[inline] def find? (o : Options) (k : Name) : Option DataValue := + o.map.find? k + +@[deprecated find? (since := "2026-01-15")] +def find := find? + +@[inline] def get? {α : Type} [KVMap.Value α] (o : Options) (k : Name) : Option α := + o.map.find? k |>.bind KVMap.Value.ofDataValue? + +@[inline] def get {α : Type} [KVMap.Value α] (o : Options) (k : Name) (defVal : α) : α := + o.get? k |>.getD defVal + +@[inline] def getBool (o : Options) (k : Name) (defVal : Bool := false) : Bool := + o.get k defVal + +@[inline] def contains (o : Options) (k : Name) : Bool := + o.map.contains k + +@[inline] def insert (o : Options) (k : Name) (v : DataValue) : Options where + map := o.map.insert k v + hasTrace := o.hasTrace || (`trace).isPrefixOf k + +def set {α : Type} [KVMap.Value α] (o : Options) (k : Name) (v : α) : Options := + o.insert k (KVMap.Value.toDataValue v) + +@[inline] def setBool (o : Options) (k : Name) (v : Bool) : Options := + o.set k v + +def erase (o : Options) (k : Name) : Options where + map := o.map.erase k + -- `erase` is expected to be used even more rarely than `set` so O(n) is fine + hasTrace := o.map.keys.any (`trace).isPrefixOf + +def mergeBy (f : Name → DataValue → DataValue → DataValue) (o1 o2 : Options) : Options where + map := o1.map.mergeWith f o2.map + hasTrace := o1.hasTrace || o2.hasTrace + +end Options structure OptionDecl where name : Name @@ -90,11 +148,11 @@ variable [Monad m] [MonadOptions m] def getBoolOption (k : Name) (defValue := false) : m Bool := do let opts ← getOptions - return opts.getBool k defValue + return opts.get k defValue def getNatOption (k : Name) (defValue := 0) : m Nat := do let opts ← getOptions - return opts.getNat k defValue + return opts.get k defValue class MonadWithOptions (m : Type → Type) where withOptions (f : Options → Options) (x : m α) : m α @@ -108,10 +166,10 @@ instance [MonadFunctor m n] [MonadWithOptions m] : MonadWithOptions n where the term being delaborated should be treated as a pattern. -/ def withInPattern [MonadWithOptions m] (x : m α) : m α := - withOptions (fun o => o.setBool `_inPattern true) x + withOptions (fun o => o.set `_inPattern true) x def Options.getInPattern (o : Options) : Bool := - o.getBool `_inPattern + o.get `_inPattern false /-- A strongly-typed reference to an option. -/ protected structure Option (α : Type) where @@ -131,12 +189,20 @@ protected def get? [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : Op protected def get [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : α := opts.get opt.name opt.defValue +@[export lean_options_get_bool] +private def getBool (opts : Options) (name : Name) (defValue : Bool) : Bool := + opts.get name defValue + protected def getM [Monad m] [MonadOptions m] [KVMap.Value α] (opt : Lean.Option α) : m α := return opt.get (← getOptions) protected def set [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val : α) : Options := opts.set opt.name val +@[export lean_options_update_bool] +private def updateBool (opts : Options) (name : Name) (val : Bool) : Options := + opts.set name val + /-- Similar to `set`, but update `opts` only if it doesn't already contains an setting for `opt.name` -/ protected def setIfNotSet [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val : α) : Options := if opts.contains opt.name then opts else opt.set opts val diff --git a/src/Lean/DocString/Parser.lean b/src/Lean/DocString/Parser.lean index 45dd2fa231..e653313c28 100644 --- a/src/Lean/DocString/Parser.lean +++ b/src/Lean/DocString/Parser.lean @@ -1220,7 +1220,7 @@ Disables the option `doc.verso` while running a parser. public def withoutVersoSyntax (p : Parser) : Parser where fn := adaptUncacheableContextFn - (fun c => { c with options := c.options.setBool `doc.verso false }) + (fun c => { c with options := c.options.set `doc.verso false }) p.fn info := p.info diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index c05a9deb0e..19bb8f2f64 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -456,7 +456,7 @@ where withRef tk <| Meta.check e let e ← Term.levelMVarToParam (← instantiateMVars e) -- TODO: add options or notation for setting the following parameters - withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do + withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.set `smartUnfolding false }) do let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := skipProofs) (skipTypes := skipTypes) logInfoAt tk e diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean index 0f7ee546bf..674678ed97 100644 --- a/src/Lean/Elab/Deriving/Basic.lean +++ b/src/Lean/Elab/Deriving/Basic.lean @@ -232,7 +232,7 @@ def applyDerivingHandlers (className : Name) (typeNames : Array Name) (setExpose withScope (fun sc => { sc with attrs := if setExpose then Unhygienic.run `(Parser.Term.attrInstance| expose) :: sc.attrs else sc.attrs -- Deactivate some linting options that only make writing deriving handlers more painful. - opts := sc.opts.setBool `warn.exposeOnPrivate false + opts := sc.opts.set `warn.exposeOnPrivate false -- When any of the types are private, the deriving handler will need access to the private scope -- and should create private instances. isPublic := !typeNames.any isPrivateName }) do diff --git a/src/Lean/Elab/DocString/Builtin.lean b/src/Lean/Elab/DocString/Builtin.lean index 0f750ab02d..a3d65075d5 100644 --- a/src/Lean/Elab/DocString/Builtin.lean +++ b/src/Lean/Elab/DocString/Builtin.lean @@ -1267,7 +1267,7 @@ def «set_option» (option : Ident) (value : DataValue) : DocM (Block ElabInline pushInfoLeaf <| .ofOptionInfo { stx := option, optionName, declName := decl.declName } validateOptionValue optionName decl value let o ← getOptions - modify fun s => { s with options := o.insert optionName value } + modify fun s => { s with options := o.set optionName value } return .empty /-- diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index 50208ff64a..c131054b9d 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -1210,8 +1210,8 @@ private def applyComputedFields (indViews : Array InductiveView) : CommandElabM computedFields := computedFields.push (declName, computedFieldNames) withScope (fun scope => { scope with opts := scope.opts - |>.setBool `bootstrap.genMatcherCode false - |>.setBool `elaboratingComputedFields true}) <| + |>.set `bootstrap.genMatcherCode false + |>.set `elaboratingComputedFields true}) <| elabCommand <| ← `(mutual $computedFieldDefs* end) liftTermElabM do Term.withDeclName indViews[0]!.declName do diff --git a/src/Lean/Elab/SetOption.lean b/src/Lean/Elab/SetOption.lean index 54fa9261c9..e04043efa0 100644 --- a/src/Lean/Elab/SetOption.lean +++ b/src/Lean/Elab/SetOption.lean @@ -52,7 +52,7 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName } let rec setOption (val : DataValue) : m Options := do validateOptionValue optionName decl val - return (← getOptions).insert optionName val + return (← getOptions).set optionName val match val.isStrLit? with | some str => setOption (DataValue.ofString str) | none => diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index 6eb5a36889..17c509fb4d 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean @@ -309,7 +309,7 @@ where Add an auxiliary declaration. Only used to create constants that appear in our reflection proof. -/ mkAuxDecl (name : Name) (value type : Expr) : CoreM Unit := - withOptions (fun opt => opt.setBool `compiler.extract_closed false) do + withOptions (fun opt => opt.set `compiler.extract_closed false) do addAndCompile <| .defnDecl { name := name, levelParams := [], diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean index 43ad452ab6..33ec89f7be 100644 --- a/src/Lean/Elab/Tactic/Do/Spec.lean +++ b/src/Lean/Elab/Tactic/Do/Spec.lean @@ -41,8 +41,8 @@ public def findSpec (database : SpecTheorems) (wp : Expr) : MetaM SpecTheorem := -- information why the defeq check failed, so we do it again. withOptions (fun o => if o.getBool `trace.Elab.Tactic.Do.spec then - o |>.setBool `pp.universes true - |>.setBool `trace.Meta.isDefEq true + o |>.set `pp.universes true + |>.set `trace.Meta.isDefEq true else o) do withTraceNode `Elab.Tactic.Do.spec (fun _ => return m!"Defeq check for {type} failed.") do diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index 92c1dbfdcb..124d4739bc 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -308,8 +308,8 @@ def setOption (opts : Options) (decl : OptionDecl) (name : Name) (val : String) match decl.defValue with | .ofBool _ => match val with - | "true" => return opts.insert name true - | "false" => return opts.insert name false + | "true" => return opts.set name true + | "false" => return opts.set name false | _ => throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \ it must be true/false" @@ -317,8 +317,8 @@ def setOption (opts : Options) (decl : OptionDecl) (name : Name) (val : String) let some val := val.toNat? | throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \ it must be a natural number" - return opts.insert name val - | .ofString _ => return opts.insert name val + return opts.set name val + | .ofString _ => return opts.set name val | _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \ cannot be set in the command line, use set_option command" @@ -342,7 +342,7 @@ def reparseOptions (opts : Options) : IO Options := do If the option is defined in a library, use '-D{`weak ++ name}' to set it conditionally" let .ofString val := val - | opts' := opts'.insert name val -- Already parsed + | opts' := opts'.set name val -- Already parsed opts' ← setOption opts' decl name val diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index af9962210b..ef5fed52e9 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -247,7 +247,7 @@ def ofConstName (constName : Name) (fullNames : Bool := false) : MessageData := let msg ← ofFormatWithInfos <$> match ctx? with | .none => pure (format constName) | .some ctx => - let ctx := if fullNames then { ctx with opts := ctx.opts.insert `pp.fullNames fullNames } else ctx + let ctx := if fullNames then { ctx with opts := ctx.opts.set `pp.fullNames fullNames } else ctx ppConstNameWithInfos ctx constName return Dynamic.mk msg) (fun _ => false) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 9bee3b41c6..cc600d2480 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -786,9 +786,6 @@ def localDeclDependsOnPred [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (pf : namespace MetavarContext -@[export lean_mk_metavar_ctx] -def mkMetavarContext : Unit → MetavarContext := fun _ => {} - /-- Low level API for adding/declaring metavariable declarations. It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`. It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique". -/ diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 86a304be4f..404cab01eb 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -387,7 +387,7 @@ register_builtin_option internal.parseQuotWithCurrentStage : Bool := { def evalInsideQuot (declName : Name) : Parser → Parser := withFn fun f c s => if c.quotDepth > 0 && !c.suppressInsideQuot && internal.parseQuotWithCurrentStage.get c.options && c.env.contains declName then adaptUncacheableContextFn (fun ctx => - { ctx with options := ctx.options.setBool `interpreter.prefer_native false }) + { ctx with options := ctx.options.set `interpreter.prefer_native false }) (evalParserConst declName) c s else f c s @@ -717,7 +717,7 @@ def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s => Id.run do adaptUncacheableContextFn (fun ctx => -- static quotations such as `(e) do not use the interpreter unless the above option is set, -- so for consistency neither should dynamic quotations using this function - { ctx with options := ctx.options.setBool `interpreter.prefer_native (!internal.parseQuotWithCurrentStage.get ctx.options) }) + { ctx with options := ctx.options.set `interpreter.prefer_native (!internal.parseQuotWithCurrentStage.get ctx.options) }) (evalParserConst parserName) ctx s | [.alias alias] => match alias with diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index d597eff3e3..ea6d342f8f 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -165,7 +165,7 @@ def getOptionsAtCurrPos : DelabM Options := do let mut opts ← getOptions if let some opts' := ctx.optionsPerPos.get? (← getPos) then for (k, v) in opts' do - opts := opts.insert k v + opts := opts.set k v return opts /-- Evaluate option accessor, using subterm-specific options if set. -/ @@ -185,7 +185,7 @@ def withOptionAtCurrPos (k : Name) (v : DataValue) (x : DelabM α) : DelabM α : let pos ← getPos withReader (fun ctx => - let opts' := ctx.optionsPerPos.get? pos |>.getD {} |>.insert k v + let opts' := ctx.optionsPerPos.get? pos |>.getD {} |>.set k v { ctx with optionsPerPos := ctx.optionsPerPos.insert pos opts' }) x diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index ae00cacc43..3457a9baf8 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -142,7 +142,7 @@ def withMDataOptions [Inhabited α] (x : DelabM α) : DelabM α := do for (k, v) in m do if (`pp).isPrefixOf k then let opts := posOpts.get? pos |>.getD {} - posOpts := posOpts.insert pos (opts.insert k v) + posOpts := posOpts.insert pos (opts.set k v) withReader ({ · with optionsPerPos := posOpts }) $ withMDataExpr x | _ => x diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean index 9379a63c0f..777c86b658 100644 --- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean +++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean @@ -22,11 +22,11 @@ abbrev OptionsPerPos := Std.TreeMap SubExpr.Pos Options def OptionsPerPos.insertAt (optionsPerPos : OptionsPerPos) (pos : SubExpr.Pos) (name : Name) (value : DataValue) : OptionsPerPos := let opts := optionsPerPos.get? pos |>.getD {} - optionsPerPos.insert pos <| opts.insert name value + optionsPerPos.insert pos <| opts.set name value /-- Merges two collections of options, where the second overrides the first. -/ def OptionsPerPos.merge : OptionsPerPos → OptionsPerPos → OptionsPerPos := - Std.TreeMap.mergeWith (fun _ => KVMap.mergeBy (fun _ _ dv => dv)) + Std.TreeMap.mergeWith (fun _ => Options.mergeBy (fun _ _ dv => dv)) namespace SubExpr diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 790ceaaf34..ce42c33ac4 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -317,7 +317,7 @@ def checkKnowsType : AnalyzeM Unit := do throw $ Exception.internal analyzeFailureId def annotateBoolAt (n : Name) (pos : Pos) : AnalyzeM Unit := do - let opts := (← get).annotations.getD pos {} |>.setBool n true + let opts := (← get).annotations.getD pos {} |>.set n true trace[pp.analyze.annotate] "{pos} {n}" modify fun s => { s with annotations := s.annotations.insert pos opts } diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean index e39a8b9f94..628cc9634c 100644 --- a/src/Lean/Shell.lean +++ b/src/Lean/Shell.lean @@ -284,7 +284,7 @@ def setConfigOption (opts : Options) (arg : String) : IO Options := do else -- More options may be registered by imports, so we leave validating them to the elaborator. -- This (minor) duplication may be resolved later. - return opts.insert name val + return opts.set name val /-- Process a command-line option parsed by the C++ shell. diff --git a/src/Lean/Util/LeanOptions.lean b/src/Lean/Util/LeanOptions.lean index 2d174804d6..7db635bd35 100644 --- a/src/Lean/Util/LeanOptions.lean +++ b/src/Lean/Util/LeanOptions.lean @@ -100,9 +100,9 @@ def LeanOptions.appendArray (self : LeanOptions) (new : Array LeanOption) : Lean instance : HAppend LeanOptions (Array LeanOption) LeanOptions := ⟨LeanOptions.appendArray⟩ def LeanOptions.toOptions (leanOptions : LeanOptions) : Options := Id.run do - let mut options := KVMap.empty + let mut options := Options.empty for ⟨name, optionValue⟩ in leanOptions.values do - options := options.insert name optionValue.toDataValue + options := options.set name optionValue.toDataValue return options def LeanOptions.fromOptions? (options : Options) : Option LeanOptions := do diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 549a4c1f80..bb8e81ba87 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -102,8 +102,8 @@ def printTraces : m Unit := do def resetTraceState : m Unit := modifyTraceState (fun _ => {}) -def checkTraceOption (inherited : Std.HashSet Name) (opts : Options) (cls : Name) : Bool := - !opts.isEmpty && go (`trace ++ cls) +@[inline] def checkTraceOption (inherited : Std.HashSet Name) (opts : Options) (cls : Name) : Bool := + opts.hasTrace && go (`trace ++ cls) where go (opt : Name) : Bool := if let some enabled := opts.get? opt then @@ -117,6 +117,15 @@ where def isTracingEnabledFor (cls : Name) : m Bool := do return checkTraceOption (← MonadTrace.getInheritedTraceOptions) (← getOptions) cls +@[export lean_is_trace_class_enabled] +private def isTracingEnabledForExport (opts : Options) (cls : Name) : BaseIO Bool := do + -- Replicate `checkTraceOption` fast path to make sure it happens before `IORef.get` (which + -- itself is slower than `MonadTrace.getInheritedTraceOptions` but at least that's only on the + -- slow path). + if !opts.hasTrace then + return false + return checkTraceOption (← inheritedTraceOptions.get) opts cls + @[inline] def getTraces : m (PersistentArray TraceElem) := do let s ← getTraceState pure s.traces @@ -265,6 +274,8 @@ def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls : (msg : Except ε α → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do let _ := always.except let opts ← getOptions + if !opts.hasTrace then + return (← k) let clsEnabled ← isTracingEnabledFor cls unless clsEnabled || trace.profiler.get opts do return (← k) @@ -374,6 +385,8 @@ def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m] (msg : Unit → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do let _ := always.except let opts ← getOptions + if !opts.hasTrace then + return (← k) let clsEnabled ← isTracingEnabledFor cls unless clsEnabled || trace.profiler.get opts do return (← k) @@ -415,4 +428,7 @@ def addTraceAsMessages [Monad m] [MonadRef m] [MonadLog m] [MonadTrace m] : m Un let data := .tagged `trace <| .trace { cls := .anonymous } .nil traceMsg logMessage <| Elab.mkMessageCore (← getFileName) (← getFileMap) data .information pos endPos +builtin_initialize + registerTraceClass `debug + end Lean diff --git a/src/kernel/trace.cpp b/src/kernel/trace.cpp index 2ff7de3950..4a1c4f65a3 100644 --- a/src/kernel/trace.cpp +++ b/src/kernel/trace.cpp @@ -13,113 +13,26 @@ Author: Leonardo de Moura #include "kernel/trace.h" namespace lean { -static name_set * g_trace_classes = nullptr; -static name_map * g_trace_aliases = nullptr; -MK_THREAD_LOCAL_GET_DEF(std::vector, get_enabled_trace_classes); -MK_THREAD_LOCAL_GET_DEF(std::vector, get_disabled_trace_classes); -LEAN_THREAD_PTR(elab_environment, g_env); -LEAN_THREAD_PTR(options, g_opts); +LEAN_THREAD_PTR(const options, g_opts); void register_trace_class(name const & n, name const & decl_name) { register_option(name("trace") + n, decl_name, data_value_kind::Bool, "false", "(trace) enable/disable tracing for the given module and submodules"); - g_trace_classes->insert(n); -} - -void register_trace_class_alias(name const & n, name const & alias) { - name_set new_s; - if (auto s = g_trace_aliases->find(n)) - new_s = *s; - new_s.insert(alias); - g_trace_aliases->insert(n, new_s); -} - -bool is_trace_enabled() { - return !get_enabled_trace_classes().empty(); -} - -static void update_class(std::vector & cs, name const & c) { - if (std::find(cs.begin(), cs.end(), c) == cs.end()) { - cs.push_back(c); - } -} - -static void enable_trace_class(name const & c) { - update_class(get_enabled_trace_classes(), c); -} - -static void disable_trace_class(name const & c) { - update_class(get_disabled_trace_classes(), c); -} - -static bool is_trace_class_set_core(std::vector const & cs, name const & n) { - for (name const & p : cs) { - if (is_prefix_of(p, n)) { - return true; - } - } - return false; -} - -static bool is_trace_class_set(std::vector const & cs, name const & n) { - if (is_trace_class_set_core(cs, n)) - return true; - auto it = n; - while (true) { - if (auto s = g_trace_aliases->find(it)) { - bool found = false; - s->for_each([&](name const & alias) { - if (!found && is_trace_class_set_core(cs, alias)) - found = true; - }); - if (found) - return true; - } - if (it.is_atomic()) - return false; - it = it.get_prefix(); - } } +extern "C" bool lean_is_trace_class_enabled(obj_arg opts, obj_arg cls); bool is_trace_class_enabled(name const & n) { - if (!is_trace_enabled()) - return false; - if (is_trace_class_set(get_disabled_trace_classes(), n)) - return false; // it was explicitly disabled - return is_trace_class_set(get_enabled_trace_classes(), n); + return lean_is_trace_class_enabled(g_opts->to_obj_arg(), n.to_obj_arg()); } -void scope_trace_env::init(elab_environment * env, options * opts) { - m_enable_sz = get_enabled_trace_classes().size(); - m_disable_sz = get_disabled_trace_classes().size(); - m_old_env = g_env; - m_old_opts = g_opts; - g_env = env; - name trace("trace"); - if (opts && g_opts != opts) { - opts->for_each([&](name const & n) { - if (is_prefix_of(trace, n)) { - name cls = n.replace_prefix(trace, name()); - if (opts->get_bool(n, false)) - enable_trace_class(cls); - else - disable_trace_class(cls); - } - }); - } - g_opts = opts; -} - scope_trace_env::scope_trace_env(elab_environment const & env, options const & o) { - init(const_cast(&env), const_cast(&o)); + m_old_opts = g_opts; + g_opts = &o; } scope_trace_env::~scope_trace_env() { - g_env = const_cast(m_old_env); g_opts = const_cast(m_old_opts); - get_enabled_trace_classes().resize(m_enable_sz); - get_disabled_trace_classes().resize(m_disable_sz); } extern "C" obj_res lean_io_eprint(obj_arg s); @@ -140,21 +53,9 @@ std::ostream & operator<<(std::ostream & ios, tclass const & c) { } void initialize_trace() { - g_trace_classes = new name_set(); - g_trace_aliases = new name_map(); - - register_trace_class(name{"debug"}); } void finalize_trace() { - delete g_trace_classes; - delete g_trace_aliases; } -/* -@[export lean_mk_metavar_ctx] -def mkMetavarContext : Unit → MetavarContext := fun _ => {} -*/ -extern "C" lean_object* lean_mk_metavar_ctx(lean_object*); - } diff --git a/src/kernel/trace.h b/src/kernel/trace.h index 79c9755b69..78bc65e08e 100644 --- a/src/kernel/trace.h +++ b/src/kernel/trace.h @@ -13,16 +13,9 @@ Author: Leonardo de Moura namespace lean { void register_trace_class(name const & n, name const & decl_name = {}); -void register_trace_class_alias(name const & n, name const & alias); -bool is_trace_enabled(); bool is_trace_class_enabled(name const & n); -#define lean_is_trace_enabled(CName) (::lean::is_trace_enabled() && ::lean::is_trace_class_enabled(CName)) - class scope_trace_env { - unsigned m_enable_sz; - unsigned m_disable_sz; - elab_environment const * m_old_env; options const * m_old_opts; void init(elab_environment * env, options * opts); public: @@ -47,7 +40,7 @@ tout & operator<<(tout const & out, T const & t) { std::ostream & operator<<(std::ostream & ios, tclass const &); #define lean_trace(CName, CODE) { \ -if (lean_is_trace_enabled(CName)) { \ +if (lean::is_trace_class_enabled(CName)) { \ tout() << tclass(CName); CODE \ }} diff --git a/src/util/options.cpp b/src/util/options.cpp index 272dd9b72f..3d4200e4f2 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -61,19 +61,16 @@ extern "C" LEAN_EXPORT obj_res lean_internal_get_default_options(obj_arg) { return get_default_options().steal(); } -options join(options const & opts1, options const & opts2) { - kvmap r = opts2.m_value; - for (kvmap_entry const & e : opts1.m_value) { - if (!opts2.contains(e.fst())) { - r = cons(e, r); - } - } - return options(r); +extern "C" LEAN_EXPORT obj_res lean_options_get_empty(); +options::options(): object_ref(lean_options_get_empty()) {} + +extern "C" LEAN_EXPORT bool lean_options_get_bool(obj_arg opts, obj_arg n, bool default_value); +bool options::get_bool(name const & n, bool default_value) const { + return lean_options_get_bool(this->to_obj_arg(), n.to_obj_arg(), default_value); } -void options::for_each(std::function const & fn) const { - for (kvmap_entry const & e : m_value) { - fn(e.fst()); - } +extern "C" LEAN_EXPORT obj_res lean_options_update_bool(obj_arg opts, obj_arg n, bool v); +options options::update(name const & n, bool v) const { + return options(lean_options_update_bool(this->to_obj_arg(), n.to_obj_arg(), v)); } } diff --git a/src/util/options.h b/src/util/options.h index f1908f8b55..84f22c6203 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -11,65 +11,13 @@ Author: Leonardo de Moura namespace lean { /** \brief Configuration options. */ -class options { - kvmap m_value; - options(kvmap const & v):m_value(v) {} +class options : public object_ref { public: - options() {} - explicit options(obj_arg o):m_value(o) {} - options(b_obj_arg o, bool v):m_value(o, v) {} - options(options const & o):m_value(o.m_value) {} - options(options && o) noexcept:m_value(std::move(o.m_value)) {} - options(name const & n, bool v) { *this = update(n, v); } - options & operator=(options const & o) { m_value = o.m_value; return *this; } - - bool empty() const { return is_nil(m_value); } - unsigned size() const { return length(m_value); } - bool contains(name const & n) const { return static_cast(find(m_value, n)); } - bool contains(char const * n) const { return contains(name(n)); } - - bool get_bool(name const & n, bool default_value = false) const { - if (auto r = ::lean::get_bool(m_value, n)) - return *r; - return default_value; - } - - unsigned get_unsigned(name const & n, unsigned default_value = 0) const { - if (auto r = ::lean::get_nat(m_value, n)) - if (r->is_small()) - return r->get_small_value(); - return default_value; - } - - char const * get_string(name const & n, char const * default_value = nullptr) const { - if (auto r = ::lean::get_string(m_value, n)) - return r->data(); // unsafe - return default_value; - } - - options update(name const & n, unsigned v) const { return options(set_nat(m_value, n, v)); } - options update(name const & n, bool v) const { return options(set_bool(m_value, n, v)); } - options update(name const & n, char const * v) const { return options(set_string(m_value, n, v)); } - - void for_each(std::function const & fn) const; - - options update_if_undef(name const & n, bool v) const { - if (contains(n)) - return *this; - else - return update(n, v); - } - - friend bool is_eqp(options const & a, options const & b) { return a.m_value.raw() == b.m_value.raw(); } - - /** - \brief Combine the options opts1 and opts2. The assignment in - opts2 overrides the ones in opts1. - */ - friend options join(options const & opts1, options const & opts2); - - object * steal() { return m_value.steal(); } - object * to_obj_arg() const { return m_value.to_obj_arg(); } + options(); + explicit options(obj_arg o): object_ref(o) {} + bool get_bool(name const & n, bool default_value = false) const; + options update(name const & n, bool v) const; + friend bool is_eqp(options const & a, options const & b) { return a.raw() == b.raw(); } }; LEAN_EXPORT bool get_verbose(options const & opts); @@ -77,10 +25,6 @@ LEAN_EXPORT name const & get_verbose_opt_name(); LEAN_EXPORT name const & get_max_memory_opt_name(); LEAN_EXPORT name const & get_timeout_opt_name(); -inline options operator+(options const & opts1, options const & opts2) { - return join(opts1, opts2); -} - struct mk_option_declaration { mk_option_declaration(name const & n, data_value_kind k, char const * default_value, char const * description); }; diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..cbd1f3a8c2 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -11,12 +11,12 @@ options get_default_options() { opts = opts.update({"debug", "terminalTacticsAsSorry"}, false); // switch to `true` for ABI-breaking changes affecting meta code; // see also next option! - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `false` when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this is usually the case, but setting // both to `true` may be necessary for handling non-builtin parsers with // builtin elaborators - opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true); + opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); // changes to builtin parsers may also require toggling the following option if macros/syntax // with custom precheck hooks were affected opts = opts.update({"quotPrecheck"}, true); diff --git a/tests/lean/625.lean b/tests/lean/625.lean index 40cc37780e..697bf8a6b4 100644 --- a/tests/lean/625.lean +++ b/tests/lean/625.lean @@ -11,7 +11,7 @@ def x : PUnit := () formatTerm (← delab e) #eval do - let opts := ({}: Options).setBool `pp.universes true + let opts := ({}: MData).set `pp.universes true -- the MData annotation should make it not a regular application, -- so the unexpander should not be called. let e : Expr := mkApp (mkMData opts $ mkConst `foo [levelOne]) (mkConst `x) diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index ddfe7acfbe..e541076279 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -58,7 +58,7 @@ section #eval checkM `(id Nat) #eval checkM `(Sum Nat Nat) end -#eval checkM `(id (id Nat)) (Std.TreeMap.empty.insert (SubExpr.Pos.ofArray #[1]) $ KVMap.empty.insert `pp.explicit true) +#eval checkM `(id (id Nat)) (Std.TreeMap.empty.insert (SubExpr.Pos.ofArray #[1]) $ Options.empty.set `pp.explicit true) -- specify the expected type of `a` in a way that is not erased by the delaborator def typeAs.{u} (α : Type u) (a : α) := () diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index 975ce50b85..c78d571a3f 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -29,7 +29,7 @@ def checkDelab (e : Expr) (tgt? : Option Term) (name? : Option Name := none) : T pure e' catch ex => throwError "{pfix} failed to re-elaborate,\n{stx}\n{← ex.toMessageData.toString}" - withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `pp.all true }) do + withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.set `pp.all true }) do if not (← isDefEq e e') then println! "{pfix} {← inferType e} {← inferType e'}" throwError "{pfix} roundtrip not structurally equal\n\nOriginal: {e}\n\nSyntax: {stx}\n\nNew: {e'}" diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean index 983403aca9..27aaf3975c 100644 --- a/tests/lean/run/Reparen.lean +++ b/tests/lean/run/Reparen.lean @@ -39,7 +39,7 @@ IO.print s; let cmds := (stx.raw.getArg 1).getArgs; cmds.forM $ fun cmd => do let cmd := unparen cmd; - let (cmd, _) ← (tryFinally (PrettyPrinter.parenthesizeCommand cmd) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug, fileName := "", fileMap := default } { env := env }; + let (cmd, _) ← (tryFinally (PrettyPrinter.parenthesizeCommand cmd) printTraces).toIO { options := Options.empty.set `trace.PrettyPrinter.parenthesize debug, fileName := "", fileMap := default } { env := env }; let some s ← pure cmd.reprint | throw $ IO.userError "cmd reprint failed"; IO.print s diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean index 58d452c441..9cc5dd2fc4 100644 --- a/tests/lean/run/meta3.lean +++ b/tests/lean/run/meta3.lean @@ -5,8 +5,8 @@ open Lean.Meta def dbgOpt : Options := let opt : Options := {}; -let opt := opt.setBool `trace.Meta true; --- let opt := opt.setBool `trace.Meta.check false; +let opt := opt.set `trace.Meta true; +-- let opt := opt.set `trace.Meta.check false; opt def print (msg : MessageData) : MetaM Unit := do diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean index 77d8d9a3ef..8fdc4af3aa 100644 --- a/tests/lean/run/trace.lean +++ b/tests/lean/run/trace.lean @@ -46,10 +46,10 @@ withReader (fun ctx => -- Try commenting/uncommeting the following `setBool`s let opts := ctx.options; - let opts := opts.setBool `trace.module true; - -- let opts := opts.setBool `trace.module.aux false; - let opts := opts.setBool `trace.bughunt true; - -- let opts := opts.setBool `trace.slow true; + let opts := opts.set `trace.module true; + -- let opts := opts.set `trace.module.aux false; + let opts := opts.set `trace.bughunt true; + -- let opts := opts.set `trace.slow true; { ctx with options := opts }) (tryCatch (tryFinally x printTraces) (fun _ => IO.println "ERROR")) diff --git a/tests/lean/sym/perf_meta_apply.lean b/tests/lean/sym/perf_meta_apply.lean index 41c6b1f56a..858906b57f 100644 --- a/tests/lean/sym/perf_meta_apply.lean +++ b/tests/lean/sym/perf_meta_apply.lean @@ -2,7 +2,7 @@ import Lean.Meta.Tactic open Lean Meta def profileM {α : Type} (k : MetaM α) (msg : String := "experiment") : MetaM α := - profileitM Exception msg ({ : Options }.setBool `profiler true |>.setNat `profiler.threshold 0) k + profileitM Exception msg ({ : Options }.set `profiler true |>.setNat `profiler.threshold 0) k def genTerm (n : Nat) : Expr := Id.run do let mut e := mkConst ``True diff --git a/tests/lean/sym/perf_sym_apply.lean b/tests/lean/sym/perf_sym_apply.lean index b5db8d9151..4ef2bb804e 100644 --- a/tests/lean/sym/perf_sym_apply.lean +++ b/tests/lean/sym/perf_sym_apply.lean @@ -3,7 +3,7 @@ import Lean.Meta.Sym open Lean Meta Sym def profileM {α : Type} (k : MetaM α) (msg : String := "experiment") : MetaM α := - profileitM Exception msg ({ : Options }.setBool `profiler true |>.setNat `profiler.threshold 0) k + profileitM Exception msg ({ : Options }.set `profiler true |>.setNat `profiler.threshold 0) k def genTerm (n : Nat) : Expr := Id.run do let mut e := mkConst ``True