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#L749)

• Typechecking: admit_smt_queries, cardinality, eager_inference, initial_fuel, initial_ifuel, max_fuel, max_ifuel, min_fuel, inline_arith, lax, reuse_hint_for, split_cases, __temp_no_proj, unthrottle_inductives, use_eq_at_higher_order, use_tactics, 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. It also restarts the SMT solver process.

Although currently, #reset-options restarts the Z3 SMT solver process as a side effect, the plan is to decouple this behaviour in a separate pragma (e.g. #reset-solver).

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 #set-options to temporarily increase the Z3 resource limits and fuel to typecheck f and then #reset-options to restore the original settings:

val f: ...

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

let f x y = ...

#reset-options

---

#set-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 set --lax at the beginning of the file to skip type checking a large chunk known to verify and then use #reset-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.