Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
xmonad in Coq
Coq Haskell
Branch: master
Failed to load latest commit information.
scripts Shifted to xmonad version 0.10
src Added logo
.gitignore Add .DS_Store to .gitignore
LICENSE Added LICENSE and README.
Makefile Added logo
README.md Removed logo from repository.

README.md

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.

Something went wrong with that request. Please try again.