The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
Can't install on Coq 8.8.1
Hi,
I want to try out Iris, but opam install coq-iris yields this this:
#=== ERROR while compiling coq-iris.dev.2019-03-14.3.2d1c8352 ================#
# context 2.0.0~beta5 | linux/x86_64 | coq.8.8.1 | git+https://gitlab.mpi-sws.org/iris/opam.git
# path ~/.opam/coq88/.opam-switch/build/coq-iris.dev.2019-03-14.3.2d1c8352
# command /usr/bin/make -j7
# exit-code 2
# env-file ~/.opam/log/coq-iris-30223-f0f09f.env
# output-file ~/.opam/log/coq-iris-30223-f0f09f.out
### output ###
# [...]
# -Closed under the global context
# +Axioms:
# +iProp_unfold : ∀ Σ : gFunctors, iProp Σ -n> iPreProp Σ
# +iProp_fold_unfold : ∀ (Σ : gFunctors) (P : iProp Σ),
# +iProp_fold (iProp_unfold P) ≡ P
# +iProp_fold : ∀ Σ : gFunctors, iPreProp Σ -n> iProp Σ
# +iPreProp : gFunctors → ofeT
# make[2]: *** [Makefile.coq.local:20: tests/one_shot.vo] Error 1
# make[2]: *** Waiting for unfinished jobs....
# make[1]: *** [Makefile.coq:318: all] Error 2
# make[1]: Leaving directory '/home/maxi/.opam/coq88/.opam-switch/build/coq-iris.dev.2019-03-14.3.2d1c8352'
# make: *** [Makefile:6: all] Error 2However, these definitions like iProp_unfold etc are not axioms (are they?). Is this a known bug of Coq 8.8.1?
I will try out the newest Coq version, but compilation takes some time...