Debugging flags

See also: Debugging FStar

Debugging in F* works by selecting 1) a set of modules to debug and 2) a set of debug levels that we are interested in. Debug messages will be printed only for the enabled modules and only when they are relevant to the level, so both usually need to be provided. Note that levels are case-sensitive (but module names are not).

As an exception to the rule above, simply providing --debug X without any level does have a small effect, it prints some top-level messages (e.g. loading of plugins and opening of files). In fact, X can be anything to enable these messages, so --debug y is a common way to do so. Also, there are (currently) two levels which are module independent: CheckedFiles and Dep; simply providing --debug_level Dep will print information on the dependency analysis without needing any --debug.

There are Low, Medium, High and Extreme levels, each of which is contained in the next one, but different levels are usually completely independent. These print increasingly detailed information on the typechecking process. If you're trying to figure out when a crash or infinite loop happens, starting from --debug_level Low and moving upwards is a good idea.

A full list of levels (as of Oct 11 2020) is given below (omitting Low-Extreme), with a very short sentence describing what they are related to. Some of these are quite obscure, improving these flags is future work (#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