Commit eca1d3c9 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

More standard directory layout, silence warnings.

parent f01fa68f
...@@ -13,7 +13,7 @@ clean: Makefile.coq ...@@ -13,7 +13,7 @@ clean: Makefile.coq
rm -f Makefile.coq rm -f Makefile.coq
Makefile.coq: _CoqProject Makefile Makefile.coq: _CoqProject Makefile
coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq coq_makefile -f _CoqProject -o Makefile.coq
_CoqProject: ; _CoqProject: ;
......
...@@ -46,7 +46,6 @@ More info on the Coq development of Iris: [there][coq-iris]. ...@@ -46,7 +46,6 @@ More info on the Coq development of Iris: [there][coq-iris].
To compile the Coq scripts: To compile the Coq scripts:
cd src/
make make
The first time (and each time `_CoqProject` is updated), it also creates the The first time (and each time `_CoqProject` is updated), it also creates the
...@@ -132,4 +131,3 @@ In `TimeReceipts.v`: ...@@ -132,4 +131,3 @@ In `TimeReceipts.v`:
matches the interface is stated by `TR_implementation`. matches the interface is stated by `TR_implementation`.
* The “Credit Exhaustion” lemma is `simulation_exec_failure_now`. * The “Credit Exhaustion” lemma is `simulation_exec_failure_now`.
* The “Soundness of Iris^⧗ ” lemma is `abstract_spec_trtranslation__adequate`. * The “Soundness of Iris^⧗ ” lemma is `abstract_spec_trtranslation__adequate`.
-Q theories iris_time
-arg -w -arg -notation-overridden
theories/Auth_mnat.v
theories/Auth_nat.v
theories/ClockIntegers.v
theories/Examples.v
theories/Misc.v
theories/Reduction.v
theories/Tactics.v
theories/Simulation.v
theories/Thunks.v
theories/TimeCredits.v
theories/TimeCreditsAltProofs.v
theories/TimeReceipts.v
theories/Translation.v
ARCHIVE=iris-time-proofs.tar.gz ARCHIVE=iris-time-proofs.tar.gz
rm -f $ARCHIVE rm -f $ARCHIVE
tar -czvf $ARCHIVE README.md src/Makefile src/_CoqProject src/*.v tar -czvf $ARCHIVE README.md Makefile _CoqProject theories/*.v
-Q . ""
Auth_mnat.v
Auth_nat.v
ClockIntegers.v
Examples.v
Misc.v
Reduction.v
Tactics.v
Simulation.v
Thunks.v
TimeCredits.v
TimeCreditsAltProofs.v
TimeReceipts.v
Translation.v
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Require Import TimeReceipts. From iris_time Require Import TimeReceipts.
Require Import stdpp.numbers. From stdpp Require Import numbers.
Open Scope Z_scope. Open Scope Z_scope.
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.program_logic Require Import adequacy. From iris.program_logic Require Import adequacy.
Require Import TimeCredits Reduction. From iris_time Require Import TimeCredits Reduction.
(** A function that sums all elements of a list, defined as a heap-lang value: *) (** A function that sums all elements of a list, defined as a heap-lang value: *)
Definition sum_list : val := Definition sum_list : val :=
...@@ -195,7 +195,7 @@ Proof. ...@@ -195,7 +195,7 @@ Proof.
iApply "Post". eauto with iFrame. iApply "Post". eauto with iFrame.
Qed. Qed.
Let prgm (n : nat) : expr := Definition prgm (n : nat) : expr :=
sum_list (make_list #n). sum_list (make_list #n).
Lemma length_make_list_coq (n : nat) : Lemma length_make_list_coq (n : nat) :
......
...@@ -2,7 +2,7 @@ From iris.heap_lang Require Import lang notation. ...@@ -2,7 +2,7 @@ From iris.heap_lang Require Import lang notation.
From iris.heap_lang Require Import adequacy. From iris.heap_lang Require Import adequacy.
From stdpp Require Import relations fin_maps gmap. From stdpp Require Import relations fin_maps gmap.
Require Import Misc Tactics. From iris_time Require Import Misc Tactics.
Implicit Type e : expr. Implicit Type e : expr.
Implicit Type v : val. Implicit Type v : val.
......
From iris.heap_lang Require Import notation proofmode. From iris.heap_lang Require Import notation proofmode.
From iris.program_logic Require Import adequacy. From iris.program_logic Require Import adequacy.
Require Import Misc Reduction Tactics. From iris_time Require Import Misc Reduction Tactics.
Require Export Translation. From iris_time Require Export Translation.
Implicit Type e : expr. Implicit Type e : expr.
Implicit Type v : val. Implicit Type v : val.
......
...@@ -2,7 +2,7 @@ From iris.heap_lang Require Import proofmode notation. ...@@ -2,7 +2,7 @@ From iris.heap_lang Require Import proofmode notation.
From iris.base_logic.lib Require Import na_invariants. From iris.base_logic.lib Require Import na_invariants.
From stdpp Require Import namespaces. From stdpp Require Import namespaces.
Require Import TimeCredits Auth_mnat. From iris_time Require Import TimeCredits Auth_mnat.
Section Thunk. Section Thunk.
......
From iris.heap_lang Require Import proofmode notation adequacy. From iris.heap_lang Require Import proofmode notation adequacy.
From iris.base_logic Require Import invariants. From iris.base_logic Require Import invariants.
Require Import Auth_nat Misc Reduction Tactics. From iris_time Require Import Auth_nat Misc Reduction Tactics.
Require Export Translation Simulation. From iris_time Require Export Translation Simulation.
From iris.proofmode Require Import coq_tactics. From iris.proofmode Require Import coq_tactics.
Import uPred. Import uPred.
......
From iris.heap_lang Require Import proofmode notation adequacy. From iris.heap_lang Require Import proofmode notation adequacy.
From iris.base_logic Require Import invariants. From iris.base_logic Require Import invariants.
Require Import Auth_nat Reduction TimeCredits. From iris_time Require Import Auth_nat Reduction TimeCredits.
Implicit Type e : expr. Implicit Type e : expr.
Implicit Type v : val. Implicit Type v : val.
......
From iris.heap_lang Require Import proofmode notation adequacy. From iris.heap_lang Require Import proofmode notation adequacy.
From iris.base_logic Require Import invariants. From iris.base_logic Require Import invariants.
Require Import Auth_nat Auth_mnat Misc Reduction Tactics. From iris_time Require Import Auth_nat Auth_mnat Misc Reduction Tactics.
Require Export Translation Simulation. From iris_time Require Export Translation Simulation.
Implicit Type e : expr. Implicit Type e : expr.
Implicit Type v : val. Implicit Type v : val.
...@@ -103,7 +103,6 @@ Section TockSpec. ...@@ -103,7 +103,6 @@ Section TockSpec.
Lemma TR_weaken (n n : nat) : Lemma TR_weaken (n n : nat) :
(n n)%nat (n n)%nat
TR n - TR n. TR n - TR n.
Require Import Auth_nat.
Proof. apply own_auth_nat_weaken. Qed. Proof. apply own_auth_nat_weaken. Qed.
Lemma TR_timeless n : Lemma TR_timeless n :
...@@ -126,7 +125,6 @@ Section TockSpec. ...@@ -126,7 +125,6 @@ Section TockSpec.
Lemma TRdup_weaken (n n : nat) : Lemma TRdup_weaken (n n : nat) :
(n n)%nat (n n)%nat
TRdup n - TRdup n. TRdup n - TRdup n.
Require Import Auth_mnat.
Proof. apply own_auth_mnat_weaken. Qed. Proof. apply own_auth_mnat_weaken. Qed.
Lemma TRdup_timeless n : Lemma TRdup_timeless n :
......
From iris.heap_lang Require Import notation. From iris.heap_lang Require Import notation.
From stdpp Require Import fin_maps. From stdpp Require Import fin_maps.
Require Import Reduction. From iris_time Require Import Reduction.
Implicit Type e : expr. Implicit Type e : expr.
Implicit Type v : val. Implicit Type v : val.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment