options.md

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 flags that are supported for the command.

The available commands are:

• help: display the main help message.
• version: give the current version of Lambdapi.
• check: runs the main type-checking mode on input source files.
• init: creates a new Lambdapi package. For more information have a look at the getting started section.
• install: installs the specified files according to package configuration.
• uninstall: uninstalls the specified package.
• parse: runs the parsing-only mode on input source files.
• beautify: runs the parser and pretty-printer on input source files.
• lsp: runs the Lambdapi LSP server.
• decision-tree: prints the decision tree for rule filtering of a symbol in the Dot language on standard output. For more information on the graph and how to read them, see src/core/tree_graphviz.ml.

Note: the parse and beautify commands can trigger the compilation of dependencies if the required object files (.lpo extension) are not present.

Note the commands that expect files are not limited to a single one. The given files are all handled independently (in the order they are given). The program immediately stops on the first failure, without going to the next file (if any).

Input files

The commands check, parse and beautify expect input files with either the standard .lp extension, or the legacy (Dedukti) .dk extension. The appropriate parser is selected automatically.

Note: the beautify command outputs only standard syntax, and hence it can be used to convert legacy syntax files (with the .dk extension) into the Lambdapi syntax.

Common flags

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

Configuration flags

• --gen-obj or -c 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).

• --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 (up to 3) print more and more information.

• --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.

• --keep-rule-order forces the rewriting engine to try and apply the rules in the order of their declaration.

Debugging flags

• --debug FLAGS enables the debugging modes specified by every character of FLAGS. Details on available character flags are obtained using --help.

• --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.

Confluence checking

Lambdapi provides an option --confluence CMD to check 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 it 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-check that one may use.

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".

Termination checking

Lambdapi provides an option --termination CMD to check 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 it is expected to output on the first line of its standard output either YES, NO or MAYBE.

As for confluence, echo MAYBE is the simplest possible (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.trs; echo MAYBE".

Specific flags for the "check" command

• --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.

• --recompile forces the compilation of the files given on the command line even if they have an up-to-date object file.

Specific flags for the "lsp" command

• --standard-lsp restricts to standard LSP protocol (no extension).

• --lsp-log-file FILE sets the log file for the LSP server. If not given, the file /tmp/lambdapi_lsp_log.txt is used.

Specific flags for the "install" and "uninstall" commands

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