Merge pull request #15 from DistributedComponents/theories-dir

reorganize files and switch to dune in Coq library opam packages

_CoqProject

@@ -1,5 +1,4 @@
--Q Core DiSeL
--Q Examples DiSeL
+-Q theories DiSeL
 
 -arg -w -arg -notation-overridden
 -arg -w -arg -local-declaration
@@ -9,45 +8,45 @@
 -arg -w -arg -notation-incompatible-format
 -arg -w -arg -deprecated-hint-without-locality
 
-Core/State.v
-Core/Freshness.v
-Core/Protocols.v
-Core/EqTypeX.v
-Core/DepMaps.v
-Core/StatePredicates.v
-Core/NewStatePredicates.v
-Core/Worlds.v
-Core/NetworkSem.v
-Core/Rely.v
-Core/Actions.v
-Core/Injection.v
-Core/InductiveInv.v
-Core/Process.v
-Core/Always.v
-Core/HoareTriples.v
-Core/InferenceRules.v
-Core/While.v
-Core/DiSeLExtraction.v
-Examples/SeqLib.v
-Examples/Greeter/Greeter.v
-Examples/Querying/QueryProtocol.v
-Examples/Querying/QueryHooked.v
-Examples/Calculator/CalculatorProtocol.v
-Examples/Calculator/CalculatorInvariant.v
-Examples/Calculator/CalculatorClientLib.v
-Examples/Calculator/CalculatorServerLib.v
-Examples/Calculator/SimpleCalculatorServers.v
-Examples/Calculator/DelegatingCalculatorServer.v
-Examples/Calculator/SimpleCalculatorApp.v
-Examples/Calculator/CalculatorExtraction.v
-Examples/TwoPhaseCommit/TwoPhaseProtocol.v
-Examples/TwoPhaseCommit/TwoPhaseCoordinator.v
-Examples/TwoPhaseCommit/TwoPhaseParticipant.v
-Examples/TwoPhaseCommit/SimpleTPCApp.v
-Examples/TwoPhaseCommit/TwoPhaseExtraction.v
-Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v
-Examples/TwoPhaseCommit/TwoPhaseInductiveProof.v
-Examples/TwoPhaseCommit/TwoPhaseClient.v
-Examples/Querying/QueryPlusTPC.v
-Examples/LockResource/LockProtocol.v
-Examples/LockResource/ResourceProtocol.v
+theories/Core/State.v
+theories/Core/Freshness.v
+theories/Core/Protocols.v
+theories/Core/EqTypeX.v
+theories/Core/DepMaps.v
+theories/Core/StatePredicates.v
+theories/Core/NewStatePredicates.v
+theories/Core/Worlds.v
+theories/Core/NetworkSem.v
+theories/Core/Rely.v
+theories/Core/Actions.v
+theories/Core/Injection.v
+theories/Core/InductiveInv.v
+theories/Core/Process.v
+theories/Core/Always.v
+theories/Core/HoareTriples.v
+theories/Core/InferenceRules.v
+theories/Core/While.v
+theories/Core/DiSeLExtraction.v
+theories/Examples/SeqLib.v
+theories/Examples/Greeter/Greeter.v
+theories/Examples/Querying/QueryProtocol.v
+theories/Examples/Querying/QueryHooked.v
+theories/Examples/Calculator/CalculatorProtocol.v
+theories/Examples/Calculator/CalculatorInvariant.v
+theories/Examples/Calculator/CalculatorClientLib.v
+theories/Examples/Calculator/CalculatorServerLib.v
+theories/Examples/Calculator/SimpleCalculatorServers.v
+theories/Examples/Calculator/DelegatingCalculatorServer.v
+theories/Examples/Calculator/SimpleCalculatorApp.v
+theories/Examples/TwoPhaseCommit/TwoPhaseProtocol.v
+theories/Examples/TwoPhaseCommit/TwoPhaseCoordinator.v
+theories/Examples/TwoPhaseCommit/TwoPhaseParticipant.v
+theories/Examples/TwoPhaseCommit/SimpleTPCApp.v
+theories/Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v
+theories/Examples/TwoPhaseCommit/TwoPhaseInductiveProof.v
+theories/Examples/TwoPhaseCommit/TwoPhaseClient.v
+theories/Examples/Querying/QueryPlusTPC.v
+theories/Examples/LockResource/LockProtocol.v
+theories/Examples/LockResource/ResourceProtocol.v
+extraction/calculator/CalculatorExtraction.v
+extraction/TPC/TwoPhaseExtraction.v

coq-disel-examples.opam

@@ -8,13 +8,11 @@ bug-reports: "https://github.com/DistributedComponents/disel/issues"
 license: "BSD-2-Clause"
 synopsis: "Example systems for Disel, a separation-style logic for compositional verification of distributed systems in Coq"
 
-build: [make "-j%{jobs}%" "-C" "Examples"]
-install: [make "-C" "Examples" "install"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "coq" {>= "8.14"}
   "coq-mathcomp-ssreflect" {>= "1.13"}
   "coq-fcsl-pcm" {>= "1.7.0"}
-  "coq-htt" {>= "1.2.0"}
   "coq-disel" {= version}
 ]
 
@@ -23,7 +21,7 @@ tags: [
   "keyword:program verification"
   "keyword:separation logic"
   "keyword:distributed algorithms"
-  "logpath:DiSeL"
+  "logpath:DiSeL.Examples"
 ]
 authors: [
   "Ilya Sergey"

coq-disel.opam

@@ -17,9 +17,9 @@ communication primitives. Components of composite systems are specified in Disel
 as protocols, which capture system-specific logic and disentangle system definitions
 from implementation details."""
 
-build: [make "-j%{jobs}%" "-C" "Core"]
-install: [make "-C" "Core" "install"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
+  "dune" {>= "2.5"}
   "coq" {>= "8.14"}
   "coq-mathcomp-ssreflect" {>= "1.13"}
   "coq-fcsl-pcm" {>= "1.7.0"}
@@ -31,7 +31,7 @@ tags: [
   "keyword:program verification"
   "keyword:separation logic"
   "keyword:distributed algorithms"
-  "logpath:DiSeL"
+  "logpath:DiSeL.Core"
 ]
 authors: [
   "Ilya Sergey"

dune-project

@@ -0,0 +1,3 @@
+(lang dune 2.5)
+(using coq 0.2)
+(name disel)

Examples/TwoPhaseCommit/TwoPhaseExtraction.v → extraction/TPC/TwoPhaseExtraction.v

@@ -1,7 +1,5 @@
-From DiSeL
-Require Import DiSeLExtraction.
-From DiSeL
-Require Import SimpleTPCApp.
+From DiSeL Require Import DiSeLExtraction.
+From DiSeL Require Import SimpleTPCApp.
 
 Cd "extraction".
   Cd "TPC".

Examples/Calculator/CalculatorExtraction.v → extraction/calculator/CalculatorExtraction.v

@@ -1,7 +1,5 @@
-From DiSeL
-Require Import DiSeLExtraction.
-From DiSeL
-Require Import SimpleCalculatorApp.
+From DiSeL Require Import DiSeLExtraction.
+From DiSeL Require Import SimpleCalculatorApp.
 
 Cd "extraction".
   Cd "calculator".

Core/Actions.v → theories/Core/Actions.v

@@ -1,14 +1,8 @@
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From mathcomp
-Require Import path.
-Require Import Eqdep.
-Require Import Relation_Operators.
-From pcm
-Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
-From DiSeL
-Require Import Freshness State EqTypeX Protocols Worlds NetworkSem.
-Require Classical_Prop.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
+From Coq Require Import Eqdep Relation_Operators.
+From pcm Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL Require Import Freshness State EqTypeX Protocols Worlds NetworkSem.
+From Coq Require Classical_Prop.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

Core/DepMaps.v → theories/Core/DepMaps.v

@@ -1,13 +1,7 @@
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From mathcomp
-Require Import path.
-Require Import Eqdep.
-Require Import Relation_Operators.
-From pcm
-Require Import pred prelude ordtype finmap pcm unionmap heap.
-From DiSeL
-Require Import Freshness EqTypeX.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
+From Coq Require Import Eqdep Relation_Operators.
+From pcm Require Import pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL Require Import Freshness EqTypeX.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.

Core/DiSeLExtraction.v → theories/Core/DiSeLExtraction.v

@@ -1,7 +1,5 @@
-From DiSeL
-Require Import While.
-
-Require Import ExtrOcamlBasic.
+From DiSeL Require Import While.
+From Coq Require Import ExtrOcamlBasic.
 
 Extraction Inline ssrbool.SimplPred.
 

Core/EqTypeX.v → theories/Core/EqTypeX.v

@@ -1,9 +1,5 @@
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From mathcomp
-Require Import path.
-Require Import Eqdep.
-Require Import Relation_Operators.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
+From Coq Require Import Eqdep Relation_Operators.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

Core/HoareTriples.v → theories/Core/HoareTriples.v

@@ -383,8 +383,7 @@ Definition inject := with_spec (DTbin_make inject_has_spec).
 
 End Inject.
 
-From DiSeL
-Require Import InductiveInv.
+From DiSeL Require Import InductiveInv.
 
 Section InductiveInv.
 Variable pr : protocol.

Core/InductiveInv.v → theories/Core/InductiveInv.v

@@ -1,14 +1,9 @@
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From mathcomp
-Require Import path.
-Require Import Eqdep.
-Require Import Relation_Operators.
-From pcm
-Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
-From DiSeL
-Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
-Require FunctionalExtensionality.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
+From Coq Require Import Eqdep Relation_Operators.
+From pcm Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL Require Import Freshness State EqTypeX Protocols.
+From DiSeL Require Import Worlds NetworkSem Rely.
+From Coq Require FunctionalExtensionality.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.

Core/Injection.v → theories/Core/Injection.v

@@ -1,13 +1,8 @@
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From mathcomp
-Require Import path.
-Require Import Eqdep.
-Require Import Relation_Operators.
-From pcm
-Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
-From DiSeL
-Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Actions.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
+From Coq Require Import Eqdep Relation_Operators.
+From pcm Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL Require Import Freshness State EqTypeX Protocols.
+From DiSeL Require Import Worlds NetworkSem Actions.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.

Core/NetworkSem.v → theories/Core/NetworkSem.v

@@ -1,18 +1,11 @@
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From mathcomp
-Require Import path.
-Require Import Eqdep.
-Require Import Relation_Operators.
-From pcm
-Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
-From DiSeL
-Require Import Freshness State EqTypeX Protocols Worlds.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
+From Coq Require Import Eqdep Relation_Operators.
+From pcm Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL Require Import Freshness State EqTypeX Protocols Worlds.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-
 (* Operational semantics of the network *)
 
 Section NetworkSemantics.