Merge pull request #16 from DistributedComponents/fix-coq-dev-deprecations

fix deprecations in Coq and OCaml

Author: palmskog

Makefile

@@ -1,4 +1,4 @@
-OCAMLBUILD = ocamlbuild -tag safe_string -libs unix -I shims
+OCAMLBUILD = ocamlbuild -tag safe_string -pkg unix -I shims
 
 default: Makefile.coq
 	$(MAKE) -f Makefile.coq

README.md

@@ -99,7 +99,7 @@ without printing "error".
 
 Extracting and running the example applications is described below.
 
-## Code corresponding to the paper
+### Code corresponding to the paper
 
 The following describes how the paper corresponds to the code:
 
@@ -156,7 +156,7 @@ The following describes how the paper corresponds to the code:
     - The querying protocol from Section 4.4 is implemented in the directory
       `Examples/Querying`.
 
-## Exploring further
+### Exploring further
 
 We encourage you to explore Disel further by extending one of the
 examples or trying your own. For example, you could build an application
@@ -166,7 +166,7 @@ protocol for leader election in a ring and prove that at most one node
 becomes leader. To get started, we recommend following the Calculator example
 and modifying it as necessary.
 
-## Extracting and Running Disel Programs
+### Extracting and Running Disel Programs
 
 As described in Section 5.1, Disel programs can be extracted to OCaml and run.
 You can build the two examples as follows.
@@ -272,7 +272,7 @@ got msg in protocol 0 with tag = 5, contents = [0] from 2
   respond with AckAbort messages (tag 6). Once all four rounds are over,
   all nodes exit.
 
-## Proof Size Statistics
+### Proof Size Statistics
 
 Section 5.2 and Table 1 describe the size of our development. Those
 were obtained by using the `coqwc` tool on manually dissected files,

_CoqProject

@@ -6,7 +6,6 @@
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -duplicate-clear
 -arg -w -arg -notation-incompatible-format
--arg -w -arg -deprecated-hint-without-locality
 
 theories/Core/State.v
 theories/Core/Freshness.v

meta.yml

@@ -133,7 +133,7 @@ documentation: |-
   
   Extracting and running the example applications is described below.
   
-  ## Code corresponding to the paper
+  ### Code corresponding to the paper
   
   The following describes how the paper corresponds to the code:
   
@@ -190,7 +190,7 @@ documentation: |-
       - The querying protocol from Section 4.4 is implemented in the directory
         `Examples/Querying`.
   
-  ## Exploring further
+  ### Exploring further
   
   We encourage you to explore Disel further by extending one of the
   examples or trying your own. For example, you could build an application
@@ -200,7 +200,7 @@ documentation: |-
   becomes leader. To get started, we recommend following the Calculator example
   and modifying it as necessary.
   
-  ## Extracting and Running Disel Programs
+  ### Extracting and Running Disel Programs
   
   As described in Section 5.1, Disel programs can be extracted to OCaml and run.
   You can build the two examples as follows.
@@ -306,7 +306,7 @@ documentation: |-
     respond with AckAbort messages (tag 6). Once all four rounds are over,
     all nodes exit.
   
-  ## Proof Size Statistics
+  ### Proof Size Statistics
   
   Section 5.2 and Table 1 describe the size of our development. Those
   were obtained by using the `coqwc` tool on manually dissected files,

theories/Core/HoareTriples.v

@@ -12,7 +12,7 @@ Unset Printing Implicit Defensive.
 Structure prog (W : world) A (this : nid) :=
   Prog {
       set_of : proc this W A -> Prop; 
-      (* Unifinshed is a bottom element that should be present *)
+      (* Unfinished is a bottom element that should be present *)
       _ : set_of Unfinished
   }.
 
@@ -441,7 +441,7 @@ Lemma conseq_refl (W : world) A this (e : DT this W A) :
   conseq e (spec_of e).
 Proof. by case: e; case=>p q [T H i] /= Hp C t; apply: H. Qed.
 
-Hint Resolve conseq_refl : core.
+#[export] Hint Resolve conseq_refl : core.
 
 
 (* Weakening the specifications *)

theories/Core/dune

@@ -8,5 +8,4 @@
    -w -local-declaration
    -w -duplicate-clear
    -w -redundant-canonical-projection
-   -w -projection-no-head-constant
-   -w -deprecated-hint-without-locality))
+   -w -projection-no-head-constant))