package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

rocq-prover.org Readme Edit opam file Versions (1)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.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