Debugging flags

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