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.clib/CUnix/index.html

Module CUnixSource

System utilities
Sourcetype physical_path = string
Sourcetype load_path = physical_path list
Sourceval physical_path_of_string : string -> physical_path
Sourceval string_of_physical_path : physical_path -> string
Sourceval escaped_string_of_physical_path : physical_path -> string

Escape what has to be escaped (e.g. surround with quotes if with spaces)

Sourceval canonical_path_name : string -> string
Sourceval remove_path_dot : string -> string

Remove all initial "./" in a path

Sourceval strip_path : string -> string

If a path p starts with the current directory $PWD then strip_path p returns the sub-path relative to $PWD. Any leading "./" are also removed from the result.

Sourceval correct_path : string -> string -> string

correct_path f dir = dir/f if f is relative

Sourceval path_to_list : string -> string list
Sourceval make_suffix : string -> string -> string

make_suffix file suf catenate file with suf when file does not already end with suf.

Sourceval file_readable_p : string -> bool
Executing commands

run_command com launches command com, and returns the contents of stdout and stderr. If given, ~hook is called on each elements read on stdout or stderr.

Sourceval run_command : ?hook:(bytes -> unit) -> string -> Unix.process_status * string

sys_command launches program prog with arguments args. It behaves like Sys.command, except that we rely on Unix.create_process, it's hardly more complex and avoids dealing with shells. In particular, no need to quote arguments (against whitespace or other funny chars in paths), hence no need to care about the different quoting conventions of /bin/sh and cmd.exe.

Sourceval sys_command : string -> string list -> Unix.process_status

A version of Unix.waitpid immune to EINTR exceptions

Sourceval waitpid_non_intr : int -> Unix.process_status
Sourceval same_file : string -> string -> bool

Check if two file names refer to the same (existing) file

Sourceval mktemp_dir : ?temp_dir:string -> string -> string -> string

Like Stdlib.Filename.temp_file but producing a directory.