From 79bf97113e0450eed4f994ba474d5f2957787aa0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 8 Jul 2014 20:01:19 +0200
Subject: [PATCH] add coq README

---
 README.txt | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 README.txt

diff --git a/README.txt b/README.txt
new file mode 100644
index 000000000..6eaa98ab6
--- /dev/null
+++ b/README.txt
@@ -0,0 +1,12 @@
+This folder contains the Coq development for Iris.
+It uses a Coq library in lib/ by Sieczkowski et al. to solve the recursive domain equation (see the paper for a reference).
+
+This 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
+* 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 tiples
+
+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.
-- 
GitLab