Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
SkySkimmer opened this issue Apr 8, 2025 · 2 comments
Open

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

SkySkimmer opened this issue Apr 8, 2025 · 2 comments
Labels
coq

Comments

@SkySkimmer
Copy link

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 @[email protected]@31..39@[email protected]@[email protected]@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 @[email protected]@31..39@[email protected]@[email protected]@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 @[email protected]@31..39@[email protected]@[email protected]@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 @[email protected]@31..39@[email protected]@[email protected]@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 @[email protected]@31..39@[email protected]@[email protected]@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 @[email protected]@31..39@[email protected]@[email protected]@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 @[email protected]@31..39@[email protected]@[email protected]@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 @[email protected]@31..39@[email protected]@[email protected]@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 Alizter added the coq label Apr 18, 2025
@Alizter
Copy link
Collaborator

Alizter commented Apr 18, 2025

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
Copy link
Collaborator

@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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
coq
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@SkySkimmer @ejgallego @Alizter