Awesome

This repository contains an implementation of xmonad's StackSet module in Coq. Extracting Haskell from this Coq file produces a drop-in replacement module for the original Haskell module (once it has been massaged a bit by a few innocuous shell scripts).

The Makefile has mostly been generated by coq_makefile. It contains several build targets:

• make patched_xmonad -- downloads xmonad and applies several reasonably innocent patches to the xmonad source;

• make extraction -- extract Haskell code from the Coq implementation of the StackSet module, and postprocess it with some final shell scripts;

• make integration -- tries to build the patched xmonad with the extracted StackSet module;

• make quickcheck -- also runs the QuickCheck testsuite on the resulting xmonad binary;

• make theorems -- gives some indication of how many QuickCheck properties have been formalized.

The Coq code is in the src/ directory. Most of the Coq code is in the StackSet.v module. The Extraction.v module has various extraction commands to generate somewhat palatable Haskell code. Several QuickCheck properties have alread been proven in the Properties.v file.

The necessary shell scripts and patches are all in the scripts/directory.