Module `Loadpath`Source

* Load paths.

A load path is a physical path in the file system; to each load path is associated a Coq 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 (Coq 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.

Sourcetype locate_error =

| LibUnmappedDir
| LibNotFound

Locate a library in the load path

Sourcetype 'a locate_result = ('a, locate_error) result

Source

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

Locates a library by implicit name.

raises LibUnmappedDir
if the library is not in the path

raises LibNotFound
if there is no corresponding file in the path

Sourceval try_locate_absolute_library : Names.DirPath.t -> string

Extending the Load Path

Sourcetype vo_path = {

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

}

Adds a path to the Coq and ML paths

Sourceval add_vo_path : vo_path -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.vernac/Loadpath/index.html

Module `Loadpath`Source

Extending the Load Path

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.vernac/Loadpath/index.html

Module LoadpathSource

Extending the Load Path

Module `Loadpath`Source