From 34467c6df6709757c42aee5356b25a40148d90ea Mon Sep 17 00:00:00 2001
From: Derek Dreyer <dreyer@mpi-sws.org>
Date: Tue, 7 Oct 2014 09:58:46 +0200
Subject: [PATCH] edits to README file

---
 README.txt | 36 +++++++++++++++++++++++++++---------
 1 file changed, 27 insertions(+), 9 deletions(-)

diff --git a/README.txt b/README.txt
index 630881f42..9829c11cf 100644
--- a/README.txt
+++ b/README.txt
@@ -17,14 +17,29 @@ DESCRIPTION
 
 CONTENTS
 
+  Our artifact is a Coq formalization of the model of our Iris logic,
+  together with a proof of adequacy (establishing that the model is
+  faithful wrt the operational semantics), and a proof of soundness of
+  the primitive rules of the logic wrt the model.
+
+
   The folder is organized as follows:
+
   * core_lang.v contains the axioms about the language
-  * lang.v defines the threadpool reduction and derives some lemmas from core_lang.v
+
+  * lang.v defines the threadpool reduction and derives some lemmas
+    from core_lang.v
+  
   * masks.v introduces some lemmas about masks
-  * world_prop.v uses the aforementioned Coq library to construct the domain for Iris propositions
-  * iris.v is the main file and contains the actual logic and the proof of the rules for view shifts and Hoare triples
+  
+  * world_prop.v uses the aforementioned Coq library to construct the
+    domain for Iris propositions
+  
+  * iris.v is the main file and contains the actual logic and the
+    proof of the rules for view shifts and Hoare triples
 
-  It uses a Coq library in lib/ by Sieczkowski et al. to solve the recursive domain equation (see the paper for a reference).
+  It uses a Coq library in lib/ by Sieczkowski et al. to solve the
+  recursive domain equation (see the paper for a reference).
 
 
 REQUIREMENTS
@@ -32,8 +47,9 @@ REQUIREMENTS
   Coq 
   8GB ram + 4GB swap
 
-  We have tested the development using Coq v. 8.4pl4 on Linux and Mac machines with at least 8GB RAM + 4GB swap.
-  The entire compilation took around 3 hours.
+  We have tested the development using Coq v. 8.4pl4 on Linux and Mac
+  machines with at least 8GB RAM + 4GB swap.  The entire compilation
+  took around 3 hours.
   
 
 HOW TO COMPILE
@@ -44,13 +60,15 @@ HOW TO COMPILE
 
   in the folder containing this README. 
 
-  Be aware that iris.v takes a long time to check and needs significant amounts of RAM!
-  8GiB may be sufficient, but to be safe you should have 16GiB and give it around 2 to 3 hours.
+  Be aware that iris.v takes a long time to check and needs
+  significant amounts of RAM!
+  
 
 
 OVERVIEW OF LEMMAS
 
-  Below we give a mapping from proof rules in the paper to Coq lemma's in Iris.v
+  Below we give a mapping from proof rules in the paper to Coq lemma's
+  in Iris.v.
 
   RULE         Coq lemma
   -----------------------
-- 
GitLab