Command line interface

The main Lambdapi executable is called lambdapi, and it can be invoked using lambdapi COMMAND .... To see the list of the supported commands, simply run lambdapi help or lambdapi --help. To get the documentation of a specific command run lambdapi COMMAND --help. It will contain the list of options that are supported by the command.

The available commands are:

check: check the correctness of input files.
decision-tree: output the decision tree of a symbol as a Dot graph (see Decision trees)
export: translate the input file to other formats.
help: display the main help message.
index: create an index of symbols and rules of input files.
init: create a new Lambdapi package (see Getting started).
install: install the specified files according to package configuration.
lsp: run the Lambdapi LSP server.
parse: parse the input files.
search: runs a search query against the index.
uninstall: uninstalls the specified package.
version: give the current version of Lambdapi.
websearch: starts a webserver to search the library.

The commands parse, export and index can trigger the compilation of dependencies if the required object files (.lpo extension) are not present.

Input files:

The commands check, parse, export and index expect input files with either the .lp extension or the .dk extension. The appropriate parser is selected automatically. The export command accept only one file as argument.

If a command takes several files as argument, the files are handled independently in the order they are given. The program immediately stops on the first failure, without going to the next file (if any).

Remark on index:

The index command generates the file ~/.LPSearch.db if $HOME is defined, and .LPSearch.db otherwise. This file contains an indexation of all the symbols and rules occurring in the dk/lp files given in argument. By default, the db file is erased first. To append new symbols and rules, use the option --add. It is also possible to normalize terms wrt some rules before indexation by using --rules options.

Remark on search:

The command search takes as argument a query and runs it against the index file ~/.LPSearch.db. It is also possible to normalize terms in the query wrt some rules by using --rules options. It is advised to use the same set of rules previously used during indexing. It is also possible to pass via --require a file to be required and opened before performing the query, e.g. to specify implicit arguments for symbols. See Query Language for the specification of the query language.

Common flags:

The commands check, decision-tree, export, parse, lsp all support the following command line arguments and flags.

--debug=<FLAGS> enables the debugging modes specified by every character of FLAGS. Details on available character flags are obtained using --help.
--lib-root=<DIR> sets the library root, that is, the folder corresponding to the entry point of the Lambdapi package system. This is the folder under which every package is installed, and a default value is only known if the program has been installed. In development mode, --lib-root lib must be given (assuming Lambdapi is run at the root of the repository).
--map-dir=<MOD>:<DIR> maps an arbitrary directory DIR under a module path MOD (relative to the root directory). This option is mainly useful during the development of a package (before it has been installed). However it can also be accessed using a package configuration file (lambdapi.pkg) at the root of the library’s source tree. More information on that is given in the section about the module system.
--no-sr-check disables subject reduction checking.
--timeout=<NUM> gives up type-checking after the given number of seconds. Note that the timeout is reset between each file, and that the parameter of the command is expected to be a natural number.
-v <NUM>, --verbose=<NUM> sets the verbosity level to the given natural number (the default value is 1). A value of 0 should not print anything, and the higher values print more and more information.

check

-c, --gen-obj instructs Lambdapi to generate object files for every checked module (including dependencies). Object files have the extension .lpo and they are automatically read back when necessary if they exist and are up to date (they are regenerated otherwise).
--too-long=<FLOAT> gives a warning for each interpreted source file command taking more than the given number of seconds to be checked. The parameter FLOAT is expected to be a floating point number.

confluence

--confluence=<CMD> checks the confluence of the rewriting system by calling an external prover with the command CMD. The given command receives HRS formatted text on its standard input, and is expected to output on the first line of its standard output either YES, NO or MAYBE. As an example, echo MAYBE is the simplest possible (valid) confluence checker that can be used.

For now, only the CSI^ho confluence checker has been tested with Lambdapi. It can be called using the flag --confluence "path/to/csiho.sh --ext trs --stdin".

To inspect the .trs file generated by Lambdapi, one may use the following dummy command: --confluence "cat > output.trs; echo MAYBE".

decision-tree

--ghost print the decision tree of a ghost symbol. Ghost symbols are symbols used internally that cannot be used in the concrete syntax.

export

-o <FMT>, --output=<FMT> instructs Lambdapi to translate the files given in argument according to <FMT>:
- lp: Lambdapi format
- dk: Dedukti format
- raw_dk: Dedukti format
- hrs: HRS format of the confluence competition
- xtc: XTC format of the termination competition
- raw_coq: Coq format
- stt_coq: Coq format assuming that the input file is in an encoding of simple type theory

WARNING: With the formats raw_coq, stt_coq and raw_dk, the translation is done just after parsing, thus before scoping and elaboration. So Lambdapi cannot translate any input file, and the output may be incomplete or fail to type-check.

The format raw_dk does not accept the commands notation and inductive, and proofs and tactics, which require elaboration.

The formats raw_coq and stt_coq only accept the commands require, open, symbol and rule, but rules are simply ignored. The encoding of simple type theory can however be defined in Coq using STTfa.v.

For the format stt_coq, several other options are available:

--encoding <LP_FILE> (mandatory option) where <LP_FILE> contains the following sequence of builtin declarations:

builtin "Set" ≔ ...; // : TYPE
builtin "prop" ≔ ...; // : Set
builtin "arr" ≔ ...; // : Set → Set → Set
builtin "El" ≔ ...; // : Set → TYPE
builtin "Prf" ≔ ...; // : El prop → TYPE
builtin "eq" ≔ ...; // : Π [a : Set], El a → El a → El prop
builtin "not" ≔ ...; // : El prop → El prop
builtin "imp" ≔ ...; // : El prop → El prop → El prop
builtin "and" ≔ ...; // : El prop → El prop → El prop
builtin "or" ≔ ...; // : El prop → El prop → El prop
builtin "all" ≔ ...; // : Π [a : Set], (El a → El prop) → El prop
builtin "ex" ≔ ...; // : Π [a : Set], (El a → El prop) → El prop

It tells Lambdapi which symbols of the input files are used for the encoding. Example: encoding.lp. The first argument a of the symbols corresponding to the builtins "eq", "all" and "ex" need not be declared as implicit.

In symbol declarations or definitions, parameters with no type are assumed to be of type the term associated with the builtin "Set".

--no-implicits instructs Lambdapi that the symbols of the encoding have no implicit arguments.
--renaming <LP_FILE> where <LP_FILE> contains a sequence of builtin declarations of the form

builtin "coq_expr" ≔ lp_id;

It instructs Lambdapi to replace any occurrence of the unqualified identifier lp_id by coq_expr, which can be any Coq expression. Example: renaming.lp.

--requiring <MODNAME> to add Require Import <MODNAME> at the beginning of the output. <MODNAME>.v usually needs to contain at least the following definitions:

Definition arr (A:Type) (B:Type) := A -> B.
Definition imp (P Q: Prop) := P -> Q.
Definition all (A:Type) (P:A->Prop) := forall x:A, P x.

if the symbols corresponding to the builtins "arr", "imp" and "all" occurs partially applied in the input file. Example: coq.v.

--mapping <LP_FILE> where <LP_FILE> contains a sequence of builtin declarations like for the option --renaming except that, this time, lp_id can be a qualified identifier. It has the same effect as the option --renaming plus it removes any declaration of the renamed symbols. coq_expr therefore needs to be defined in Coq standard library or in the Coq file specified with the option --requiring. It is not necessary to have entries for the symbols corresponding to the builtins "El" and "Prf" declared with the option --encoding since they are erased automatically. Example: mapping.lp.
--use-notations instructs Lambdapi to use the usual Coq notations for the symbols corresponding to the builtins "eq", "not", "and" and "or".

Examples of libraries exported to Coq:

In the Lambdapi sources, see how to export the Holide Dedukti library obtained from OpenTheory in README.md.
See in hol2dk how to export the Lambdapi library obtained from HOL-Light.

index

--add tells lambdapi to not erase the index before adding new symbols and rules.
--rules <LPSearch.lp> tells lambdapi to normalize terms using the rules given in the file <LPSearch.lp> before indexing. Several files can be specified by using several --rules options. In these files, symbols must be fully qualified but no require command is needed. Moreover, the rules do not need to preserve typing. On the other hand, right hand-side of rules must contain implicit arguments.

For instance, to index the Matita library, you can use the following rules:

rule cic.Term _ $x ↪ $x;
rule cic.lift _ _ $x ↪ $x;

--db <FILE.db> tells lambdapi to index symbols and rules in <FILE.db> instead of ~/.LPSearch.db.

install/uninstall

--dry-run prints the system commands that should be called instead of running them.

lsp

--standard-lsp restricts to standard LSP protocol (no extension).
--log-file=<FILE> sets the log file for the LSP server. If not given, the file /tmp/lambdapi_lsp_log.txt is used.

search

--rules <LPSearch.lp> tells lambdapi to normalize terms in the query using the rules given in the file <LPSearch.lp>. Several files can be specified by using several --rules options. In these files, symbols must be fully qualified but no require command is needed. Moreover, the rules do not need to preserve typing. On the other hand, right hand-side of rules must contain implicit arguments. It is advised to use the same set of rules previously used during indexing.
--require <FILE.lp> requires and open <FILE.lp> when starting the search engine. The file can be used for example to specify implicit arguments for symbols used in the queries.
--db <FILE.db> tells lambdapi to search in <FILE.db> instead of ~/.LPSearch.db.

termination

--termination=<CMD> checks the termination of the rewriting system by calling an external prover with the command CMD. The given command receives XTC formatted text on its standard input, and is expected to output on the first line of its standard output either YES, NO or MAYBE. echo MAYBE is the simplest (valid) command for checking termination.

To the best of our knowledge, the only termination checker that is compatible with all the features of Lambdapi is SizeChangeTool. It can be called using the flag --termination "path/to/sct.native --no-color --stdin=xml"

If no type-level rewriting is used Wanda can also be used. However, it does not directly accept input on its standard input, so it is tricky to have Lambdapi call it directly. Alternatively, one can first generate a .xml file as described below.

To inspect the .xml file generated by Lambdapi, one may use the following dummy command:--termination "cat > output.xml; echo MAYBE".

websearch

--port=<N> specifies the port number to use (default is 8080).
--rules <LPSearch.lp> tells lambdapi to normalize terms in the queries using the rules given in the file <LPSearch.lp>. Several files can be specified by using several --rules options. In these files, symbols must be fully qualified but no require command is needed. Moreover, the rules do not need to preserve typing. On the other hand, right hand-side of rules must contain implicit arguments. It is advised to use the same set of rules previously used during indexing.
--require <FILE.lp> requires and open the file <FILE.lp> when starting the search engine. The file can be used for example to specify implicit arguments for symbols used in the queries.
--db <FILE.db> tells the server to use <FILE.db> instead of ~/.LPSearch.db.
--header <FILE.html> uses <FILE.html> as header of the search engine web page.
--url <STRING> tells the server to only accept requests on URLs which path is <STRING>. By default, the server only accepts requests on URLs which path is empty. Use ** to accept requests with any path. It is possible to express more complex constraints using the Dream framework.