Running the tutorial

[jnarboux]

Hi,

I installed lambdapi lambdapi-logic lambdapi-blanqui-lib using opam:

Packages matching: match(lambdapi)

Name # Installed # Synopsis

lambdapi 2.2.1 Proof assistant for the λΠ-cal
lambdapi-blanqui-lib 0.0.0 Library on natural numbers and p
lambdapi-logic 0.0.0 Repository of logic definitions

I created a package using lambdapi init and copied the tutorial file in the directory:
I seems that lambdapi can not find some tests files necessary for the tutorial:
"/Users/jnarboux/.opam/4.09.0/lib/lambdapi/lib_root/tests/OK/logic.lp" (or .dk) not found.
How should I install it ?

On the contrary require Logic.U.Set; works.

Julien

[fblanqui]

Hi Julien. Test files are used by developers only and are not installed. The fact that the tutorial is among test files is not very satisfactory indeed if it requires uninstalled files. I should fix this by either removing the require or adding a package including the tutorial.

Edit: See #919.