You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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 text was updated successfully, but these errors were encountered:
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 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
.The text was updated successfully, but these errors were encountered: