package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

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

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.0.tar.gz

md5=66e57ea55275903bef74d5bf36fbe0f1

sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b

doc/coq-core.clib/CUnix/index.html

Module `CUnix`Source

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.

Source

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

On This Page

System utilities
Executing commands