Skip to content

Instantly share code, notes, and snippets.

@bryangingechen

bryangingechen/lean4_options Secret

Created Mar 21, 2021
Embed
What would you like to do?
version: nightly-2021-03-21
#[(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)]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment