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.

#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.

#set-options "{option list}"

Provides a way of overriding options given in the command-line. This is most often used to modify the Z3 timeout setting 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:

• Typechecking: --z3timeout, --initial_fuel, --min_fuel, --max_fuel, --initial_ifuel, --max_ifuel, --lax, --eager_inference, --unthrottle_inductives, use_eq_at_higher_order, --split_cases, admit_smt_queries, --cardinality, --inline_arith, --reuse_hint_for

• 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_implicits, --print_universes, --prn, --show_signatures, --silent, --timing, --trace_error, --warn_top_level_effects

• Extraction: --__temp_no_proj

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

Note: When working in the soon-to-be-deprecated --stratified mode, --z3timeout can be only set through #reset-options below (restarting the SMT solver).

#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 behavior in a separate pragma (e.g. #reset-solver).

Usage examples

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

val f: ...

#set-options "--z3timeout 100 --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.