Module `System`Source

Coqtop specific system utilities

Directories

Sourcetype unix_path = string

Sourcetype file_kind =

| FileDir of unix_path * string
| FileRegular of string

Sourceval (//) : unix_path -> string -> unix_path

Sourceval exists_dir : unix_path -> bool

exclude_search_in_dirname path excludes path when processing directories

Sourceval exclude_directory : unix_path -> unit

process_directory f path applies f on contents of directory path; fails with Unix_error if the latter does not exists; skips all files or dirs starting with "."

Sourceval process_directory : (file_kind -> unit) -> unix_path -> unit

process_subdirectories f path applies f path/file file on each file of the directory path; fails with Unix_error if the latter does not exists; kips all files or dirs starting with "."

Sourceval process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit

Files and load paths

Load path entries remember the original root given by the user. For efficiency, we keep the full path (field directory), the root path and the path relative to the root.

Sourceval all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list

Sourceval is_in_path : CUnix.load_path -> string -> bool

Sourceval is_in_system_path : string -> bool

Source

val where_in_path : 
  ?warn:bool ->
  CUnix.load_path ->
  string ->
  CUnix.physical_path * string

Source

val find_file_in_path : 
  ?warn:bool ->
  CUnix.load_path ->
  string ->
  CUnix.physical_path * string

Sourceval trust_file_cache : bool 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

Sourceval file_exists_respecting_case : string -> string -> bool

I/O functions

Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception Bad_magic_number when the check fails, with the full file name and expected/observed magic numbers.

Sourcetype magic_number_error = {

filename : string;
actual : int32;
expected : int32;

}

Sourceexception Bad_magic_number of magic_number_error

Sourceexception Bad_version_number of magic_number_error

Sourceval raw_extern_state : int -> string -> out_channel

Sourceval raw_intern_state : int -> string -> in_channel

Sourceval extern_state : int -> string -> 'a -> unit

Sourceval intern_state : int -> string -> 'a

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

Clones of Marshal.to_channel (with flush) and Marshal.from_channel (with nice error message)

Sourceval marshal_out : out_channel -> 'a -> unit

Sourceval marshal_in : string -> in_channel -> 'a

Sourceval check_caml_version : caml:string -> file:string -> unit

Time stamps.

Sourcetype time

Sourceval get_time : unit -> time

Sourceval time_difference : time -> time -> float

in seconds

Sourceval fmt_time_difference : time -> time -> Pp.t

Sourceval with_time : batch:bool -> header:Pp.t -> ('a -> 'b) -> 'a -> 'b

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

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `System`Source

Coqtop specific system utilities

Directories

Files and load paths

I/O functions

Time stamps.

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module SystemSource

Coqtop specific system utilities

Directories

Files and load paths

I/O functions

Time stamps.

Module `System`Source