Incompatible dependency versions
The README lists Ssreflect 1.6.4 and Coq 8.6.1 (among other possible versions) as two dependencies that are required to install Iris. However, with Coq 8.6.1 installed, I am receiving an error message when trying to install Ssreflect 1.6.4 using opam (see below). The error message does not appear if I use Coq 8.7.1.
$ opam pin add coq-mathcomp-ssreflect 1.6.4
[coq-mathcomp-ssreflect] http://github.com/math-comp/math-comp/archive/mathcomp-1.6.4.tar.gz downloaded
coq-mathcomp-ssreflect needs to be installed.
The following actions will be performed:
∗ install coq-mathcomp-ssreflect 1.6.4*
Do you want to continue ? [Y/n] y
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
[ERROR] The compilation of coq-mathcomp-ssreflect failed at "make -C
mathcomp/ssreflect -j 4".
Processing 1/1: [coq-mathcomp-ssreflect: sh]
#=== ERROR while installing coq-mathcomp-ssreflect.1.6.4 ======================#
# opam-version 1.2.2
# os darwin
# command make -C mathcomp/ssreflect -j 4
# path ~/.opam/4.04.2/build/coq-mathcomp-ssreflect.1.6.4
# compiler 4.04.2
# exit-code 2
# env-file ~/.opam/4.04.2/build/coq-mathcomp-ssreflect.1.6.4/coq-mathcomp-ssreflect-9231-e7966f.env
# stdout-file ~/.opam/4.04.2/build/coq-mathcomp-ssreflect.1.6.4/coq-mathcomp-ssreflect-9231-e7966f.out
# stderr-file ~/.opam/4.04.2/build/coq-mathcomp-ssreflect.1.6.4/coq-mathcomp-ssreflect-9231-e7966f.err
### stdout ###
# [...]
# COQDEP binomial.v
# COQDEP bigop.v
# COQDEP ssrnat.v
# COQDEP ssrfun.v
# COQDEP ssreflect.v
# COQDEP ssrbool.v
# COQDEP seq.v
# COQDEP eqtype.v
# COQDEP all_ssreflect.v
# COQC ssreflect.v
### stderr ###
# [...]
# *** Warning: in file ssrfun.v, library Coq.ssrfun is required and has not been found in the loadpath!
# *** Warning: in file ssrfun.v, library Coq.ssrfun is required and has not been found in the loadpath!
# *** Warning: in file ssreflect.v, library Coq.ssreflect is required and has not been found in the loadpath!
# *** Warning: in file ssreflect.v, library Coq.ssreflect is required and has not been found in the loadpath!
# *** Warning: in file ssrbool.v, library Coq.ssrbool is required and has not been found in the loadpath!
# *** Warning: in file ssrbool.v, library Coq.ssrbool is required and has not been found in the loadpath!
# File "./ssreflect.v", line 3, characters 24-33:
# Error: Unable to locate library ssreflect with prefix Coq.
# make[1]: *** [ssreflect.vo] Error 1
# make: *** [all] Error 2
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
The following actions failed
∗ install coq-mathcomp-ssreflect 1.6.4
No changes have been performed