Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
How to install the gappa tactic?
[go: Go Back, main page]

How to instal the gappa tactic?

Only steps 1 and 2 are needed to use the gappa tactic. The other steps are needed to use it in conjunction with the Caduceus tool and the Why platform.

Steps 2 and 3 can be done in parallel.

  1. Download and install Coq. You need at least Coq V8.2. See here.
  2. Download, compile and install Gappa and its support library. See here.
  3. Download, compile and install the PFF library about floating-point arithmetic. See here.
  4. Download, compile and install the Why platform that includes Caduceus. See here.
  5. Download, compile and install the Why2Gappa file.