-
Notifications
You must be signed in to change notification settings - Fork 8
/
README
37 lines (24 loc) · 1.26 KB
/
README
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