version: nightly-2021-03-21

lean4_options

#[(smartUnfolding,
  true, []: when computing weak head normal form, use auxiliary definition created for functions defined by structural recursion),
 (trace.compiler.stage1, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.PrettyPrinter.format, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.let, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.letrec, false, [trace]: enable/disable tracing for the given module and submodules),
 (bootstrap.genMatcherCode, true, [bootstrap]: disable code generation for auxiliary matcher function),
 (trace.compiler, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.PrettyPrinter.delab, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.Match, false, [trace]: enable/disable tracing for the given module and submodules),
 (pp.all,
  false, [pp]: (pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universes, and disable beta reduction and notations during pretty printing),
 (pp.notation,
  true, [pp]: (pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)),
 (trace.Meta.appBuilder, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.compiler.spec_info, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.Meta.sizeOf, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.info, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.struct, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.isDefEq, false, [trace]: enable/disable tracing for the given module and submodules),
 (pp.macroStack, false, [pp]: dispaly macro expansion stack),
 (trace.compiler.simp_detail, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.compiler.eta_expand, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.compiler.ir.simp_case, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.Meta.Tactic.cases, false, [trace]: enable/disable tracing for the given module and submodules),
 (printMessageEndPos, false, []: print end position of each message in addition to start position),
 (trace.compiler.lcnf, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.compiler.ir.rc, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.Elab, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.isLevelDefEq, false, [trace]: enable/disable tracing for the given module and submodules),
 (synthInstance.maxHeartbeats,
  500, []: maximum amount of heartbeats per typeclass resolution problem. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit),
 (trace.compiler.extract_closed, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.debug, false, []: (trace) enable/disable tracing for the given module and submodules),
 (maxCoeSize, 16, []: maximum number of instances used to construct an automatic coercion),
 (autoBoundImplicitLocal,
  true, []: Unbound local variables in declaration headers become implicit arguments if they are a lower case or greek letter followed by numeric digits. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}.),
 (pp.structure_projections, true, [pp]: (pretty printer) display structure projections using field notation),
 (trace.Meta.synthInstance.newSubgoal, false, [trace]: enable/disable tracing for the given module and submodules),
 (maxRecDepth, 512, []: maximum recursion depth for many Lean procedures),
 (pp.inaccessibleNames, false, [pp]: display inaccessible declarations in the local context),
 (trace.Meta.isDefEq.constApprox, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.Deriving.beq, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.Deriving.inhabited, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.compiler.erase_irrelevant, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.Meta.check, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.tactic, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.whnf, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.compiler.ir.init, false, []: (trace) enable/disable tracing for the given module and submodules),
 (pp.explicit, false, [pp]: (pretty printer) display implicit arguments),
 (trace.compiler.llnf, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.Elab.do, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.compiler.ir.elim_dead_branches, false, []: (trace) enable/disable tracing for the given module and submodules),
 (format.unicode, true, []: unicode characters),
 (trace.Meta.isDefEq.hint, false, [trace]: enable/disable tracing for the given module and submodules),
 (pp.raw, false, [pp]: (pretty printer) print raw expression/syntax tree),
 (trace.compiler.simp, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.Meta.Tactic.subst, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.synthInstance.generate, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.syntax, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.isDefEq.foApprox, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.postpone, false, [trace]: enable/disable tracing for the given module and submodules),
 (pp.auxDecls, false, [pp]: display auxiliary declarations used to compile recursive functions),
 (hygienicIntro, true, [tactic]: make sure 'intro'-like tactics are hygienic),
 (pp.raw.maxDepth, 32, [pp]: (pretty printer) maximum `Syntax` depth for raw printer),
 (trace.compiler.stage2, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.Meta, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.cases, false, [trace]: enable/disable tracing for the given module and submodules),
 (maxUniverseOffset, 32, []: maximum universe level offset),
 (profiler.threshold,
  0, []: (profiler) threshold in milliseconds, profiling times under threshold will not be reported),
 (trace.Elab.match_syntax.result, false, [trace]: enable/disable tracing for the given module and submodules),
 (format.width, 120, []: indentation),
 (trace.Elab.match_syntax, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.PrettyPrinter, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.compiler.cce, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.PrettyPrinter.parenthesize, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.isDefEq.assign, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.Tactic.simp, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.Tactic.induction, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.Match.unify, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.compiler.ir, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.compiler.result, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.compiler.simp_float_cases, false, []: (trace) enable/disable tracing for the given module and submodules),
 (pp.structure_instance_type, false, [pp]: (pretty printer) display type of structure instances),
 (trace.Elab.Deriving.decEq, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.app, false, [trace]: enable/disable tracing for the given module and submodules),
 (codegen, true, []: (compiler) enable/disable code generation),
 (pp.coercions, true, [pp]: (pretty printer) hide coercion applications),
 (trace.Elab.coe, false, [trace]: enable/disable tracing for the given module and submodules),
 (pp.full_names, false, [pp]: (pretty printer) display fully qualified names),
 (trace.compiler.simp_app_args, false, []: (trace) enable/disable tracing for the given module and submodules),
 (bootstrap.inductiveCheckResultingUniverse,
  true, [bootstrap]: by default the `inductive/structure commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into `Prop`. In the `Init` package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator),
 (trace.compiler.optimize_bytecode, false, []: (trace) enable/disable tracing for the given module and submodules),
 (pp.private_names, false, [pp]: (pretty printer) display internal names assigned to private declarations),
 (trace.Meta.Match.match, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.synthInstance.tryResolve, false, [trace]: enable/disable tracing for the given module and submodules),
 (pp.raw.showInfo, false, [pp]: (pretty printer) print `SourceInfo` metadata with raw printer),
 (trace.Elab.definition, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.compiler.lambda_pure, false, []: (trace) enable/disable tracing for the given module and submodules),
 (maxHeartbeats,
  50000, []: maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit),
 (trace.compiler.ir.reset_reuse, false, []: (trace) enable/disable tracing for the given module and submodules),
 (synthInstance.maxSize,
  128, []: maximum number of instances used to construct a solution in the type class instance synthesis procedure),
 (trace.compiler.lambda_lifting, false, []: (trace) enable/disable tracing for the given module and submodules),
 (pp.universes, false, [pp]: (pretty printer) display universes),
 (match.ignoreUnusedAlts, false, []: if true, do not generate error if an alternative is not used),
 (trace.Debug.Meta.Tactic.simp, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.inductive, false, [trace]: enable/disable tracing for the given module and submodules),
 (compiler.extract_closed, true, []: (compiler) enable/disable closed term caching),
 (hygiene,
  true, []: Annotate identifiers in quotations such that they are resolved relative to the scope at their declaration, not that at their eventual use/expansion, to avoid accidental capturing. Note that quotations/notations already defined are unaffected.),
 (trace.compiler.cse, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.Elab.Deriving, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.synthInstance.resume, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.isDefEq.step, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.synthInstance.globalInstances, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.compiler.ir.result, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.compiler.code_gen, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.compiler.spec_candidate, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.Meta.isLevelDefEq.step, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.command, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.structure, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.definition.structural, false, [trace]: enable/disable tracing for the given module and submodules),
 (genSizeOf, true, []: generate `SizeOf` instance for inductive types and structures),
 (trace.Meta.typeError, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.isLevelDefEq.postponed, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.compiler.ir.expand_reset_reuse, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.compiler.struct_cases_on, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.Meta.debug, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.match, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.compiler.specialize, false, []: (trace) enable/disable tracing for the given module and submodules),
 (pp.structure_instances,
  true, [pp]: (pretty printer) display structure instances using the '{ fieldName := fieldValue, ... }' notation or '⟨fieldValue, ... ⟩' if structure is tagged with [pp_using_anonymous_constructor] attribute),
 (autoLift, true, []: insert monadic lifts (i.e., `liftM` and `liftCoeM`) when needed),
 (pp.sanitizeNames, true, [pp]: add suffix '_{<idx>}' to shadowed/inaccessible variables when pretty printing),
 (trace.compiler.reduce_arity, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.compiler.ir.borrow, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.Meta.Tactic, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.compiler.ir.elim_dead, false, []: (trace) enable/disable tracing for the given module and submodules),
 (pp.binder_types, false, [pp]: (pretty printer) display types of lambda and Pi parameters),
 (trace.Elab.step, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.isDefEq.delta, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.compiler.input, false, []: (trace) enable/disable tracing for the given module and submodules),
 (trace.Elab.debug, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.synthInstance, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Elab.Deriving.repr, false, [trace]: enable/disable tracing for the given module and submodules),
 (trace.Meta.Match.debug, false, [trace]: enable/disable tracing for the given module and submodules),
 (interpreter.prefer_native, true, []: (interpreter) whether to use precompiled code where available),
 (trace.compiler.ll_infer_type, false, []: (trace) enable/disable tracing for the given module and submodules),
 (pp.safe_shadowing, true, [pp]: (pretty printer) allow variable shadowing if there is no collision),
 (trace.compiler.eager_lambda_lifting, false, []: (trace) enable/disable tracing for the given module and submodules),
 (genSizeOfSpec, true, []: generate `SizeOf` specificiation theorems for automatically generated instances),
 (trace.compiler.ir.push_proj, false, []: (trace) enable/disable tracing for the given module and submodules),
 (format.indent, 2, []: indentation),
 (trace.compiler.elim_dead_let, false, []: (trace) enable/disable tracing for the given module and submodules),
 (profiler, false, []: (profiler) profile tactics and vm_eval command),
 (trace.compiler.ir.boxing, false, []: (trace) enable/disable tracing for the given module and submodules)]