Internal error: [as_in_build_dir_exn] called on something not in build dir

[SkySkimmer]

Expected Behavior

Error that doesn't say "Internal error, please report upstream including the contents of _build/log."

Actual Behavior

+ dune build @check
File "_build_ci/elpi/builtin-doc/dune", line 3, characters 12-23:
3 |  (libraries elpi_plugin))
                ^^^^^^^^^^^
Error: Library "elpi_plugin" not found.
-> required by
   _build/default/_build_ci/elpi/builtin-doc/.gen_doc.eobjs/byte/dune__exe__Gen_doc.cmi
-> required by alias _build_ci/elpi/builtin-doc/check
      ocamlc _build_ci/elpi/etc/tools/.hash.eobjs/byte/dune__exe__Hash.{cmi,cmti}
      ocamlc _build_ci/elpi/etc/tools/.hash.eobjs/byte/dune__exe__Hash.{cmo,cmt}
      ocamlc _build_ci/elpi/etc/.shafile.eobjs/byte/dune__exe__Shafile.{cmi,cmti}
      ocamlc _build_ci/elpi/etc/.optcomp.eobjs/byte/dune__exe__Optcomp.{cmi,cmti}
      ocamlc _build_ci/elpi/etc/.version_parser.eobjs/byte/dune__exe__Version_parser.{cmi,cmti}
      ocamlc _build_ci/elpi/etc/.shafile.eobjs/byte/dune__exe__Shafile.{cmo,cmt}
      ocamlc _build_ci/elpi/etc/.optcomp.eobjs/byte/dune__exe__Optcomp.{cmo,cmt}
Internal error, please report upstream including the contents of _build/log.
Description:
  ("[as_in_build_dir_exn] called on something not in build dir",
   { t =
       External
         "/home/gaetan/.opam/4.14.0/lib/rocq-elpi/elpi/elpi_plugin.cmxs"
   })
Raised at Stdune__Code_error.raise in file
  "otherlibs/stdune/src/code_error.ml", line 10, characters 30-62
Called from
  Dune_rules__Coq_rules.coq_plugins_install_rules.rules_for_lib.(fun) in file
  "src/dune_rules/coq/coq_rules.ml", line 1084, characters 26-62
Called from Stdlib__List.rev_map.rmap_f in file "list.ml", line 103,
  characters 22-25
Called from Stdune__List.map in file "otherlibs/stdune/src/list.ml"
  (inlined), line 5, characters 19-33
Called from Dune_rules__Coq_rules.coq_plugins_install_rules.rules_for_lib in
  file "src/dune_rules/coq/coq_rules.ml", line 1081, characters 6-586
Called from Stdune__List.rev_concat_map.aux in file
  "otherlibs/stdune/src/list.ml", line 54, characters 15-18
Called from Stdune__List.concat_map in file "otherlibs/stdune/src/list.ml"
  (inlined), line 60, characters 26-47
Called from Dune_rules__Coq_rules.coq_plugins_install_rules in file
  "src/dune_rules/coq/coq_rules.ml", line 1094, characters 2-42
Called from Fiber__Core.O.(>>|).(fun) in file "vendor/fiber/src/core.ml",
  line 253, characters 36-41
Called from Fiber__Scheduler.exec in file "vendor/fiber/src/scheduler.ml",
  line 76, characters 8-11
-> required by ("stanzas-to-entries", "default")
-> required by ("symlinked_entries", ("default", "rocqide"))
-> required by ("evaluate-restrict", ())
-> required by ("restrict-by-child-non-default-inner", ())
-> required by ("restrict-by-child-non-default-inner", ())
-> required by ("restrict-by-child-non-default-outer", ())
-> required by ("scheme-union", ())
-> required by ("gen-rules", In_build_dir "install/default")
-> required by ("gen-rules", In_build_dir "install/default/lib")
-> required by ("gen-rules", In_build_dir "install/default/lib/rocq-runtime")
-> required by ("load-dir", In_build_dir "install/default/lib/rocq-runtime")
-> required by
   ("build-file", In_build_dir "install/default/lib/rocq-runtime/META")
-> required by ("deps", ())
-> required by ("Rule.make", ())
-> required by
   ("execute-rule",
    { id = 3983
    ; info =
        From_dune_file
          { pos_fname = "tools/coqdep/lib/dune"
          ; start = { pos_lnum = 8; pos_bol = 150; pos_cnum = 150 }
          ; stop = { pos_lnum = 16; pos_bol = 459; pos_cnum = 486 }
          }
    })
-> required by ("<unnamed>", ())
-> required by
   ("build-file",
    In_build_dir "default/tools/coqdep/lib/static_toplevel_libs.ml")
-> required by ("Rule.make", ())
-> required by ("Rule.set_action", ())
-> required by ("execute-rule", { id = 7970; info = Internal })
-> required by ("<unnamed>", ())
-> required by
   ("build-file",
    In_build_dir
      "default/tools/coqdep/lib/.coqdeplib.objs/byte/coqdeplib__Static_toplevel_libs.cmt")
-> required by
   ("build_file_selector",
    { dir = In_build_dir "default/tools/coqdep/lib/.coqdeplib.objs/byte"
    ; predicate = Glob (Glob "*.{cmt,cmti,cmi}")
    ; only_generated_files = false
    })
-> required by ("<unnamed>", ())
-> required by
   ("build-alias",
    { dir = In_build_dir "default/tools/coqdep/lib"; name = "check" })
-> 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.
Internal error, please report upstream including the contents of _build/log.
Description:
  ("[as_in_build_dir_exn] called on something not in build dir",
   { t =
       External
         "/home/gaetan/.opam/4.14.0/lib/rocq-elpi/coercion/elpi_coercion_plugin.cmxs"
   })
Raised at Stdune__Code_error.raise in file
  "otherlibs/stdune/src/code_error.ml", line 10, characters 30-62
Called from
  Dune_rules__Coq_rules.coq_plugins_install_rules.rules_for_lib.(fun) in file
  "src/dune_rules/coq/coq_rules.ml", line 1084, characters 26-62
Called from Stdlib__List.rev_map.rmap_f in file "list.ml", line 103,
  characters 22-25
Called from Stdune__List.map in file "otherlibs/stdune/src/list.ml"
  (inlined), line 5, characters 19-33
Called from Dune_rules__Coq_rules.coq_plugins_install_rules.rules_for_lib in
  file "src/dune_rules/coq/coq_rules.ml", line 1081, characters 6-586
Called from Stdune__List.rev_concat_map.aux in file
  "otherlibs/stdune/src/list.ml", line 54, characters 15-18
Called from Stdune__List.concat_map in file "otherlibs/stdune/src/list.ml"
  (inlined), line 60, characters 26-47
Called from Dune_rules__Coq_rules.coq_plugins_install_rules in file
  "src/dune_rules/coq/coq_rules.ml", line 1094, characters 2-42
Called from Fiber__Core.O.(>>|).(fun) in file "vendor/fiber/src/core.ml",
  line 253, characters 36-41
Called from Fiber__Scheduler.exec in file "vendor/fiber/src/scheduler.ml",
  line 76, characters 8-11
-> required by ("stanzas-to-entries", "default")
-> required by ("symlinked_entries", ("default", "rocqide"))
-> required by ("evaluate-restrict", ())
-> required by ("restrict-by-child-non-default-inner", ())
-> required by ("restrict-by-child-non-default-inner", ())
-> required by ("restrict-by-child-non-default-outer", ())
-> required by ("scheme-union", ())
-> required by ("gen-rules", In_build_dir "install/default")
-> required by ("gen-rules", In_build_dir "install/default/lib")
-> required by ("gen-rules", In_build_dir "install/default/lib/rocq-runtime")
-> required by ("load-dir", In_build_dir "install/default/lib/rocq-runtime")
-> required by
   ("build-file", In_build_dir "install/default/lib/rocq-runtime/META")
-> required by ("deps", ())
-> required by ("Rule.make", ())
-> required by
   ("execute-rule",
    { id = 3983
    ; info =
        From_dune_file
          { pos_fname = "tools/coqdep/lib/dune"
          ; start = { pos_lnum = 8; pos_bol = 150; pos_cnum = 150 }
          ; stop = { pos_lnum = 16; pos_bol = 459; pos_cnum = 486 }
          }
    })
-> required by ("<unnamed>", ())
-> required by
   ("build-file",
    In_build_dir "default/tools/coqdep/lib/static_toplevel_libs.ml")
-> required by ("Rule.make", ())
-> required by ("Rule.set_action", ())
-> required by ("execute-rule", { id = 7970; info = Internal })
-> required by ("<unnamed>", ())
-> required by
   ("build-file",
    In_build_dir
      "default/tools/coqdep/lib/.coqdeplib.objs/byte/coqdeplib__Static_toplevel_libs.cmt")
-> required by
   ("build_file_selector",
    { dir = In_build_dir "default/tools/coqdep/lib/.coqdeplib.objs/byte"
    ; predicate = Glob (Glob "*.{cmt,cmti,cmi}")
    ; only_generated_files = false
    })
-> required by ("<unnamed>", ())
-> required by
   ("build-alias",
    { dir = In_build_dir "default/tools/coqdep/lib"; name = "check" })
-> required by ("toplevel", ())
Internal error, please report upstream including the contents of _build/log.
Description:
  ("[as_in_build_dir_exn] called on something not in build dir",
   { t =
       External
         "/home/gaetan/.opam/4.14.0/lib/rocq-elpi/cs/elpi_cs_plugin.cmxs"
   })
Raised at Stdune__Code_error.raise in file
  "otherlibs/stdune/src/code_error.ml", line 10, characters 30-62
Called from
  Dune_rules__Coq_rules.coq_plugins_install_rules.rules_for_lib.(fun) in file
  "src/dune_rules/coq/coq_rules.ml", line 1084, characters 26-62
Called from Stdlib__List.rev_map.rmap_f in file "list.ml", line 103,
  characters 22-25
Called from Stdune__List.map in file "otherlibs/stdune/src/list.ml"
  (inlined), line 5, characters 19-33
Called from Dune_rules__Coq_rules.coq_plugins_install_rules.rules_for_lib in
  file "src/dune_rules/coq/coq_rules.ml", line 1081, characters 6-586
Called from Stdune__List.rev_concat_map.aux in file
  "otherlibs/stdune/src/list.ml", line 54, characters 15-18
Called from Stdune__List.concat_map in file "otherlibs/stdune/src/list.ml"
  (inlined), line 60, characters 26-47
Called from Dune_rules__Coq_rules.coq_plugins_install_rules in file
  "src/dune_rules/coq/coq_rules.ml", line 1094, characters 2-42
Called from Fiber__Core.O.(>>|).(fun) in file "vendor/fiber/src/core.ml",
  line 253, characters 36-41
Called from Fiber__Scheduler.exec in file "vendor/fiber/src/scheduler.ml",
  line 76, characters 8-11
-> required by ("stanzas-to-entries", "default")
-> required by ("symlinked_entries", ("default", "rocqide"))
-> required by ("evaluate-restrict", ())
-> required by ("restrict-by-child-non-default-inner", ())
-> required by ("restrict-by-child-non-default-inner", ())
-> required by ("restrict-by-child-non-default-outer", ())
-> required by ("scheme-union", ())
-> required by ("gen-rules", In_build_dir "install/default")
-> required by ("gen-rules", In_build_dir "install/default/lib")
-> required by ("gen-rules", In_build_dir "install/default/lib/rocq-runtime")
-> required by ("load-dir", In_build_dir "install/default/lib/rocq-runtime")
-> required by
   ("build-file", In_build_dir "install/default/lib/rocq-runtime/META")
-> required by ("deps", ())
-> required by ("Rule.make", ())
-> required by
   ("execute-rule",
    { id = 3983
    ; info =
        From_dune_file
          { pos_fname = "tools/coqdep/lib/dune"
          ; start = { pos_lnum = 8; pos_bol = 150; pos_cnum = 150 }
          ; stop = { pos_lnum = 16; pos_bol = 459; pos_cnum = 486 }
          }
    })
-> required by ("<unnamed>", ())
-> required by
   ("build-file",
    In_build_dir "default/tools/coqdep/lib/static_toplevel_libs.ml")
-> required by ("Rule.make", ())
-> required by ("Rule.set_action", ())
-> required by ("execute-rule", { id = 7970; info = Internal })
-> required by ("<unnamed>", ())
-> required by
   ("build-file",
    In_build_dir
      "default/tools/coqdep/lib/.coqdeplib.objs/byte/coqdeplib__Static_toplevel_libs.cmt")
-> required by
   ("build_file_selector",
    { dir = In_build_dir "default/tools/coqdep/lib/.coqdeplib.objs/byte"
    ; predicate = Glob (Glob "*.{cmt,cmti,cmi}")
    ; only_generated_files = false
    })
-> required by ("<unnamed>", ())
-> required by
   ("build-alias",
    { dir = In_build_dir "default/tools/coqdep/lib"; name = "check" })
-> required by ("toplevel", ())
Internal error, please report upstream including the contents of _build/log.
Description:
  ("[as_in_build_dir_exn] called on something not in build dir",
   { t =
       External
         "/home/gaetan/.opam/4.14.0/lib/rocq-elpi/tc/elpi_tc_plugin.cmxs"
   })
Raised at Stdune__Code_error.raise in file
  "otherlibs/stdune/src/code_error.ml", line 10, characters 30-62
Called from
  Dune_rules__Coq_rules.coq_plugins_install_rules.rules_for_lib.(fun) in file
  "src/dune_rules/coq/coq_rules.ml", line 1084, characters 26-62
Called from Stdlib__List.rev_map.rmap_f in file "list.ml", line 103,
  characters 22-25
Called from Stdune__List.map in file "otherlibs/stdune/src/list.ml"
  (inlined), line 5, characters 19-33
Called from Dune_rules__Coq_rules.coq_plugins_install_rules.rules_for_lib in
  file "src/dune_rules/coq/coq_rules.ml", line 1081, characters 6-586
Called from Stdune__List.rev_concat_map.aux in file
  "otherlibs/stdune/src/list.ml", line 54, characters 15-18
Called from Stdune__List.concat_map in file "otherlibs/stdune/src/list.ml"
  (inlined), line 60, characters 26-47
Called from Dune_rules__Coq_rules.coq_plugins_install_rules in file
  "src/dune_rules/coq/coq_rules.ml", line 1094, characters 2-42
Called from Fiber__Core.O.(>>|).(fun) in file "vendor/fiber/src/core.ml",
  line 253, characters 36-41
Called from Fiber__Scheduler.exec in file "vendor/fiber/src/scheduler.ml",
  line 76, characters 8-11
-> required by ("stanzas-to-entries", "default")
-> required by ("symlinked_entries", ("default", "rocqide"))
-> required by ("evaluate-restrict", ())
-> required by ("restrict-by-child-non-default-inner", ())
-> required by ("restrict-by-child-non-default-inner", ())
-> required by ("restrict-by-child-non-default-outer", ())
-> required by ("scheme-union", ())
-> required by ("gen-rules", In_build_dir "install/default")
-> required by ("gen-rules", In_build_dir "install/default/lib")
-> required by ("gen-rules", In_build_dir "install/default/lib/rocq-runtime")
-> required by ("load-dir", In_build_dir "install/default/lib/rocq-runtime")
-> required by
   ("build-file", In_build_dir "install/default/lib/rocq-runtime/META")
-> required by ("deps", ())
-> required by ("Rule.make", ())
-> required by
   ("execute-rule",
    { id = 3983
    ; info =
        From_dune_file
          { pos_fname = "tools/coqdep/lib/dune"
          ; start = { pos_lnum = 8; pos_bol = 150; pos_cnum = 150 }
          ; stop = { pos_lnum = 16; pos_bol = 459; pos_cnum = 486 }
          }
    })
-> required by ("<unnamed>", ())
-> required by
   ("build-file",
    In_build_dir "default/tools/coqdep/lib/static_toplevel_libs.ml")
-> required by ("Rule.make", ())
-> required by ("Rule.set_action", ())
-> required by ("execute-rule", { id = 7970; info = Internal })
-> required by ("<unnamed>", ())
-> required by
   ("build-file",
    In_build_dir
      "default/tools/coqdep/lib/.coqdeplib.objs/byte/coqdeplib__Static_toplevel_libs.cmt")
-> required by
   ("build_file_selector",
    { dir = In_build_dir "default/tools/coqdep/lib/.coqdeplib.objs/byte"
    ; predicate = Glob (Glob "*.{cmt,cmti,cmi}")
    ; only_generated_files = false
    })
-> required by ("<unnamed>", ())
-> required by
   ("build-alias",
    { dir = In_build_dir "default/tools/coqdep/lib"; name = "check" })
-> required by ("toplevel", ())
      ocamlc _build_ci/elpi/etc/.version_parser.eobjs/byte/dune__exe__Version_parser.{cmo,cmt}

_build/log:

# dune build @check
# OCAMLPARAM: unset
# Shared cache: enabled
# Shared cache location: /home/gaetan/.cache/dune/db
# Workspace root: /home/gaetan/dev/coq/coq
# 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_ea1e13_output
# cache store success [072bbb1310d359a8b5dd01f050659500]
# cache store success [57ce74afa0135e840d697d60368696bd]
# cache store success [a35b9e8ee98a22e4dde56eb04e4102e1]
# cache store success [10e690926dcbca2e836a29a79b81f671]
# cache store success [1c30fd6cbce45508448508cec5b510c2]
# cache store success [1a70519d4fa833a0503ab159d2deccfc]
# cache store success [fffbd22834ab7a53e39a66c82cf71e9f]
# cache store success [e9cdc03c4ab13ba5f980937f887cd8ea]
# cache store success [3e337b31ed588223b16d37a163905e19]
$ /home/gaetan/.opam/4.14.0/bin/coqc --config > /tmp/dune_e2fe60_output
# cache store success [80d89bf8dfae72d0a714a10cba246d26]
# cache store success [8fe25561b5e054bc40c25b0fadfa5d68]
# cache store success [2c98f08145c3016e796509a57cf59e1d]
# cache store success [f21558ed52bd08ac524a5fe6bc47e879]
# cache store success [c0846561a7a6080953aed0d7ce6d5e6b]
# cache store success [17ee0c17054b4cc27807ba53ad7a9ee8]
# cache store success [453015c755cb04f3c41473216c0e1a7c]
# cache store success [802fb1091179e53f1cf27e037b8b9099]
# cache store success [7a9f0982fa900e3ecf8beb3c7753807e]
# cache store success [53facbd86cd2258d83b0b71f50d8da8f]
# cache store success [25eb4d6767b17c5371a3a4acbb2a34f7]
# cache store success [05f60ba8206723cb2b2a6ca4401ee9c6]
# cache store success [dcd75c626cbca5c096f24c8221088510]
# cache store success [e95073df0f6ffb5be9fc786e1282b062]
# cache store success [fde089070a8f3a63af06cd64eea4f2c9]
# cache store success [f9fb0bad2955cf1546060d9b24db1005]
# cache store success [db3a2c5d1b269276a60ed7db3bc6f061]
# cache store success [03ea84f7263b9b2346bc628c7ffcb5f7]
# cache store success [1ce754b1b48d308cf04b35bba17e1ccb]
# cache store success [a172e9a313cd6d1378f76cdb9fbf6e29]
# cache store success [37086d3cf6d1061af62c81b94106ae0b]
# cache store success [477ec3cd19228c6e0c617e6678933048]
# cache store success [b5a2d85b270221a6218d16da956ca8e8]
# cache store success [432e67a072a292cef0f33c94e1581fed]
$ (cd _build/default && /home/gaetan/.opam/4.14.0/bin/ocamlc.opt -w @1..3@5..28@31..39@43@46..47@49..57@61..62@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A -g -bin-annot -I _build_ci/elpi/etc/tools/.hash.eobjs/byte -no-alias-deps -opaque -o _build_ci/elpi/etc/tools/.hash.eobjs/byte/dune__exe__Hash.cmi -c -intf _build_ci/elpi/etc/tools/hash.mli)
# cache store success [05fe5d9999cfe6b6c9f8ad45bb9fecd3]
# cache store success [94e8afadfcdc43837f85f078a88f5778]
# cache store success [24ea86e3009975a318fcafc597c12832]
$ (cd _build/default && /home/gaetan/.opam/4.14.0/bin/ocamlc.opt -w @1..3@5..28@31..39@43@46..47@49..57@61..62@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A -g -bin-annot -I _build_ci/elpi/etc/tools/.hash.eobjs/byte -intf-suffix .ml -no-alias-deps -opaque -o _build_ci/elpi/etc/tools/.hash.eobjs/byte/dune__exe__Hash.cmo -c -impl _build_ci/elpi/etc/tools/hash.ml)
# cache store success [98e1e76e96cc10d78c68a1585a45de0f]
# cache store success [f3743849e91638b1d430bf57ad7716a8]
# cache store success [5ed6d0907d429da672ae3ceed59b15a3]
# cache store success [ad2af903fced842a4e80b91ab469205a]
# cache store success [882f084d3b91f85b62ef72ee962c8e52]
# cache store success [f9370c81d81a3ca87dc00960121191fc]
# cache store success [86ad55d214032dae704332c26a02b0a8]
# cache store success [5ffc4c1f7937430dc2cbb9f7c1c3ef67]
# cache store success [0dbde4c9429c1bfbce6855120189fe57]
# cache store success [31d82aef946223b517fbc010b7f843a2]
# cache store success [f4435dcae92242880f508c6cdc2ccb41]
# cache store success [9e70b67af6ba6e14d7d41fb8d60fddb6]
# cache store success [fe8b64eb1a0089f504f03dbfb2f4cd0d]
# cache store success [c6e53bfab63b400dcc96f97d9b814f73]
# cache store success [8d02bf7a246a7c33b356f47550812c93]
# cache store success [3ec2b4123546db18afa8e1f8c9b9a514]
# cache store success [3ce77321728bd4e94502da3b2bb511b4]
# cache store success [2d2a02fd0cab9caa8f91566e8cb1d8ae]
# cache store success [88aa3399b2bae41673055ecf99c64e4c]
# cache store success [a9d46f227e79d46ac2a9b33a571a7964]
# cache store success [1053b40365c47c20017770f2a1b9af7a]
# cache store success [7d2bc0b7088cdce34dbcb297afb8d7ee]
# cache store success [20e5d711502e18fdd70cb3147e503c2b]
# cache store success [0cfa589c5edc07820eda2cec22ce4478]
# cache store success [50a2977b2df3eef3a05d7b50856f7e57]
# cache store success [bba30041ca2e645a6af43b3076280034]
# cache store success [62696a975ffcad6f8cfce532d60d68ed]
# cache store success [c7baaca835ccaee95b845e1d08e12079]
# cache store success [570ee0ff2a25a8e5fe7d8515dba6bc6e]
# cache store success [95c2d3cd28f6e5ed0d16c675589c1b05]
# cache store success [eb466c0a6498529e163be251f9680884]
# cache store success [c171da74955a3f7dfa97a71a48b96ebb]
# cache store success [dd95405723a5bc423c0821b602629bfe]
# cache store success [a82bec078d224ce260e2b9a401c88a44]
# cache store success [ed2092e2ea0201143a97bf6d7a2ba04c]
# cache store success [8db404d0c16e7b6ee2ec06322d34d01d]
# cache store success [ccdf89262d0dd029b6dd73d2b767980f]
# cache store success [7d65ca98ca950092daf346837e3a32e7]
# cache store success [20425894216e8b342af9c3b225262336]
# cache store success [44e9385225d6ce0ebc0e77b79761524a]
# cache store success [ff4a948787ae7072ead2ba0a07020603]
# cache store success [6e38fa2eb743bd09b00be15ac4fc6cee]
# cache store success [9d52dc5a089e5b45ef4c209b37e71929]
# cache store success [a8d01384339c9da525979c05d5edf199]
# cache store success [895b395907bd1ea068982dbd29ccd663]
# cache store success [8e301421bcf221dee933e882f312eb8d]
# cache store success [8ca8985fb207cda5c1e1d90942b9d24b]
# cache store success [fc70818393afcad450ea99a45761219e]
# cache store success [882de76fd73e95ec1675f35c69a63bbf]
# cache store success [3bb3afdc2f85345102cdb1d328dc1242]
# cache store success [2cc4f4fc10350a335ee3d8ae26cb0092]
# cache store success [1eefeeecdf18f9da7e18e850ef05ce28]
# cache store success [42a87a9e302d5e727e51eb68a1f63922]
# cache store success [de9b665d1cdcb5e7252cce157b41d9ce]
# cache store success [26bce62fb388bca65ae6d5d12919fca6]
# cache store success [dfec7acd551418cbd17269496edc2ec8]
# cache store success [179406836e9ab42241767c79f317c88b]
# cache store success [2357879dcbe17088b6fbcdfc65e0968a]
# cache store success [8f52b6425bec534edea3d54a2c0b07f6]
# cache store success [88335501d69f4741afc9654873329152]
# cache store success [4e1a8312583b4fff7d2c7b11e124a95c]
# cache store success [8b4ed6abaf1c5528eded5264e7fefa80]
# cache store success [5a7d2fed8b77e60fad75d8144a276461]
# cache store success [7b45b2eb5a1a571690bb46012b6e0f28]
# cache store success [3ce4984d5f96f8824e19b06252794ebc]
# cache store success [faad85569dac7cbd1275b7b73cf06540]
# cache store success [7d6f4b560f79a863c5dbdac76c53bc47]
# cache store success [0a761062dd1723c0104359141e5ca509]
# cache store success [0e5befd31ebc8711bb2558a8ec14e3cd]
# cache store success [4428957229fda722933f6184450b2a7c]
# cache store success [2b0ecb4adf4f1cd3accb857ea9bcd41d]
# cache store success [5e5f409ff2d62c8c97f87f4483d8339c]
# cache store success [a589872e97d3299e32cf36242ceec0e4]
# cache store success [2737338d9d3f7c7d4515b3351a2a8aee]
# cache store success [74ecac13908cb736b2ab6b3658009335]
$ _build/default/topbin/coqc_bin.exe --config > /tmp/dune_9096c8_output
[1]
# cache store success [1c02adb6460a2d38503b13ee4fc46239]
# cache store success [e42b6a41e2fab9de0e951bf187e25e70]
# cache store success [96300033f23fb0f5220d6116e4f1bf94]
$ (cd _build/default && /home/gaetan/.opam/4.14.0/bin/ocamlc.opt -w @1..3@5..28@31..39@43@46..47@49..57@61..62@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A -g -bin-annot -I _build_ci/elpi/etc/.shafile.eobjs/byte -no-alias-deps -opaque -o _build_ci/elpi/etc/.shafile.eobjs/byte/dune__exe__Shafile.cmi -c -intf _build_ci/elpi/etc/shafile.mli)
# cache store success [20e17d381e174d8fb87894150f1118e1]
$ (cd _build/default && /home/gaetan/.opam/4.14.0/bin/ocamlc.opt -w @1..3@5..28@31..39@43@46..47@49..57@61..62@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A -g -bin-annot -I _build_ci/elpi/etc/.optcomp.eobjs/byte -no-alias-deps -opaque -o _build_ci/elpi/etc/.optcomp.eobjs/byte/dune__exe__Optcomp.cmi -c -intf _build_ci/elpi/etc/optcomp.mli)
# cache store success [3b003e752a60255eb91e6e304f2bb67c]
$ (cd _build/default && /home/gaetan/.opam/4.14.0/bin/ocamlc.opt -w @1..3@5..28@31..39@43@46..47@49..57@61..62@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A -g -bin-annot -I _build_ci/elpi/etc/.version_parser.eobjs/byte -I /home/gaetan/.opam/4.14.0/lib/elpi -I /home/gaetan/.opam/4.14.0/lib/elpi/compiler -I /home/gaetan/.opam/4.14.0/lib/elpi/lexer_config -I /home/gaetan/.opam/4.14.0/lib/elpi/parser -I /home/gaetan/.opam/4.14.0/lib/elpi/runtime -I /home/gaetan/.opam/4.14.0/lib/elpi/trace/runtime -I /home/gaetan/.opam/4.14.0/lib/elpi/util -I /home/gaetan/.opam/4.14.0/lib/menhirLib -I /home/gaetan/.opam/4.14.0/lib/ppx_deriving/runtime -I /home/gaetan/.opam/4.14.0/lib/re -I /home/gaetan/.opam/4.14.0/lib/re/str -I /home/gaetan/.opam/4.14.0/lib/seq -I /home/gaetan/.opam/4.14.0/lib/stdlib-shims -no-alias-deps -opaque -o _build_ci/elpi/etc/.version_parser.eobjs/byte/dune__exe__Version_parser.cmi -c -intf _build_ci/elpi/etc/version_parser.mli)
# cache store success [315b244e3825f5e78254d87474882ae3]
$ (cd _build/default && /home/gaetan/.opam/4.14.0/bin/ocamlc.opt -w @1..3@5..28@31..39@43@46..47@49..57@61..62@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A -g -bin-annot -I _build_ci/elpi/etc/.shafile.eobjs/byte -intf-suffix .ml -no-alias-deps -opaque -o _build_ci/elpi/etc/.shafile.eobjs/byte/dune__exe__Shafile.cmo -c -impl _build_ci/elpi/etc/shafile.ml)
# cache store success [ff3cf097d8275a4c07b00c310639a178]
$ (cd _build/default && /home/gaetan/.opam/4.14.0/bin/ocamlc.opt -w @1..3@5..28@31..39@43@46..47@49..57@61..62@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A -g -bin-annot -I _build_ci/elpi/etc/.optcomp.eobjs/byte -intf-suffix .ml -no-alias-deps -opaque -o _build_ci/elpi/etc/.optcomp.eobjs/byte/dune__exe__Optcomp.cmo -c -impl _build_ci/elpi/etc/optcomp.ml)
# cache store success [58b79393225a2790f565ea4b88a64cf4]
$ (cd _build/default && /home/gaetan/.opam/4.14.0/bin/ocamlc.opt -w @1..3@5..28@31..39@43@46..47@49..57@61..62@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A -g -bin-annot -I _build_ci/elpi/etc/.version_parser.eobjs/byte -I /home/gaetan/.opam/4.14.0/lib/elpi -I /home/gaetan/.opam/4.14.0/lib/elpi/compiler -I /home/gaetan/.opam/4.14.0/lib/elpi/lexer_config -I /home/gaetan/.opam/4.14.0/lib/elpi/parser -I /home/gaetan/.opam/4.14.0/lib/elpi/runtime -I /home/gaetan/.opam/4.14.0/lib/elpi/trace/runtime -I /home/gaetan/.opam/4.14.0/lib/elpi/util -I /home/gaetan/.opam/4.14.0/lib/menhirLib -I /home/gaetan/.opam/4.14.0/lib/ppx_deriving/runtime -I /home/gaetan/.opam/4.14.0/lib/re -I /home/gaetan/.opam/4.14.0/lib/re/str -I /home/gaetan/.opam/4.14.0/lib/seq -I /home/gaetan/.opam/4.14.0/lib/stdlib-shims -intf-suffix .ml -no-alias-deps -opaque -o _build_ci/elpi/etc/.version_parser.eobjs/byte/dune__exe__Version_parser.cmo -c -impl _build_ci/elpi/etc/version_parser.ml)
# cache store success [37ccde06b592044f733bd42d6020910e]

Reproduction

git clone https://github.com/rocq-prover/rocq
cd rocq
git clone https://github.com/LPCIC/coq-elpi/
dune build @check 

Probably also need to have coq-elpi opam installed considering the error message.

Specifications

• dune 3.18.0
• ocaml 4.14.0
• debian linux

Additional information

This is probably linked to coq-elpi having a configure step (which we didn't run to get the error) which generates a dune file, but the missing dune file should only lead to the "elpi_plugin not found" error not an internal error.

[Alizter]

This is an issue in the Coq rules. We are doing:

        (* Safe because all coq libraries are local for now *)
        let plugin_file = Path.as_in_build_dir_exn plugin_file in

That is definitely not safe anymore. cc @ejgallego

[ejgallego]

@Alizter thanks a lot for the debug info, what's the non-local plugin file here tho?

A quick inspection doesn't reveal any out-of-tree file there. Do you have the backtrace?