Debugging flags - FStarLang/FStar GitHub Wiki

See Debugging FStar for explanation.

Updated Oct 2020. See also issue #2089.

  • 1346: unification within tactics (do_unify)
  • 380: logical simplification in the normalizer
  • bind: binding of effectful computations in typechecker
  • CheckedFiles: loading and writing of .checked files; does not need a matching --debug
  • Coercions: insertion of type-directed coercions in typechecker
  • Dep: dependency analysis; does not need a matching --debug
  • ED: typechecking of effect definitions
  • Exports: something about internal letbindings?
  • Extraction: extraction pipeline, including detailed info on the translation of terms into the backend language
  • ExtractionReify: reification of effects on extraction
  • ExtractNorm: normalization of top-level letbindings before extraction
  • FastImplicits: fast implicit typechecking feature
  • Gen: generalization
  • GenUniverses: universe generalization
  • Imp: prints implicits on proofstate dumps in tactics (remove?)
  • ImplicitTrace: prints messages every time an implicit is created during typechecking or unification
  • LayeredEffects, LayeredEffectsApp, LayeredEffectsEqns, LayeredEffectsTc: layered effects
  • LogTypes: prints the types of top-levels after checking them
  • NBE, NBETop: debugging of NBE normalizer
  • Norm: normalization, prints full trace of abstract machine, very verbose! See following ones
  • NormCfg: when in addition to Norm, dumps the full machine's cfg on every step (even more verbose!)
  • NormDelayed: prints a message when the normalizer reaches a Tm_delayed node (remove? is this useful?)
  • NormRebuild: like Norm, but for the rebuild phase (join with Norm?)
  • NormTop: prints a message on the entry and exit of every normalization call, but no steps; useful to find slow norm calls
  • Normalize: affects the behaviour of --dump_module by normalizing before printing.
  • NYC: not sure
  • PartialApp: partial applications during SMT encoding
  • Patterns: typechecking of patterns
  • Positivity: positivity analysis of inductives
  • Primops: during normalization, print info about primitive operators (e.g. (+))
  • print_normalized_terms: in normalizer, print results of norm requests (Pervasives.norm, etc)
  • Range: print information, including position info, of top-level variables when they appear in a program
  • Rel, RelBench,RelCheck, RelDelta, EQ, ExplainRel: unification, see code for more details
  • ResolveImplicitsHook: triggering and handling of @@resolve_implicits
  • Return: insertion of returns in WPs
  • Simplification: simplification of guards
  • SMTEncoding: encoding pipeline, including a trace of the translation
  • SMTEncodingReify: encoding of reifiable effects
  • SMTQuery: prints obligations before encoding them, and some information on the querying process itself
  • Tac: high-level messages about tactic execution
  • TacFail: prints a message when a tactic fails internally, even if the failure is handled!
  • TacVerbose: more tactic information, and more information in proofstate dumps
  • TCDeclTime: print the time it takes to check each decl
  • Time: print how long it takes to encode queries
  • TwoPhases: info on 2-phase debugging, including what the elaborated definition looks like
  • UF: elimination (compression) of uvars after typechecking
  • Unfolding: in normalization, print when and why top-level variable names are unfolded to their definitions (or not unfolded), i.e. information about delta steps
  • UniverseOf: prints a message in a given case of the universe_of auxiliary function, likely not useful for users
  • univ_norm: normalization of universe levels
  • WPE: optimization of WPs in normalizer

PS. This can help in obtaining a list: sed -e '/Binary/d' -e 's/.*Options.Other "\(\S*\)".*/\1/' <(git grep "Options.Othe") | sort | uniq