Skip to content
Snippets Groups Projects
Commit b85a3cfc authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ci/ralf/ref' into 'master' 

Coq-version-specific ref files

See merge request FP/iris-coq!202
parents 15e4ed53 28f23802
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Makefile.coq.local
+ 10
− 7
View file @ b85a3cfc
...@@ -8,7 +8,8 @@ test: $(TESTFILES:.v=.vo) ...@@ -8,7 +8,8 @@ test: $(TESTFILES:.v=.vo)
.PHONY: test .PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
COQ_BROKEN=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(9|10)\b" > /dev/null && echo 1) COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" > /dev/null && echo 1)
COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+' -o)
# Can't use pipes because that discards error codes and dash provides no way to control that. # Can't use pipes because that discards error codes and dash provides no way to control that.
# Also egrep errors if it doesn't match anything, we have to ignore that. # Also egrep errors if it doesn't match anything, we have to ignore that.
...@@ -21,17 +22,19 @@ tests/.coqdeps.d: $(TESTFILES) ...@@ -21,17 +22,19 @@ tests/.coqdeps.d: $(TESTFILES)
-include tests/.coqdeps.d -include tests/.coqdeps.d
$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
$(SHOW)$(if $(MAKE_REF),COQTEST [ref],$(if $(COQ_BROKEN),COQTEST [ignored],COQTEST)) $<
$(HIDE)TEST="$$(basename -s .v $<)" && \ $(HIDE)TEST="$$(basename -s .v $<)" && \
if test -f "tests/$$TEST.$(COQ_MINOR_VERSION).ref"; then \
REF="tests/$$TEST.$(COQ_MINOR_VERSION).ref"; \
else \
REF="tests/$$TEST.ref"; \
fi && \
echo $(if $(MAKE_REF),"COQTEST [ref] `basename "$$REF"`","COQTEST$(if $(COQ_OLD), [ignored],) `basename "$$REF"`") && \
TMPFILE="$$(mktemp)" && \ TMPFILE="$$(mktemp)" && \
$(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \ $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \ ($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
$(if $(MAKE_REF), \ $(if $(MAKE_REF), \
mv "$$TMPFILE.filtered" "tests/$$TEST.ref", \ mv "$$TMPFILE.filtered" "$$REF", \
$(if $(COQ_BROKEN), \ $(if $(COQ_OLD),true,diff -u "$$REF" "$$TMPFILE.filtered") \
true, \
diff -u "tests/$$TEST.ref" "$$TMPFILE.filtered" \
) \
) && \ ) && \
rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \ rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \
touch $@ touch $@
README.md
+ 4
− 0
View file @ b85a3cfc
...@@ -134,3 +134,7 @@ This is used to make sure the proof mode prints goals and reduces terms the way ...@@ -134,3 +134,7 @@ This is used to make sure the proof mode prints goals and reduces terms the way
we expect it to. You can run `MAKE_REF=1 make` to re-generate all the `.ref` files; we expect it to. You can run `MAKE_REF=1 make` to re-generate all the `.ref` files;
this is useful after adding or removing `Show.` from a test. If you do this, this is useful after adding or removing `Show.` from a test. If you do this,
make sure to check the diff for any unexpected changes in the output! make sure to check the diff for any unexpected changes in the output!
Some test cases have per-Coq-version `.ref` files (e.g., `atomic.8.8.ref` is a
Coq-8.8-specific `.ref` file). If you change one of these, remember to update
*all* the `.ref` files.
tests/atomic.8.8.ref 0 → 100644
+ 371
− 0
View file @ b85a3cfc
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
============================
<<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
_ : AACC << ∀ x : val, P x
ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
_ : AACC << ∀ x : val, l ↦ x
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅
<< l ↦ x, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
<< l ↦ x, COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> >>
@ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
"Now come the long pre/post tests"
: string
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
@ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
_ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< ∃ yyyy : val, l ↦ yyyy
∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
<<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< l ↦ x, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< l ↦ x, COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
x : val
============================
<<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
x : val
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
x : val
============================
<<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< l ↦ #(), RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
x : val
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
<< l ↦ #(), COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
xx, yyyy : val
============================
<<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< l ↦ yyyy, RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
xx, yyyy : val
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
@ ⊤, ∅ << l ↦ yyyy, COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
xx, yyyy : val
============================
<<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
xx, yyyy : val
Q : iPropI Σ
Φ : language.val heap_lang → iProp Σ
============================
_ : Q
"AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
COMM Q -∗ Φ #() >>
--------------------------------------∗
WP code {{ v, Φ v }}
"Prettification"
: string
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
============================
--------------------------------------∗
∀ Φ : language.val heap_lang → iProp Σ, AU << ∀
x : val,
P x >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>
-∗ WP ! #0 {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
============================
"AU" : ∃ x : val, P x
∗ (P x
={∅,⊤}=∗ AU << ∀ x0 : val,
P x0 >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>)
∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
--------------------------------------∗
WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
tests/atomic.ref
+ 9
− 11
View file @ b85a3cfc
...@@ -347,11 +347,9 @@ ...@@ -347,11 +347,9 @@
P : val → iProp Σ P : val → iProp Σ
============================ ============================
--------------------------------------∗ --------------------------------------∗
∀ Φ : language.val heap_lang → iProp Σ, AU << ∀ ∀ Φ : language.val heap_lang → iProp Σ,
x : val, AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
P x >> @ ⊤, ∅ -∗ WP ! #0 {{ v, Φ v }}
<< ∃ y : val, P y, COMM Φ #() >>
-∗ WP ! #0 {{ v, Φ v }}
1 subgoal 1 subgoal
...@@ -360,12 +358,12 @@ ...@@ -360,12 +358,12 @@
P : val → iProp Σ P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ Φ : language.val heap_lang → iProp Σ
============================ ============================
"AU" : ∃ x : val, P x "AU" : ∃ x : val,
∗ (P x P x
={∅,⊤}=∗ AU << ∀ x0 : val, ∗ (P x
P x0 >> @ ⊤, ∅ ={∅,⊤}=∗ AU << ∀ x0 : val, P x0 >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>) << ∃ y : val, P y, COMM Φ #() >>)
∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #()) ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
--------------------------------------∗ --------------------------------------∗
WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }} WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
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