package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

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

Maintainers

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

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

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

Module SystemSource

Coqtop specific system utilities
Directories
Sourcetype unix_path = string
Sourcetype file_kind =
  1. | FileDir of unix_path * string
  2. | FileRegular of string
Sourceval (//) : unix_path -> string -> unix_path
Sourceval exists_dir : unix_path -> bool

mkdir path ensures that path exists as a directory, creating the missing suffix if necessary (like Unix' mkdirhier)

Sourceval mkdir : unix_path -> unit

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
Sourceval warn_cannot_open_dir : ?loc:Loc.t -> string -> unit

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
Sourceval where_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string

get_output_path fname relativizes fname with respect to the default output directory if fname is not absolute

Sourceval 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

Sourceval 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

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 speeds 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 = {
  1. filename : string;
  2. actual : int32;
  3. expected : int32;
}
Sourceexception Bad_magic_number of magic_number_error
Sourceexception Bad_version_number of magic_number_error
Sourceval with_magic_number_check : ?loc:Loc.t -> ('a -> 'b) -> 'a -> 'b

big-endian encoding and decoding of int32 (4 btyes) and int64 (8 bytes)

Sourceval input_int32 : in_channel -> int32
Sourceval input_int64 : in_channel -> int64
Sourceval output_int32 : out_channel -> int32 -> unit
Sourceval output_int64 : out_channel -> int64 -> unit

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
Sourcetype duration
Sourceval empty_duration : duration
Sourceval get_time : unit -> time
Sourceval time_difference : time -> time -> float

in seconds

Sourceval duration_between : start:time -> stop:time -> duration
Sourceval duration_add : duration -> duration -> duration
Sourceval duration_real : duration -> float
Sourceval fmt_time_difference : time -> time -> Pp.t
Sourceval fmt_duration : duration -> Pp.t
Sourcetype 'a transaction_result = ('a * duration, Exninfo.iexn * duration) Result.t
Sourceval measure_duration : ('a -> 'b) -> 'a -> 'b transaction_result
Sourceval fmt_transaction_result : 'a transaction_result -> Pp.t
Instruction count.
Sourcetype instruction_count = (Int64.t, string) Result.t
Sourceval instructions_between : c_start:instruction_count -> c_end:instruction_count -> instruction_count
Sourcetype 'a instructions_result = ('a * instruction_count, Exninfo.iexn * instruction_count) Result.t
Sourceval count_instructions : ('a -> 'b) -> 'a -> 'b instructions_result
Sourceval fmt_instructions_result : 'a instructions_result -> Pp.t
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.