package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.coqargs/Coqargs/index.html

Module CoqargsSource

Sourcetype native_compiler = Coq_config.native_compiler =
  1. | NativeOff
  2. | NativeOn of {
    1. ondemand : bool;
    }
Sourcetype top =
  1. | TopLogical of string
  2. | TopPhysical of string
Sourcetype option_command =
  1. | OptionSet of string option
  2. | OptionUnset
  3. | OptionAppend of string
Sourcetype export_flag =
  1. | Export
  2. | Import
Sourcetype require_injection = {
  1. lib : string;
  2. prefix : string option;
  3. export : export_flag option;
  4. allow_failure : bool;
}

Parameters follow Library, that is to say, lib,prefix,export means require library lib from optional prefix and import or export if export is Some Lib.Import/Some Lib.Export.

Sourcetype injection_command =
  1. | OptionInjection of string list * option_command
    (*

    Set flags or options before the initial state is ready.

    *)
  2. | RequireInjection of require_injection
    (*

    Require libraries before the initial state is ready.

    *)
  3. | WarnNoNative of string
    (*

    Used so that "-w -native-compiler-disabled -native-compiler yes" does not cause a warning. The native option must be processed before injections (because it affects require), so the instruction to emit a message is separated.

    *)
  4. | WarnNativeDeprecated
    (*

    Used so that "-w -native-compiler-deprecated-option -native-compiler FLAG" does not cause a warning, similarly to above.

    *)
Sourcetype coqargs_logic_config = {
  1. impredicative_set : bool;
  2. indices_matter : bool;
  3. type_in_type : bool;
  4. rewrite_rules : bool;
  5. toplevel_name : top;
}
Sourcetype time_config =
  1. | ToFeedback
  2. | ToFile of string
Sourcetype coqargs_config = {
  1. logic : coqargs_logic_config;
  2. rcfile : string option;
  3. coqlib : string option;
  4. enable_VM : bool;
  5. native_compiler : native_compiler;
  6. native_output_dir : CUnix.physical_path;
  7. native_include_dirs : CUnix.physical_path list;
  8. output_directory : CUnix.physical_path option;
  9. exclude_dirs : CUnix.physical_path list;
  10. beautify : bool;
  11. quiet : bool;
  12. time : time_config option;
  13. test_mode : bool;
  14. profile : string option;
  15. print_emacs : bool;
}
Sourcetype vo_path = {
  1. implicit : bool;
    (*

    true if -R, otherwise -Q

    *)
  2. unix_path : string;
  3. rocq_path : string;
}
Sourcetype coqargs_pre = {
  1. boot : bool;
  2. load_init : bool;
  3. load_rcfile : bool;
  4. ml_includes : CUnix.physical_path list;
  5. vo_includes : vo_path list;
  6. load_vernacular_list : (string * bool) list;
  7. injections : injection_command list;
}
Sourcetype coqargs_query =
  1. | PrintWhere
  2. | PrintConfig
  3. | PrintVersion
  4. | PrintMachineReadableVersion
  5. | PrintHelp
Sourcetype coqargs_main =
  1. | Queries of coqargs_query list
  2. | Run
Sourcetype coqargs_post = {
  1. memory_stat : bool;
}
Sourcetype t = {
  1. config : coqargs_config;
  2. pre : coqargs_pre;
  3. main : coqargs_main;
  4. post : coqargs_post;
}
Sourceval default : t
Sourceval parse_args : init:t -> string list -> t * string list
Sourceval injection_commands : t -> injection_command list
Sourceval get_int : opt:string -> string -> int
Sourceval get_int_opt : opt:string -> string -> int option
Sourceval get_bool : opt:string -> string -> bool
Sourceval get_float : opt:string -> string -> float
Sourceval error_missing_arg : string -> 'a
Sourceval error_wrong_arg : string -> 'a