Skip to content

Commit fd95c9f

Browse files
palmskogpalmskog
authored
Merge pull request #15 from DistributedComponents/theories-dir
reorganize files and switch to dune in Coq library opam packages
2 parents 91f5550 + 5640de2 commit fd95c9f

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

55 files changed

+254
-538
lines changed

‎Core/Make‎

Lines changed: 0 additions & 27 deletions
This file was deleted.

‎Core/Makefile‎

Lines changed: 0 additions & 14 deletions
This file was deleted.

‎Examples/Make‎

Lines changed: 0 additions & 28 deletions
This file was deleted.

‎Examples/Makefile‎

Lines changed: 0 additions & 14 deletions
This file was deleted.

‎_CoqProject‎

Lines changed: 43 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
1-
-Q Core DiSeL
2-
-Q Examples DiSeL
1+
-Q theories DiSeL
32

43
-arg -w -arg -notation-overridden
54
-arg -w -arg -local-declaration
@@ -9,45 +8,45 @@
98
-arg -w -arg -notation-incompatible-format
109
-arg -w -arg -deprecated-hint-without-locality
1110

12-
Core/State.v
13-
Core/Freshness.v
14-
Core/Protocols.v
15-
Core/EqTypeX.v
16-
Core/DepMaps.v
17-
Core/StatePredicates.v
18-
Core/NewStatePredicates.v
19-
Core/Worlds.v
20-
Core/NetworkSem.v
21-
Core/Rely.v
22-
Core/Actions.v
23-
Core/Injection.v
24-
Core/InductiveInv.v
25-
Core/Process.v
26-
Core/Always.v
27-
Core/HoareTriples.v
28-
Core/InferenceRules.v
29-
Core/While.v
30-
Core/DiSeLExtraction.v
31-
Examples/SeqLib.v
32-
Examples/Greeter/Greeter.v
33-
Examples/Querying/QueryProtocol.v
34-
Examples/Querying/QueryHooked.v
35-
Examples/Calculator/CalculatorProtocol.v
36-
Examples/Calculator/CalculatorInvariant.v
37-
Examples/Calculator/CalculatorClientLib.v
38-
Examples/Calculator/CalculatorServerLib.v
39-
Examples/Calculator/SimpleCalculatorServers.v
40-
Examples/Calculator/DelegatingCalculatorServer.v
41-
Examples/Calculator/SimpleCalculatorApp.v
42-
Examples/Calculator/CalculatorExtraction.v
43-
Examples/TwoPhaseCommit/TwoPhaseProtocol.v
44-
Examples/TwoPhaseCommit/TwoPhaseCoordinator.v
45-
Examples/TwoPhaseCommit/TwoPhaseParticipant.v
46-
Examples/TwoPhaseCommit/SimpleTPCApp.v
47-
Examples/TwoPhaseCommit/TwoPhaseExtraction.v
48-
Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v
49-
Examples/TwoPhaseCommit/TwoPhaseInductiveProof.v
50-
Examples/TwoPhaseCommit/TwoPhaseClient.v
51-
Examples/Querying/QueryPlusTPC.v
52-
Examples/LockResource/LockProtocol.v
53-
Examples/LockResource/ResourceProtocol.v
11+
theories/Core/State.v
12+
theories/Core/Freshness.v
13+
theories/Core/Protocols.v
14+
theories/Core/EqTypeX.v
15+
theories/Core/DepMaps.v
16+
theories/Core/StatePredicates.v
17+
theories/Core/NewStatePredicates.v
18+
theories/Core/Worlds.v
19+
theories/Core/NetworkSem.v
20+
theories/Core/Rely.v
21+
theories/Core/Actions.v
22+
theories/Core/Injection.v
23+
theories/Core/InductiveInv.v
24+
theories/Core/Process.v
25+
theories/Core/Always.v
26+
theories/Core/HoareTriples.v
27+
theories/Core/InferenceRules.v
28+
theories/Core/While.v
29+
theories/Core/DiSeLExtraction.v
30+
theories/Examples/SeqLib.v
31+
theories/Examples/Greeter/Greeter.v
32+
theories/Examples/Querying/QueryProtocol.v
33+
theories/Examples/Querying/QueryHooked.v
34+
theories/Examples/Calculator/CalculatorProtocol.v
35+
theories/Examples/Calculator/CalculatorInvariant.v
36+
theories/Examples/Calculator/CalculatorClientLib.v
37+
theories/Examples/Calculator/CalculatorServerLib.v
38+
theories/Examples/Calculator/SimpleCalculatorServers.v
39+
theories/Examples/Calculator/DelegatingCalculatorServer.v
40+
theories/Examples/Calculator/SimpleCalculatorApp.v
41+
theories/Examples/TwoPhaseCommit/TwoPhaseProtocol.v
42+
theories/Examples/TwoPhaseCommit/TwoPhaseCoordinator.v
43+
theories/Examples/TwoPhaseCommit/TwoPhaseParticipant.v
44+
theories/Examples/TwoPhaseCommit/SimpleTPCApp.v
45+
theories/Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v
46+
theories/Examples/TwoPhaseCommit/TwoPhaseInductiveProof.v
47+
theories/Examples/TwoPhaseCommit/TwoPhaseClient.v
48+
theories/Examples/Querying/QueryPlusTPC.v
49+
theories/Examples/LockResource/LockProtocol.v
50+
theories/Examples/LockResource/ResourceProtocol.v
51+
extraction/calculator/CalculatorExtraction.v
52+
extraction/TPC/TwoPhaseExtraction.v

‎coq-disel-examples.opam‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,11 @@ bug-reports: "https://github.com/DistributedComponents/disel/issues"
88
license: "BSD-2-Clause"
99
synopsis: "Example systems for Disel, a separation-style logic for compositional verification of distributed systems in Coq"
1010

11-
build: [make "-j%{jobs}%" "-C" "Examples"]
12-
install: [make "-C" "Examples" "install"]
11+
build: ["dune" "build" "-p" name "-j" jobs]
1312
depends: [
1413
"coq" {>= "8.14"}
1514
"coq-mathcomp-ssreflect" {>= "1.13"}
1615
"coq-fcsl-pcm" {>= "1.7.0"}
17-
"coq-htt" {>= "1.2.0"}
1816
"coq-disel" {= version}
1917
]
2018

@@ -23,7 +21,7 @@ tags: [
2321
"keyword:program verification"
2422
"keyword:separation logic"
2523
"keyword:distributed algorithms"
26-
"logpath:DiSeL"
24+
"logpath:DiSeL.Examples"
2725
]
2826
authors: [
2927
"Ilya Sergey"

‎coq-disel.opam‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,9 @@ communication primitives. Components of composite systems are specified in Disel
1717
as protocols, which capture system-specific logic and disentangle system definitions
1818
from implementation details."""
1919

20-
build: [make "-j%{jobs}%" "-C" "Core"]
21-
install: [make "-C" "Core" "install"]
20+
build: ["dune" "build" "-p" name "-j" jobs]
2221
depends: [
22+
"dune" {>= "2.5"}
2323
"coq" {>= "8.14"}
2424
"coq-mathcomp-ssreflect" {>= "1.13"}
2525
"coq-fcsl-pcm" {>= "1.7.0"}
@@ -31,7 +31,7 @@ tags: [
3131
"keyword:program verification"
3232
"keyword:separation logic"
3333
"keyword:distributed algorithms"
34-
"logpath:DiSeL"
34+
"logpath:DiSeL.Core"
3535
]
3636
authors: [
3737
"Ilya Sergey"

‎dune-project‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
(lang dune 2.5)
2+
(using coq 0.2)
3+
(name disel)

‎extraction/TPC/.gitkeep‎

Whitespace-only changes.

Examples/TwoPhaseCommit/TwoPhaseExtraction.v renamed to extraction/TPC/TwoPhaseExtraction.v

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,5 @@
1-
From DiSeL
2-
Require Import DiSeLExtraction.
3-
From DiSeL
4-
Require Import SimpleTPCApp.
1+
From DiSeL Require Import DiSeLExtraction.
2+
From DiSeL Require Import SimpleTPCApp.
53

64
Cd "extraction".
75
Cd "TPC".

0 commit comments

Comments
 (0)