Module system

Lambdapi has a very light module system based on file paths. It allows you to split your developments across files and folders. The main thing to know is that a file holds a single module, and accessing this module in other files requires using its full module path.

Module path

The module path that corresponds to a source file is defined using the name of the file, but also the position of the file under the library root (a folder under which all libraries are installed).

By default, the library root is /usr/local/lib/lambdapi/lib_root or $OPAM_SWITCH_PREFIX/lib/lambdapi/lib_root if OPAM_SWITCH_PREFIX is defined. An alternative library root can be specified using the environment variable LAMBDAPI_LIB_ROOT or the command line flag --lib-root.

The typical case is when we want to access a module of some installed library. In that case, the module path is built using the file path as follows: if our source file is at <LIB_ROOT>/std/bool.lp it is accessed with module path std.bool. And if there are nested folders then the module path gets more members. File <LIB_ROOT>/std/a/b/c/d.lp has module path std.a.b.c.d.

By default, all modules are looked up under the library root. However, there are cases where the files we want to work with are not yet placed under the library root. The typical case is when a library is under development. In that case, the development folder can be mapped under the library root, similarly to what would happen when mounting a volume in a file system. There are two ways of doing that, the first one is to use the --map-dir MOD:DIR command line option. However, the best way is to use a package configuration file.

Package configuration file

A package configuration file lambdapi.pkg can be placed at the root of the source tree of a library under development. It must contain the following fields (an example is given below for the syntax):

  • package_name giving a globally unique name for the package being defined. This is not used yet, but will be necessary when packages will eventually be published online so that they can be automatically downloaded when users (the idea is to come up with a system similar to Cargo in Rust).

  • root_path gives the module path under which the library is to be placed. Assuming that our configuration file is at <REPO_ROOT>/lambdapi.pkg, this means that <REPO_ROOT>/a/b/c.lp will get module path <ROOT_PATH>.a.b.c. In other words, this is equivalent to --map-dir <ROOT_PATH>:<REPO_ROOT> on the command line.

Remark: .lpo files needs to be removed and regenerated if the root_path is changed.

In the future, more useful meta data may be added to the configuration file, for example the name of the author, the version number, the dependencies, …

Example of configuration file (syntax reference):

# Lines whose first non-whitespace charater is # are comments
# The end of a non-comment line cannot be commented.
# The config file MUST be called "lambdapi.pkg".
# The syntax for entries is:
key = value
# If the key is not known then it is ignored.
# There are two used keys for now:
package_name = my_package_name
root_path    = a.b.c
# We will use more entries later (e.g., authors, version, ...)

Installation procedure for third-party packages

A package should be installed under the library directory, under the specified root path. In other words a package whose root path is x.y.z should have its files installed under the directory <LIB_ROOT>/x/y/z. Moreover the directory structure relative to the package configuration file should be preserved.

Of course, we should enforce that a root path is uniquely used by one package. This can be enforced using a central authority, but this can only be done when we actually decide to implement automatic package distribution. For now, it is assumed that every user uses reasonable root paths for their packages.

Note that if a package uses root path a.b.c then no other package should use root path a or a.b (and obviously not a.b.c either). However there is no problem in using a.d or a.b.d. The rules are as follows:

  • the root path of a package cannot be a prefix of the root path of another,

  • the root path of a package cannot extend the root path of another.

We will use the following conventions:

  • root path std is reserved for the standard library,

  • extracted libraries are installed under libraries.<NAME> (for example, we would use root path libraries.matita for matita).