From d75da809429d5d2d40d108608db9e5acd9aec9c9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 11:08:37 +0200
Subject: STM: support for nested boxes of nodes to model error boundaries

Dag extended to support arbitrary clusters, renamed to Property.
Vcs generalized to not impose the data hold by a Property.
Stm(VCS) names a property "a box" and imposes a topological invariant (no
overlap).  It defines 2 kind of boxes: ProofTasks (the old cluster
notion) and ErrorBound (meant to confine errors to sub-proofs).

In the meanwhile more equations added to Make(..) functors in order to
have just one Stateid.Set module around.
---
 lib/stateid.ml  | 8 +++++++-
 lib/stateid.mli | 3 ++-
 2 files changed, 9 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/stateid.ml b/lib/stateid.ml
index c17df2b321..500581a39e 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -29,7 +29,13 @@ let get exn = Exninfo.get exn state_id_info
 let equal = Int.equal
 let compare = Int.compare
 
-module Set = Set.Make(struct type t = int let compare = compare end)
+module Self = struct
+ type t = int
+ let compare = compare
+ let equal = equal
+end
+
+module Set = Set.Make(Self)
 
 type ('a,'b) request = {
   exn_info : t * t;
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 516ad891ff..cd8fddf0ce 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -11,7 +11,8 @@ type t
 val equal : t -> t -> bool
 val compare : t -> t -> int
 
-module Set : Set.S with type elt = t
+module Self : Map.OrderedType with type t = t
+module Set : Set.S with type elt = t and type t = Set.Make(Self).t
 
 val initial : t
 val dummy : t
-- 
cgit v1.2.3


From 821937aee71bf9439158e27e06f7b4f74289b209 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 16:57:31 +0200
Subject: STM: proof block detection made optional + simple test

---
 lib/flags.ml  | 2 ++
 lib/flags.mli | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index c1ec9738ca..ecf3c3f168 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -68,6 +68,8 @@ let priority_of_string = function
   | "low" -> Low
   | "high" -> High
   | _ -> raise (Invalid_argument "priority_of_string")
+let async_proofs_tac_error_resilience = ref true
+let async_proofs_cmd_error_resilience = ref true
 
 let async_proofs_is_worker () =
   !async_proofs_worker_id <> "master"
diff --git a/lib/flags.mli b/lib/flags.mli
index 24780f0dcc..b26ef027c6 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -34,6 +34,8 @@ type priority = Low | High
 val async_proofs_worker_priority : priority ref
 val string_of_priority : priority -> string
 val priority_of_string : string -> priority
+val async_proofs_tac_error_resilience : bool ref
+val async_proofs_cmd_error_resilience : bool ref
 
 val debug : bool ref
 val in_debugger : bool ref
-- 
cgit v1.2.3


From 845dd3dd17b880999a956839c0d84d46de9e27b8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 5 Jun 2016 21:21:43 +0200
Subject: STM: each proof block can be enabled separately

By default we enable only {} and par: that are detectable in
a complete way.
---
 lib/flags.ml  | 3 ++-
 lib/flags.mli | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index ecf3c3f168..e78fa7c0c9 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -68,7 +68,8 @@ let priority_of_string = function
   | "low" -> Low
   | "high" -> High
   | _ -> raise (Invalid_argument "priority_of_string")
-let async_proofs_tac_error_resilience = ref true
+type tac_error_filter = [ `None | `Only of string list | `All ]
+let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "proof-block" ])
 let async_proofs_cmd_error_resilience = ref true
 
 let async_proofs_is_worker () =
diff --git a/lib/flags.mli b/lib/flags.mli
index b26ef027c6..d729be385b 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -34,7 +34,8 @@ type priority = Low | High
 val async_proofs_worker_priority : priority ref
 val string_of_priority : priority -> string
 val priority_of_string : string -> priority
-val async_proofs_tac_error_resilience : bool ref
+type tac_error_filter = [ `None | `Only of string list | `All ]
+val async_proofs_tac_error_resilience : tac_error_filter ref
 val async_proofs_cmd_error_resilience : bool ref
 
 val debug : bool ref
-- 
cgit v1.2.3


From 4dcd50dd2767c60f8f773fb4ca1c3d4bc68819c8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 7 Jun 2016 09:57:09 -0400
Subject: Documentation

---
 lib/flags.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index e78fa7c0c9..16996c144b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -69,7 +69,7 @@ let priority_of_string = function
   | "high" -> High
   | _ -> raise (Invalid_argument "priority_of_string")
 type tac_error_filter = [ `None | `Only of string list | `All ]
-let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "proof-block" ])
+let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "curly" ])
 let async_proofs_cmd_error_resilience = ref true
 
 let async_proofs_is_worker () =
-- 
cgit v1.2.3