refinedc can fail to build, because instructions allow picking coq.dev
Not sure this is important, but you might want to add an opam pin add coq ...
somewhere.
Spot why this build plan will fail:
$ opam pin add refinedc refinedc
$ opam pin add -n refinedc refinedc
$ opam install refinedc
$ time opam install -j1 -y refinedc
<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><> 🐫
[refinedc.~dev] no changes from git+file:///Users/pgiarrusso/git-bedrock/refinedc-switch/refinedc#master
The following actions will be performed:
∗ install conf-python-2-7 1.1 [required by z3]
∗ install conf-findutils 1 [required by coq]
∗ install conf-m4 1 [required by ocamlfind]
∗ install ocaml-secondary-compiler 4.08.1-1 [required by ocamlfind-secondary]
∗ install camlidl 1.09 [required by apron]
∗ install conf-perl 1 [required by apron]
∗ install ocamlbuild 0.14.0 [required by lem, apron, menhir]
∗ install cmdliner 1.0.4 [required by refinedc]
∗ install conf-gmp 2 [required by z3]
∗ install ocamlfind 1.8.1 [required by coq]
∗ install conf-mpfr 2 [required by mlgmpidl]
∗ install zarith 1.10 [required by coq]
∗ install ocamlfind-secondary 1.8.1 [required by dune]
∗ install num 1.3 [required by coq]
∗ install menhir 20190924 [required by cerberus, toml]
∗ install mlgmpidl 1.2.12 [required by apron]
∗ install dune 2.7.1 [required by refinedc]
∗ install z3 4.8.4 [required by cerberus]
∗ install lem 2020-06-03 [required by cerberus]
∗ install coq dev [required by refinedc]
∗ install apron v0.9.13 [required by cerberus]
∗ install stdlib-shims 0.1.0 [required by earley]
∗ install sha 1.13 [required by cerberus]
∗ install sexplib0 v0.14.0 [required by ppx_sexp_conv, sexplib]
∗ install result 1.5 [required by cerberus]
∗ install ppx_derivers 1.2.1 [required by ppxlib]
∗ install pprint 20200410 [required by cerberus]
∗ install ocaml-migrate-parsetree 2.0.0 [required by ppxlib]
∗ install ocaml-compiler-libs v0.12.3 [required by ppxlib]
∗ install easy-format 1.3.2 [required by yojson]
∗ install cppo 1.6.6 [required by yojson]
∗ install ISO8601 0.2.6 [required by toml]
∗ install coq-stdpp dev.2020-10-01.1.f806b9b0 [required by coq-iris]
∗ install earley 3.0.0 [required by refinedc]
∗ install csexp 1.3.2 [required by dune-configurator]
∗ install ppxlib 0.17.0 [required by ppx_sexp_conv]
∗ install biniou 1.2.1 [required by yojson]
∗ install toml 5.0.0 [required by refinedc]
∗ install coq-iris dev.2020-10-01.3.8f6c063a [required by refinedc]
∗ install dune-configurator 2.7.1 [required by base]
∗ install yojson 1.7.0 [required by cerberus]
∗ install base v0.14.0 [required by ppx_sexp_conv]
∗ install ppx_sexp_conv v0.14.1 [required by cerberus]
∗ install parsexp v0.14.0 [required by sexplib]
∗ install sexplib v0.14.0 [required by cerberus]
∗ install cerberus ~dev* [required by refinedc]
∗ install refinedc ~dev*
[ERROR] The compilation of refinedc failed at "/Users/pgiarrusso/.opam/opam-init/hooks/sandbox.sh build dune build -p refinedc -j 1".
#=== ERROR while compiling refinedc.~dev ======================================#
# context 2.0.7 | macos/x86_64 | ocaml-variants.4.07.1+flambda | pinned(git+file:///Users/pgiarrusso/git-bedrock/refinedc-switch/refinedc#master#ea5c3527)
# path ~/.opam/coq-refinedc/.opam-switch/build/refinedc.~dev
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p refinedc -j 1
# exit-code 1
# env-file ~/.opam/log/refinedc-74790-a5c172.env
# output-file ~/.opam/log/refinedc-74790-a5c172.out
### output ###
# coqc theories/lang/.base.aux,theories/lang/base.{glob,vo} (exit 1)
# (cd _build/default && theories/lang/.bin/coqc -w -notation-overridden -w -redundant-canonical-projection -R theories/lang refinedc.lang theories/lang/base.v)
# File "./theories/lang/base.v", line 382, characters 13-61:
# Error: The LHS of Pos2Z.inj_pow
# (Z.pos (_ ^ _))
# does not match any subterm of the goal
#
# ocamlopt frontend/main.exe
# ld: warning: directory not found for option '-L/opt/local/lib'
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
┌─ The following actions failed
│ λ build refinedc ~dev
└─
┌─ The following changes have been performed
│ ∗ install apron v0.9.13
│ ∗ install base v0.14.0
│ ∗ install biniou 1.2.1
│ ∗ install camlidl 1.09
│ ∗ install cerberus ~dev
│ ∗ install cmdliner 1.0.4
│ ∗ install conf-findutils 1
│ ∗ install conf-gmp 2
│ ∗ install conf-m4 1
│ ∗ install conf-mpfr 2
│ ∗ install conf-perl 1
│ ∗ install conf-python-2-7 1.1
│ ∗ install coq dev
│ ∗ install coq-iris dev.2020-10-01.3.8f6c063a
│ ∗ install coq-stdpp dev.2020-10-01.1.f806b9b0
│ ∗ install cppo 1.6.6
│ ∗ install csexp 1.3.2
│ ∗ install dune 2.7.1
│ ∗ install dune-configurator 2.7.1
│ ∗ install earley 3.0.0
│ ∗ install easy-format 1.3.2
│ ∗ install ISO8601 0.2.6
│ ∗ install lem 2020-06-03
│ ∗ install menhir 20190924
│ ∗ install mlgmpidl 1.2.12
│ ∗ install num 1.3
│ ∗ install ocaml-compiler-libs v0.12.3
│ ∗ install ocaml-migrate-parsetree 2.0.0
│ ∗ install ocaml-secondary-compiler 4.08.1-1
│ ∗ install ocamlbuild 0.14.0
│ ∗ install ocamlfind 1.8.1
│ ∗ install ocamlfind-secondary 1.8.1
│ ∗ install parsexp v0.14.0
│ ∗ install pprint 20200410
│ ∗ install ppx_derivers 1.2.1
│ ∗ install ppx_sexp_conv v0.14.1
│ ∗ install ppxlib 0.17.0
│ ∗ install result 1.5
│ ∗ install sexplib v0.14.0
│ ∗ install sexplib0 v0.14.0
│ ∗ install sha 1.13
│ ∗ install stdlib-shims 0.1.0
│ ∗ install toml 5.0.0
│ ∗ install yojson 1.7.0
│ ∗ install z3 4.8.4
│ ∗ install zarith 1.10
└─
The former state can be restored with:
opam switch import "/Users/pgiarrusso/.opam/coq-refinedc/.opam-switch/backup/state-20201020125946.export"
real 52m33.706s
user 43m42.869s
sys 7m53.975s
Edited by Paolo G. Giarrusso