module.md

Module system

Lambdapi has a (very) light module system based on file paths. It allows us to split our developments into several files, and even several 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 the standard library and all packages are installed).

The typical case is when we want to access a module of some installed library, for example the standard 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, every 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 (or package) is still under development. In that case, what we can do is map the development folder under the library root, similarly to what would happen when mounting a volume in our file system. There are two ways of doing that, the first one being 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 can be placed at the root of the source tree of a library (or package) under development. It should be named lambdapi.pkg, and 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 yet used, but will be necessary when we eventually publish our packages online so that they can be automatically downloaded when our users need them. (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.

In the future, more useful meta data will be added to the configuration file, for example the name of the author, version number, 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).