Pragmas (#set options, #reset options)

Pragmas

Pragmas are directives that are not part of the F★ language proper. They can be used to modify the way the parser and the type checker process the rest of a file.

#set-options "{option list}"

Provides a way of overriding options given in the command-line. This is most often used to modify the Z3 resource limits or the amount of fuel and inversion fuel used to typecheck part of a file.

Many options can only be set at the command-line and cannot be controlled using pragmas.

The following options can be set through pragmas (https://github.com/FStarLang/FStar/blob/master/src/basic/FStar.Options.fs#L1170, let settable = ...)

• Typechecking: admit_smt_queries, initial_fuel, initial_ifuel, max_fuel, max_ifuel, min_fuel, lax, reuse_hint_for, split_cases, __temp_no_proj, unthrottle_inductives, use_eq_at_higher_order, z3rlimit_factor, z3rlimit, z3refresh

• Debugging: debug, debug_level, detail_errors, hide_genident_nums, hide_uvar_nums, hint_info, log_types, log_queries, print_before_norm, print_bound_var_types, print_effect_args, print_fuels, print_full_names, print_implicits, print_universes, print_z3_statistics, prn, show_signatures, silent, timing, trace_error

Use fstar.exe --help to get a brief description of the behaviour of each option

#reset-options ["{option list}"]

Restores the options given originally in the command-line; then adds the options given.

Note: this pragma does not (since commit 2d524c0863bbdc4dc45b3b8a81d58290258af275, merged to master on June 24, 2019) necessarily restart the SMT solver. The SMT solver is automatically restarted by F* when options that affect the encoding are changed, and only at the time of a query, not of a pragma. Currently, the options that trigger a solver restart when changed are --z3seed, --z3cliopt, --using_facts_from, --smtencoding.valid_intro and --smtencoding.valid_elim.

#push-options "{option list}" and #pop-options

The #push-options <opts> pragma will push a new option state in the stack, copied from the current one and modified by setting the options given as if by a #set-options <opts>. The previous state can be restored by doing #pop-options. The stack can grow to any depth.

Doing #reset-options will not pop the stack, and only affect the current option state.

#restart-solver

Force a restart of the SMT solver. In normal usage, you should not need to do this, but it can be helpful in debugging flaky proofs.

Usage examples

If checking the definition of function f in a file requires higher resources and more fuel than verifying other parts of the file, one could use first #push-options to temporarily increase the Z3 resource limits and fuel to typecheck f and then #pop-options to restore the original settings:

val f: ...

#push-options "--z3rlimit 50 --initial_fuel 5 --max_fuel 5 --initial_ifuel 2 --max_ifuel 2"

let f x y = ...

#pop-options

---

#push-options "--lax" is useful to focus on parts of a file at a time, and to mark progress when working on restoring full type checking of a file following changes in other modules. For example, when working towards the end of a large file, one may want to push --lax at the beginning of the file to skip type checking a large chunk known to verify and then use #pop-options to switch back to full type checking at the point one is working on.

See Working with files with huge verification times for an example of this usage pattern. As an alternative, you should consider using hints to speed up replaying proofs. The Emacs interactive mode also provides an easier way of lax-typechecking parts of files using the fstar-subp-advance-or-retract-to-point-lax command (C-c C-l).

#light ["on" | "off"]

Switches between verbose and lightweight F# syntax; #light by itself is equivalent to #light "on". Used for source compatibility with F#. See F# Verbose Syntax.

No real reason why a user would want to use this in an F★ file.