Internal error with (env (_ (binaries (../tools/myrock.exe as coqc))))

[SkySkimmer]

Expected Behavior

It calls myrock.exe instead of coqc from PATH

Actual Behavior

Internal error, please report upstream including the contents of _build/log.
Description:
  ("internal dependency cycle",
   { frames =
       [ ("<unnamed>", ())
       ; ("load-dir", In_build_dir "default/theories/.bin")
       ; ("build-file", In_build_dir "default/theories/.bin/coqc")
       ; ("coq-config", In_build_dir "default/theories/.bin/coqc")
       ; ("<unnamed>", ())
       ]
   })
Raised at Memo.Exec.exec_dep_node.(fun) in file "src/memo/memo.ml", line
  1289, characters 29-62
Called from Fiber__Scheduler.exec in file "vendor/fiber/src/scheduler.ml",
  line 76, characters 8-11
-> required by ("load-dir", In_build_dir "default/theories")
-> required by ("<unnamed>", ())
-> required by
   ("build-alias", { dir = In_build_dir "default"; name = "default" })
-> required by ("toplevel", ())

I must not crash.  Uncertainty is the mind-killer. Exceptions are the
little-death that brings total obliteration.  I will fully express my cases.
Execution will pass over me and through me.  And when it has gone past, I
will unwind the stack along its path.  Where the cases are handled there will
be nothing.  Only I will remain.
      ocamlc tools/.myrock.eobjs/byte/dune__exe__Myrock.{cmi,cmti}
    ocamlopt tools/.myrock.eobjs/native/dune__exe__Myrock.{cmx,o}
    ocamlopt tools/myrock.exe

_build/log contents:

# dune build
# OCAMLPARAM: unset
# Shared cache: enabled-except-user-rules
# Shared cache location: /home/gaetan/.cache/dune/db
# Workspace root: /tmp/wk
# Auto-detected concurrency: 20
# Dune context:
#  { name = "default"
#  ; kind = "default"
#  ; profile = Dev
#  ; merlin = true
#  ; fdo_target_exe = None
#  ; build_dir = In_build_dir "default"
#  ; instrument_with = []
#  }
$ /home/gaetan/.opam/4.14.0/bin/ocamlc.opt -config > /tmp/dune_582350_output
$ /home/gaetan/.opam/4.14.0/bin/coqc --config > /tmp/dune_317102_output
$ (cd _build/default && /home/gaetan/.opam/4.14.0/bin/ocamlc.opt -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I tools/.myrock.eobjs/byte -no-alias-deps -opaque -o tools/.myrock.eobjs/byte/dune__exe__Myrock.cmi -c -intf tools/myrock.mli)
$ (cd _build/default && /home/gaetan/.opam/4.14.0/bin/ocamlopt.opt -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -I tools/.myrock.eobjs/byte -I tools/.myrock.eobjs/native -intf-suffix .ml -no-alias-deps -opaque -o tools/.myrock.eobjs/native/dune__exe__Myrock.cmx -c -impl tools/myrock.ml)
$ (cd _build/default && /home/gaetan/.opam/4.14.0/bin/ocamlopt.opt -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -o tools/myrock.exe tools/.myrock.eobjs/native/dune__exe__Myrock.cmx)

(note that it calls /home/gaetan/.opam/4.14.0/bin/coqc --config instead of `myrock.exe --config)

Reproduction

Call dune build inside wk.zip

Specifications

• Version of dune (output of dune --version): 3.17.0
• Version of ocaml (output of ocamlc --version): 4.14.0
• Operating system (distribution and version): debian testing (linux)

[ejgallego]

@maiste I'm not sure this is a Coq bug, it seems to me this is more a problem of how (env ...) and binary resolution is implemented. It should be possible to duplicate this in a Coq-free setup.

@SkySkimmer , can you extract the corresponding dune files from the .zip and insert them in the issue?

[SkySkimmer]

theories/dune

(include_subdirs qualified)
(coq.theory
 (name Foo)
 (package foo))

(env
 (_
  (binaries
    (../tools/myrock.exe as coqc))))

tools/dune

(executable (name myrock))

(myrock in the zip is just a noop so it should fail when dune tries to use it as coqc, but that should be a different failure than what we get)

[SkySkimmer]

As mentioned in https://coq.zulipchat.com/#narrow/channel/237656-Coq-devs-.26-plugin-devs/topic/stdlib.20and.20rocq/near/487332513, if the (env) is in the root dir instead of theories/ the error does not happen.
However I still see $ /home/gaetan/.opam/4.14.0/bin/coqc --config in _build/log so coqc is not completely replaced.