Refinedc install: make under opam can't find dune

Using Coq
1

Here are the install instructions for refinedc

opam repo add coq-released "https://coq.inria.fr/opam/released"
opam repo add iris-dev "https://gitlab.mpi-sws.org/iris/opam.git"
opam update
opam pin add -n -y cerberus-lib "git+https://github.com/rems-project/cerberus.git#57c0e80af140651aad72e3514133229425aeb102"
opam pin add -n -y cerberus "git+https://github.com/rems-project/cerberus.git#57c0e80af140651aad72e3514133229425aeb102"

My distro

╰─>$ uname -a
Linux rise 6.11.11 #1-NixOS SMP PREEMPT_DYNAMIC Thu Dec  5 12:54:34 UTC 2024 x86_64 GNU/Linux

…
The install error:

[ERROR] The compilation of cerberus-lib.dev failed at "make prelude-src".

#=== ERROR while compiling cerberus-lib.dev ===================================#
# context     2.2.0 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.14.0+options | pinned(git+https://github.com/rems-project/cerberus.git#57c0e80af140651aad72e3514133229425aeb102#57c0e80af140651aad72e3514133229425aeb102)
# path        ~/.opam/refinedc-projects/.opam-switch/build/cerberus-lib.dev
# command     ~/.opam/opam-init/hooks/sandbox.sh build make prelude-src
# exit-code   2
# env-file    ~/.opam/log/cerberus-lib-308838-241618.env
# output-file ~/.opam/log/cerberus-lib-308838-241618.out
### output ###
# Makefile:3: *** "Compilation requires [dune].".  Stop.
...

Proof that I have dune installed

╰─>$ which dune
/home/qd/.opam/refinedc-projects/bin/dune

I also have it globally/nonephemerally installed.

The offending lines of the cerberus makefile (the start of the file):

# Checking for required tools.
ifeq (,$(shell which dune 2> /dev/null))
$(error "Compilation requires [dune].")
endif
ifeq (,$(shell which lem 2> /dev/null))
$(error "Compilation requires [lem].")
endif

Things I’ve tried:

  • OPAM_SANDBOX_DISABLE=1
  • triple checking that ~/.opam/refinedc-projects/bin is added to $PATH
  • manually patching the Makefile (gets overwritten when opam re-clones)
  • opam option depext=false

opam version:

╰─>$ which opam
/nix/store/ai2hbbjx1br1c0bbcnbkjpnfc2akangd-opam-2.2.0/bin/opam

Has anyone run into anything similar?

I notice that the # command is still running ~/.opam/opam-init/hooks/sandbox.sh ... even though i’m passing in OPAM_SANDBOX_DISABLE=1, which could be the problem. What is the flag that disables sandbox?

2

Thanks Gaetan Gilbert in Zulip, I found that it wasn’t a problem of finding dune, but of finding which. I submitted a patch to cerberus, and fixed the build by pointing to my fork.