Permalink
Browse files

Added LICENSE and README.

  • Loading branch information...
Wouter Swierstra
Wouter Swierstra committed Jan 10, 2012
1 parent 9f9c3fb commit 832c52055dcb0c81ec3aff5f9284c23559c15648
Showing with 69 additions and 0 deletions.
  1. +32 −0 LICENSE
  2. +37 −0 README
View
32 LICENSE
@@ -0,0 +1,32 @@
+Copyright (c) 2007,2008 Spencer Janssen
+Copyright (c) 2007,2008 Don Stewart
+Copyright (c) 2010, Wouter Swierstra
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the author nor the names of his contributors
+ may be used to endorse or promote products derived from this software
+ without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR
+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
View
37 README
@@ -0,0 +1,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

0 comments on commit 832c520

Please sign in to comment.