Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: a717951a2f
Fetching contributors…

Octocat-spinner-32-eaf2f5

Cannot retrieve contributors at this time

file 37 lines (24 sloc) 1.294 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37


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.


Author:

Wouter Swierstra
Something went wrong with that request. Please try again.