package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a
sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf
doc/lambdapi.tool/Tool/External/index.html
Module Tool.External
Source
Provides a function for calling external checkers using a Unix command.
run prop pp cmd sign
runs the external checker given by the Unix command cmd
on the signature sign
. The signature is processed and written to a Unix pipe using the formatter pp
, and the produced output is fed to the command on its standard output. The return value is Some true
in case of a successful check, Some false
in the case of a failed check, and None
if the external tool cannot conclude. Note that the command cmd
should write either "YES"
, "NO"
or "MAYBE"
as its first line of (standard) output. The exception Fatal
may be raised if cmd
exhibits a different behavior. The name prop
is used to refer to the checked property when an error message is displayed.
NOTE that for any given property being checked, the simplest possible valid command is "echo MAYBE"
. Moreover, "cat > file; echo MAYBE"
can conveniently be used to write generated data to the file "file"
. This is useful for debugging purposes.