Module `Flags`Source

Global options of the system.

WARNING: don't add new entries to this file!

This file is own its way to deprecation in favor of a purely functional state, but meanwhile it will contain options that are truly global to the system such as debug

If you are thinking about adding a global flag, well, just don't. First of all, options make testins exponentially more expensive, due to the growth of flag combinations. So please make some effort in order for your idea to work in a configuration-free manner.

If you absolutely must pass an option to your new system, then do so as a functional argument so flags are exposed to unit testing. Then, register such parameters with the proper state-handling mechanism of the top-level subsystem of Coq.

Command-line flags

Sourceval async_proofs_worker_id : string ref

Async-related flags

Sourceval async_proofs_is_worker : unit -> bool

Sourceval load_vos_libraries : bool ref

Flag to indicate that .vos files should be loaded for dependencies instead of .vo files. Used by -vos and -vok options.

Sourceval xml_debug : bool ref

Debug flags

Sourceval in_debugger : bool ref

Sourceval in_toplevel : bool ref

Sourceval we_are_parsing : bool ref

Sourceval raw_print : bool ref

Sourceval beautify : bool ref

Sourceval beautify_file : bool ref

Sourceval quiet : bool ref

Sourceval silently : ('a -> 'b) -> 'a -> 'b

Sourceval verbosely : ('a -> 'b) -> 'a -> 'b

Sourceval if_silent : ('a -> unit) -> 'a -> unit

Sourceval if_verbose : ('a -> unit) -> 'a -> unit

Sourceval warn : bool ref

Sourceval make_warn : bool -> unit

Sourceval if_warn : ('a -> unit) -> 'a -> unit

Sourceval with_modified_ref : 'c ref -> ('c -> 'c) -> ('a -> 'b) -> 'a -> 'b

with_modified_ref r nf f x Temporarily modify a reference in the call to f x . Be very careful with these functions, it is very easy to fall in the typical problem with effects:

with_modified_ref r nf f x y != with_modified_ref r nf (f x) y

Sourceval with_option : bool ref -> ('a -> 'b) -> 'a -> 'b

Temporarily activate an option (to activate option o on f x y z, use with_option o (f x y) z)

Sourceval with_options : bool ref list -> ('a -> 'b) -> 'a -> 'b

As with_option, but on several flags.

Sourceval without_option : bool ref -> ('a -> 'b) -> 'a -> 'b

Temporarily deactivate an option

Sourceval with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b

Temporarily extends the reference to a list

Sourceval get_native_compiler : unit -> bool

Native compilation flag

Sourceval set_native_compiler : bool -> unit

Must be set exactly once at initialization time.

Sourceval set_inline_level : int -> unit

Level of inlining during a functor application

Sourceval get_inline_level : unit -> int

Sourceval default_inline_level : int

Sourceval profile_ltac : bool ref

Global profile_ltac flag

Sourceval profile_ltac_cutoff : float ref

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.lib/Flags/index.html

Module `Flags`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.lib/Flags/index.html

Module FlagsSource

Module `Flags`Source