package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.vernac/Loadpath/index.html

Module LoadpathSource

* Load paths.

A load path is a physical path in the file system; to each load path is associated a Rocq DirPath.t (the "logical" path of the physical path).

Sourcetype t

Type of loadpath bindings.

Sourceval logical : t -> Names.DirPath.t

Get the logical path (Rocq module hierarchy) of a loadpath.

Sourceval physical : t -> CUnix.physical_path

Get the physical path of a loadpath

Sourceval pp : t -> Pp.t

Print a load path

Sourceval get_load_paths : unit -> t list

Get the current loadpath association.

Sourceval remove_load_path : CUnix.physical_path -> unit

Remove the current logical path binding associated to a given physical path, if any.

Sourceval find_load_path : CUnix.physical_path -> t

Get the binding associated with a physical path. Raises Not_found if there is none.

Sourceval find_with_logical_path : Names.DirPath.t -> t list

get the list of load paths that correspond to a given logical path

Sourceval find_extra_dep_with_logical_path : ?loc:Loc.t -> from:Names.DirPath.t -> file:string -> unit -> CUnix.physical_path

finds a file rooted in from.

  • raises UserError

    if the file is not found

Sourceval locate_file : string -> string

Locate a file among the registered paths. Do not use this function, as it does not respect the visibility of paths.

Sourcemodule Error : sig ... end
Sourceval locate_absolute_library : Names.DirPath.t -> (CUnix.physical_path, Error.t) Result.t

Locates a library by implicit name.

  • returns

    LibUnmappedDir if the library is not in the path

  • returns

    LibNotFound if there is no corresponding file in the path

Extending the Load Path
Sourcetype vo_path = {
  1. unix_path : string;
    (*

    Filesystem path containing vo/ml files

    *)
  2. coq_path : Names.DirPath.t;
    (*

    Rocq prefix for the path

    *)
  3. implicit : bool;
    (*

    implicit = true avoids having to qualify with coq_path true for -R, false for -Q in command line

    *)
  4. recursive : bool;
    (*

    recursive will determine whether we explore sub-directories

    *)
  5. installed : bool;
    (*

    installed is true for automatically added paths (eg user-contrib), which are assumed to be installed files. False is assumed to be local files (ie current development).

    *)
}

Adds a path to the Rocq and ML paths

Sourceval add_vo_path : vo_path -> unit