Module `Loadpath`Source

* 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

Source

val 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

Source

val locate_qualified_library : 
  ?root:Names.DirPath.t ->
  Libnames.qualid ->
  (Names.DirPath.t * CUnix.physical_path, Error.t) Result.t

Source

val 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 = {

unix_path : string;
(*
Filesystem path containing vo/ml files
*)
coq_path : Names.DirPath.t;
(*
Rocq prefix for the path
*)
implicit : bool;
(*
implicit = true avoids having to qualify with coq_path true for -R, false for -Q in command line
*)
recursive : bool;
(*
recursive will determine whether we explore sub-directories
*)

}

Adds a path to the Rocq and ML paths

Sourceval add_vo_path : vo_path -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Loadpath`Source

Extending the Load Path

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module LoadpathSource

Extending the Load Path

Module `Loadpath`Source