coq fails to build #248
Description
The build error occurs while running sandmark on navajo with 4.12.0+domains+effects variant. But this doesn't seem to be limited to navajo because I got a similar error on my personal laptop
The following error log is from navajo.
[ERROR] The compilation of coq failed at "/local/scratch/shubham/sandmark/_opam/opam-init/hooks/sandbox.sh build dune build -p coq -j 127".
#=== ERROR while compiling coq.dev ============================================#
# context 2.0.7 | linux/x86_64 | ocaml-base-compiler.4.12.0+domains+effects | file:///local/scratch/shubham/sandmark/dependencies
# path /local/scratch/shubham/sandmark/_opam/4.12.0+domains+effects/.opam-switch/build/coq.dev
# command /local/scratch/shubham/sandmark/_opam/opam-init/hooks/sandbox.sh build dune build -p coq -j 127
# exit-code 137
# env-file /local/scratch/shubham/sandmark/_opam/log/coq-2821127-2ffe40.env
# output-file /local/scratch/shubham/sandmark/_opam/log/coq-2821127-2ffe40.out
### output ###
# 265 | let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps =
# [...]
# Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased.
# ocamlopt stm/.stm.objs/native/stm.{cmx,o}
# File "stm/stm.ml", line 1759, characters 24-27:
# 1759 | let build_proof ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname =
# ^^^
# Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased.
# ocamlopt plugins/ssr/.ssreflect_plugin.objs/native/ssreflect_plugin__Ssrview.{cmx,o}
# File "plugins/ssr/ssrview.ml", line 396, characters 30-47:
# 396 | let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion =
# ^^^^^^^^^^^^^^^^^
# Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased.
Steps to recreate the error:
- Clone the sandmark repo
git clone https://github.com/ocaml-bench/sandmark.git
- Download the gist that has the coq benchmarks only (
run_config.jsonpresent locally can also be used, it might take a lot of time and the other benchmarks are not important for this issue)
wget https://gist.githubusercontent.com/shubhamkumar13/ba9dc421a745d0d5f57d10409bf6e5a4/raw/c39ccf43cec129907f0f5adcc2422b4ef3fe6eaa/run_config.json coq_run_config.json -O coq_run_config.json
- Run the following commands to start running the benchmark (if using
run_config.jsoninstead of the custom .json file interchange thecoq_run_config_filtered.jsonwithrun_config.json)
TAG='"macro_bench"' make coq_run_config_filtered.json \
RUN_CONFIG_JSON=coq_run_config_filtered.json make ocaml-versions/4.12.0+domains+effects.bench