Focalide is the name of the Dedukti output of the FoCaLiZe compiler. It relies on the Dedukti output of the Zenon Modulo theorem prover for deduction modulo and on Sukerujo, a syntaxic extension of Dedukti. Focalide is developed by Raphaël Cauderlier.
Focalide is included in FoCaLiZe, it can be installed using the Opam Package Manager.
$ opam repository add deducteam git://scm.gforge.inria.fr/opam-deducteam/opam-deducteam.git $ opam update $ opam install focalize=focalide
If you prefer to install Focalide from source, you can download the code as a tarball.
FoCaLiZe compiler is invoked by the command focalizec.
If you are only interested in the Dedukti output, you can ask the
compiler not to output Coq and Ocaml code:
$ focalizec -no-coq-code -no-ocaml-code my_file.fcl
This will generate a file my_file.sk in Sukerujo format and check it.
Alternatively, you can ask the compiler not to check the file:
$ focalizec -no-coq-code -no-ocaml-code -stop-before-dedukti my_file.fcl
In both cases, the .sk file can be translated to pure Dedukti format by issuing the following command:
$ skindent my_file.sk > my_file.dk
Finally, this file can be checked by Dedukti.
$ FOCALIZE_LIB=`focalizec -where | cut -d ' ' -f 2` $ dkcheck -I "$FOCALIZE_LIB" -nl my_file.dk
Focalide performance compared to FoCaLiZe backend to Coq are usually comparable; the generated Sukerujo file is usually approximately twice as big as the corresponding Coq file and the time used by Zenon Modulo and Dedukti for finding and checking the proofs is almost always shorter than the time used by Zenon and Coq.
For more details, we provide a benchmark consisting of several FoCaLiZe libraries.