Skip to content

Latest commit

 

History

History
112 lines (95 loc) · 3.81 KB

devel.md

File metadata and controls

112 lines (95 loc) · 3.81 KB

Dependencies and compilation

Lambdapi requires a Unix-like system. It should work on Linux as well as on MacOS. It might also be possible to make it work on Windows with Cygwyn or with "bash on Windows".

List of dependencies:

Using Opam, a suitable OCaml environment can be setup as follows.

opam switch 4.05.0
eval `opam config env`
opam install dune odoc menhir yojson cmdliner bindlib.5.0.0 timed.1.0 earley.2.0.0 ppx_inline_test

To compile Lambdapi, just run the command make in the source directory. This produces the _build/install/default/bin/lambdapi binary, which can be run on files with the .dk or .lp extension (use the --help option for more information).

make               # Build lambdapi.
make doc           # Build the documentation.
make install       # Install the program.
make install_vim   # Install vim support.
make install_emacs # Install emacs (>= 26.1) support (needs the eglot package)

Note: you can run lambdapi with dune exec lambdapi. The -- dune flag is necessary when calling lambapi with flags. If it is not given, flags are fed to the dune command instead.

The following commands can be used for cleaning up the repository:

make clean     # Removes files generated by OCaml.
make distclean # Same as clean, but also removes library checking files.
make fullclean # Same as distclean, but also removes downloaded libraries.

Tests and supported libraries

You can run tests using the following commands.

make tests        # Unit tests (not stopping on failure).
make real_tests   # Unit tests (stopping on first failure).

make dklib        # Checks files at https://github.com/rafoo/dklib/
make focalide     # Checks files generated from the Focalize library
make holide       # Checks files generated from the OpenTheory library
make matita       # Checks the traduction of Matita's arithmetic library.
make verine       # Checks files generated by the VeriT prover.
make iprover      # Checks files generated by iProverModulo.
make zenon_modulo # Checks files generated by ZenonModulo.

Profiling tools

This document explains the use of standard profiling tools for the development of lambdapi.

Using Linux perf

The quickest way to obtain a per-symbol execution time is perf. It is simple to use, provided that you have the right privileges on your machine. No change is required in the build procedure, but lambdapi must be invoked as follows.

dune exec -- perf record lambdapi [LAMBDAPI_OPTIONS]

The program behaves as usual, but a trace is recorded in file perf.data. The data can then be displayed with the following command.

perf report

Profiling using Gprof

The gprof tool can be used to obtain a more precise (and thorough) execution trace. However, it requires modifying the src/dune file by replacing

(executable
 (name lambdapi)

with the following.

(executable
 (name lambdapi)
 (ocamlopt_flags (:standard -p))

This effectively adds the -p flag to every invocation of ocamlopt.

After doing that, lambdapi can be launched on the desired example, to record an execution trace. This has the (side-)effect of producing a gmon.out file. To retrieve the data, the following command can then be used.

gprof _build/install/default/lambdapi gmon.out > profile.txt

It takes two arguments: the path to the lambdapi binary used to generate the profiling data, and the profiling data itself.