Module System

Coqtop specific system utilities
Directories
type unix_path = string
type file_kind =
| FileDir of unix_path * string
| FileRegular of string
val (//) : unix_path -> string -> unix_path
val exists_dir : unix_path -> bool
val mkdir : unix_path -> unit
val exclude_directory : unix_path -> unit
val process_directory : (file_kind -> unit) -> unix_path -> unit
val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit
Files and load paths
val warn_cannot_open_dir : ?⁠loc:Loc.t -> string -> unit
val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list
val is_in_path : CUnix.load_path -> string -> bool
val is_in_system_path : string -> bool
val where_in_path : ?⁠warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
val find_file_in_path : ?⁠warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string

find_file_in_path ?warn loadpath filename returns the directory name and long name of the first physical occurrence filename in one of the directory of the loadpath; fails with a user error if no such file exists; warn if two or more files exist in the loadpath; returns instead the directory name of filename is filename is an absolute path

val all_in_path : (CUnix.physical_path * 'a) list -> string -> ('a * string) list

all_in_path loadpath filename returns the list of the directory name and full name of all physical occurrences of filename in a loadpath binding physical paths to some arbitrary key

val trust_file_cache : bool Stdlib.ref

trust_file_cache indicates whether we trust the underlying mapped file-system not to change along the execution of Coq. This assumption greatly speds up file search, but it is often inconvenient in interactive mode

val file_exists_respecting_case : string -> string -> bool
I/O functions
type magic_number_error = {
filename : string;
actual : int32;
expected : int32;
}
exception Bad_magic_number of magic_number_error
exception Bad_version_number of magic_number_error
val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
val input_int32 : Stdlib.in_channel -> int32
val input_int64 : Stdlib.in_channel -> int64
val output_int32 : Stdlib.out_channel -> int32 -> unit
val output_int64 : Stdlib.out_channel -> int64 -> unit
val marshal_out : Stdlib.out_channel -> 'a -> unit
val marshal_in : string -> Stdlib.in_channel -> 'a
val check_caml_version : caml:string -> file:string -> unit
Time stamps.
type time
type duration
val get_time : unit -> time
val time_difference : time -> time -> float

in seconds

val duration_between : start:time -> stop:time -> duration
val duration_add : duration -> duration -> duration
val duration_real : duration -> float
val fmt_time_difference : time -> time -> Pp.t
val fmt_duration : duration -> Pp.t
type 'a transaction_result = ('a * duration, Exninfo.iexn * duration) Stdlib.Result.t
val measure_duration : ('a -> 'b) -> 'a -> 'b transaction_result
val fmt_transaction_result : 'a transaction_result -> Pp.t
Instruction count.
type instruction_count = (Stdlib.Int64.t, string) Stdlib.Result.t
val instructions_between : c_start:instruction_count -> c_end:instruction_count -> instruction_count
val instruction_count_add : instruction_count -> instruction_count -> instruction_count
type 'a instructions_result = ('a * instruction_count, Exninfo.iexn * instruction_count) Stdlib.Result.t
val count_instructions : ('a -> 'b) -> 'a -> 'b instructions_result
val fmt_instructions_result : 'a instructions_result -> Pp.t
val get_toplevel_path : ?⁠byte:bool -> string -> string

get_toplevel_path program builds a complete path to the executable denoted by program. This involves:

  • locating the directory: we don't rely on PATH as to make calls to /foo/bin/coqtop chose the right /foo/bin/coqproofworker
  • adding the proper suffixes: .opt/.byte depending on the current mode, + .exe if in windows.

Note that this function doesn't check that the executable actually exists. This is left back to caller, as well as the choice of fallback strategy. We could add a fallback strategy here but it is better not to as in most cases if this function fails to construct the right name you want you execution to fail rather than fall into choosing some random binary from the system-wide installation of Coq.