Skip to content

`opam` file should specify minimum required Iris version

I got the following failure, I guess the needed fix is requiring coq-iris.dev.2020-04-07.0.86b62616.

$ opam install coq-iris-string-ident
The following actions will be performed:
  ∗ install coq-iris-string-ident dev

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
[coq-iris-string-ident.dev] synchronised from git+https://gitlab.mpi-sws.org/iris/string-ident#v8.11

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
[ERROR] The compilation of coq-iris-string-ident failed at "/Users/pgiarrusso/.opam/opam-init/hooks/sandbox.sh build make -j4".

#=== ERROR while compiling coq-iris-string-ident.dev ==========================#
# context     2.0.6 | macos/x86_64 | ocaml-variants.4.07.1+flambda | git+https://gitlab.mpi-sws.org/iris/opam.git
# path        ~/.opam/ocaml-4.07-coq-8.11.1-flambda/.opam-switch/build/coq-iris-string-ident.dev
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j4
# exit-code   2
# env-file    ~/.opam/log/coq-iris-string-ident-71460-865888.env
# output-file ~/.opam/log/coq-iris-string-ident-71460-865888.out
### output ###
# "coq_makefile" -f _CoqProject -o Makefile.coq
# COQDEP VFILES
# COQC theories/ltac2_string_ident.v
# File "./theories/ltac2_string_ident.v", line 114, characters 5-38:
# Error: There is no Ltac named ltac_tactics.string_to_ident_hook.
#
# Command exited with non-zero status 1
# theories/ltac2_string_ident (real: 2.43, user: 1.64, sys: 0.40, mem: 502788 ko)
# make[2]: *** [theories/ltac2_string_ident.vo] Error 1
# make[1]: *** [all] Error 2
# make: *** [all] Error 2



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
┌─ The following actions failed
│ λ build coq-iris-string-ident dev
└─
╶─ No changes have been performed