GitLab

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 2

However, 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...