The Makefile generated by lambdapi init is not that nice since it is calling lambdapi only once with all the files as argument so that files are not checked in parallel according to their dependencies and the option -j we could pass to make.
We should add a command lambdapi dep to automatically include the dependencies in a Makefile with
include .depends
.depends: $(SRC)
lambdapi dep $(SRC) > $@
This could be done via a script like https://github.com/Deducteam/hol2dk/blob/main/dep-lpo but more elaborated because, in general, require (and require open) commands can appear any where, may have several arguments, and may be written on several lines.
Some tests could then be run in parallel using make instead of for f in ... do ... done.
The Makefile generated by lambdapi init is not that nice since it is calling lambdapi only once with all the files as argument so that files are not checked in parallel according to their dependencies and the option -j we could pass to make. We should add a command
lambdapi depto automatically include the dependencies in a Makefile withThis could be done via a script like https://github.com/Deducteam/hol2dk/blob/main/dep-lpo but more elaborated because, in general, require (and require open) commands can appear any where, may have several arguments, and may be written on several lines. Some tests could then be run in parallel using make instead of
for f in ... do ... done.