Input and output

Gappa reads the script whose filename is passed as an argument to the tool, or on its standard input if none. Such a script is made of three parts: the definitions, the logical formula, and the hints. Warning messages, error messages, and results, are displayed on the standard error output. Gappa also sends to the standard output a formal proof of the logical formula; its format depends on the selected back-end. Finally, if the tool was unable to prove some goals, its return code is a nonzero value.

For example, the following command lines create a simple script in file test.g, pass it to Gappa, and store the generated Coq proof in file test.v file. They also test the return code of Gappa and send the generated proof to Coq so that it is automatically checked. Since the proof checker does not display anything, it means no errors were detected and the result computed by Gappa is correct.

$ echo "{ x in [-2,2] -> x * x in ? }" > test.g

$ gappa -Bcoq test.g > test.v
  x * x in [0, 4]

$ echo "Return code is $?"
Return code is 0

$ coqc -I path/to/gappalib-coq test.v


Note that, if no ranges are left unspecified in the logical formula, Gappa will not have anything to display in case of success.

$ echo "{ 1 + 1 = 2 }" | gappa

$ echo "Return code is $?"
Return code is 0