search

ocaml / dune

A composable build system for OCaml.
https://dune.build/
MIT License
1.63k stars 401 forks source link

Can't find Coq plugin cmxs on loadpath error #7893

Closed palmskog closed 1 year ago

palmskog commented 1 year ago

Expected Behavior

When I create a dune-project and dune file for a Coq project with Dune 3.8 and depend on a Coq plugin installed via coq_makefile like Equations, it should suffice to add (theories Equations) into (coq.theory ...) to enable compilation of the project.

Actual Behavior

When I run dune build, I get the following error:

Error: Can't find file equations_plugin.cmxs on loadpath.

Reproduction

  1. Create a dune-project file like the following: 
    (lang dune 3.8)
(using coq 0.8)
(name TestEquations)
  2. Create a dune file like the following: 
    (coq.theory
(name TestEquations)
(synopsis "Test Equations")
(theories Equations)
;(plugins coq-equations)
)
  3. Create Eqn.v or other .v file like the following: 
    From Equations Require Import Equations.
  4. Run dune build, get the following error: 
    File "./Eqn.v", line 1, characters 0-40:
Error: Can't find file equations_plugin.cmxs on loadpath.

Note that the error disappears if ;(plugins coq-equations) in dune is uncommented.

Specifications

Additional information

This bug report was submitted at the suggestion of @ejgallego.

ejgallego commented 1 year ago

Thanks a lot for the reproduction instructions @palmskog , for the sake to be sure what the problem is, can you confirm that the user-contrib/Equations directory has the equations_plugins.cmxs file on it?

Can you also post the contents of the _build/log file, after a dune clean && dune build --cache=disabled ?

palmskog commented 1 year ago

For the first confirmation:

$ ls ~/.opam/4.14.1+flambda+coq.8.16/lib/coq/user-contrib/Equations/
CoreTactics.glob  CoreTactics.v  CoreTactics.vo  equations_plugin.cmxs  Init.glob  Init.v Init.vo  Prop  Signature.glob  Signature.v  Signature.vo  Type

For the contents of _build/log after a dune clean && dune build --cache=disabled for the successful run with (plugins coq-equations):

# dune build --cache=disabled
# OCAMLPARAM: unset
# Shared cache: disabled
# Workspace root: /home/palmskog/src/rv/vlsm-eqn
# Auto-detected concurrency: 32
$ /home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/ocamlc.opt -config > /tmp/dune_9bfbe0_output
# Dune context:
#  { name = "default"
#  ; kind = "default"
#  ; profile = Dev
#  ; merlin = true
#  ; for_host = None
#  ; fdo_target_exe = None
#  ; build_dir = In_build_dir "default"
#  ; ocaml_bin = External "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin"
#  ; ocaml =
#      Ok External "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/ocaml"
#  ; ocamlc =
#      External "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/ocamlc.opt"
#  ; ocamlopt =
#      Ok
#        External
#          "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/ocamlopt.opt"
#  ; ocamldep =
#      Ok
#        External
#          "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/ocamldep.opt"
#  ; ocamlmklib =
#      Ok
#        External
#          "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/ocamlmklib.opt"
#  ; env =
#      map
#        { "DUNE_OCAML_HARDCODED" :
#            "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib"
#        ; "DUNE_OCAML_STDLIB" :
#            "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/ocaml"
#        ; "DUNE_SOURCEROOT" : "/home/palmskog/src/rv/vlsm-eqn"
#        ; "INSIDE_DUNE" : "/home/palmskog/src/rv/vlsm-eqn/_build/default"
#        ; "OCAMLFIND_IGNORE_DUPS_IN" :
#            "/home/palmskog/src/rv/vlsm-eqn/_build/install/default/lib"
#        ; "OCAMLPATH" :
#            "/home/palmskog/src/rv/vlsm-eqn/_build/install/default/lib"
#        ; "OCAMLTOP_INCLUDE_PATH" :
#            "/home/palmskog/src/rv/vlsm-eqn/_build/install/default/lib/toplevel"
#        ; "OCAML_COLOR" : "always"
#        ; "OPAMCOLOR" : "always"
#        }
#  ; findlib_paths =
#      [ External "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib" ]
#  ; natdynlink_supported = true
#  ; supports_shared_libraries = true
#  ; ocaml_config =
#      { version = "4.14.1"
#      ; standard_library_default =
#          "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/ocaml"
#      ; standard_library =
#          "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/ocaml"
#      ; standard_runtime = "the_standard_runtime_variable_was_deleted"
#      ; ccomp_type = "cc"
#      ; c_compiler = "gcc"
#      ; ocamlc_cflags =
#          [ "-O2"; "-fno-strict-aliasing"; "-fwrapv"; "-pthread"; "-fPIC" ]
#      ; ocamlc_cppflags = [ "-D_FILE_OFFSET_BITS=64" ]
#      ; ocamlopt_cflags =
#          [ "-O2"; "-fno-strict-aliasing"; "-fwrapv"; "-pthread"; "-fPIC" ]
#      ; ocamlopt_cppflags = [ "-D_FILE_OFFSET_BITS=64" ]
#      ; bytecomp_c_compiler =
#          [ "gcc"
#          ; "-O2"
#          ; "-fno-strict-aliasing"
#          ; "-fwrapv"
#          ; "-pthread"
#          ; "-fPIC"
#          ; "-D_FILE_OFFSET_BITS=64"
#          ]
#      ; bytecomp_c_libraries = [ "-lm"; "-lpthread" ]
#      ; native_c_compiler =
#          [ "gcc"
#          ; "-O2"
#          ; "-fno-strict-aliasing"
#          ; "-fwrapv"
#          ; "-pthread"
#          ; "-fPIC"
#          ; "-D_FILE_OFFSET_BITS=64"
#          ]
#      ; native_c_libraries = [ "-lm" ]
#      ; native_pack_linker = [ "ld"; "-r"; "-o" ]
#      ; cc_profile = []
#      ; architecture = "amd64"
#      ; model = "default"
#      ; int_size = 63
#      ; word_size = 64
#      ; system = "linux"
#      ; asm = [ "as" ]
#      ; asm_cfi_supported = true
#      ; with_frame_pointers = false
#      ; ext_exe = ""
#      ; ext_obj = ".o"
#      ; ext_asm = ".s"
#      ; ext_lib = ".a"
#      ; ext_dll = ".so"
#      ; os_type = "Unix"
#      ; default_executable_name = "a.out"
#      ; systhread_supported = true
#      ; host = "x86_64-pc-linux-gnu"
#      ; target = "x86_64-pc-linux-gnu"
#      ; profiling = false
#      ; flambda = true
#      ; spacetime = false
#      ; safe_string = true
#      ; exec_magic_number = "Caml1999X031"
#      ; cmi_magic_number = "Caml1999I031"
#      ; cmo_magic_number = "Caml1999O031"
#      ; cma_magic_number = "Caml1999A031"
#      ; cmx_magic_number = "Caml1999y031"
#      ; cmxa_magic_number = "Caml1999z031"
#      ; ast_impl_magic_number = "Caml1999M031"
#      ; ast_intf_magic_number = "Caml1999N031"
#      ; cmxs_magic_number = "Caml1999D031"
#      ; cmt_magic_number = "Caml1999T031"
#      ; natdynlink_supported = true
#      ; supports_shared_libraries = true
#      ; windows_unicode = false
#      }
#  }
$ /home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/coqc --config > /tmp/dune_c16a1d_output
$ /home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/coqc --print-version > /tmp/dune_64915f_output
$ (cd _build/default && /home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/coqdep -boot -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq-equations -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/btauto -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/cc -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/derive -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/extraction -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/firstorder -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/funind -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ltac -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ltac2 -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/micromega -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/nsatz -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/number_string_notation -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ring -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/rtauto -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ssreflect -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ssrmatching -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/tauto -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/tutorial -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/zify -R /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/theories Coq -Q /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/user-contrib/Equations Equations -R . TestEquations -dyndep opt -vos Eqn.v) > _build/default/.TestEquations.theory.d
$ (cd _build/default && /home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq-equations -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/btauto -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/cc -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/derive -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/extraction -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/firstorder -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/funind -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ltac -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ltac2 -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/micromega -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/nsatz -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/number_string_notation -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ring -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/rtauto -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ssreflect -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ssrmatching -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/tauto -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/tutorial -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/zify -R /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/theories Coq -Q /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/user-contrib/Equations Equations -R . TestEquations Eqn.v)
ejgallego commented 1 year ago

Thanks @palmskog , that's the succesful run with the (plugin ...) thing added, isn't it?

[I correctly see -I $ocaml_lib/lib/coq-equations in the command line]

palmskog commented 1 year ago

@ejgallego you're right, my mistake, here is the erroring log with ;(plugins coq-equations):

# dune build --cache=disabled
# OCAMLPARAM: unset
# Shared cache: disabled
# Workspace root: /home/palmskog/src/rv/vlsm-eqn
# Auto-detected concurrency: 32
$ /home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/ocamlc.opt -config > /tmp/dune_42964b_output
# Dune context:
#  { name = "default"
#  ; kind = "default"
#  ; profile = Dev
#  ; merlin = true
#  ; for_host = None
#  ; fdo_target_exe = None
#  ; build_dir = In_build_dir "default"
#  ; ocaml_bin = External "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin"
#  ; ocaml =
#      Ok External "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/ocaml"
#  ; ocamlc =
#      External "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/ocamlc.opt"
#  ; ocamlopt =
#      Ok
#        External
#          "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/ocamlopt.opt"
#  ; ocamldep =
#      Ok
#        External
#          "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/ocamldep.opt"
#  ; ocamlmklib =
#      Ok
#        External
#          "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/ocamlmklib.opt"
#  ; env =
#      map
#        { "DUNE_OCAML_HARDCODED" :
#            "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib"
#        ; "DUNE_OCAML_STDLIB" :
#            "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/ocaml"
#        ; "DUNE_SOURCEROOT" : "/home/palmskog/src/rv/vlsm-eqn"
#        ; "INSIDE_DUNE" : "/home/palmskog/src/rv/vlsm-eqn/_build/default"
#        ; "OCAMLFIND_IGNORE_DUPS_IN" :
#            "/home/palmskog/src/rv/vlsm-eqn/_build/install/default/lib"
#        ; "OCAMLPATH" :
#            "/home/palmskog/src/rv/vlsm-eqn/_build/install/default/lib"
#        ; "OCAMLTOP_INCLUDE_PATH" :
#            "/home/palmskog/src/rv/vlsm-eqn/_build/install/default/lib/toplevel"
#        ; "OCAML_COLOR" : "always"
#        ; "OPAMCOLOR" : "always"
#        }
#  ; findlib_paths =
#      [ External "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib" ]
#  ; natdynlink_supported = true
#  ; supports_shared_libraries = true
#  ; ocaml_config =
#      { version = "4.14.1"
#      ; standard_library_default =
#          "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/ocaml"
#      ; standard_library =
#          "/home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/ocaml"
#      ; standard_runtime = "the_standard_runtime_variable_was_deleted"
#      ; ccomp_type = "cc"
#      ; c_compiler = "gcc"
#      ; ocamlc_cflags =
#          [ "-O2"; "-fno-strict-aliasing"; "-fwrapv"; "-pthread"; "-fPIC" ]
#      ; ocamlc_cppflags = [ "-D_FILE_OFFSET_BITS=64" ]
#      ; ocamlopt_cflags =
#          [ "-O2"; "-fno-strict-aliasing"; "-fwrapv"; "-pthread"; "-fPIC" ]
#      ; ocamlopt_cppflags = [ "-D_FILE_OFFSET_BITS=64" ]
#      ; bytecomp_c_compiler =
#          [ "gcc"
#          ; "-O2"
#          ; "-fno-strict-aliasing"
#          ; "-fwrapv"
#          ; "-pthread"
#          ; "-fPIC"
#          ; "-D_FILE_OFFSET_BITS=64"
#          ]
#      ; bytecomp_c_libraries = [ "-lm"; "-lpthread" ]
#      ; native_c_compiler =
#          [ "gcc"
#          ; "-O2"
#          ; "-fno-strict-aliasing"
#          ; "-fwrapv"
#          ; "-pthread"
#          ; "-fPIC"
#          ; "-D_FILE_OFFSET_BITS=64"
#          ]
#      ; native_c_libraries = [ "-lm" ]
#      ; native_pack_linker = [ "ld"; "-r"; "-o" ]
#      ; cc_profile = []
#      ; architecture = "amd64"
#      ; model = "default"
#      ; int_size = 63
#      ; word_size = 64
#      ; system = "linux"
#      ; asm = [ "as" ]
#      ; asm_cfi_supported = true
#      ; with_frame_pointers = false
#      ; ext_exe = ""
#      ; ext_obj = ".o"
#      ; ext_asm = ".s"
#      ; ext_lib = ".a"
#      ; ext_dll = ".so"
#      ; os_type = "Unix"
#      ; default_executable_name = "a.out"
#      ; systhread_supported = true
#      ; host = "x86_64-pc-linux-gnu"
#      ; target = "x86_64-pc-linux-gnu"
#      ; profiling = false
#      ; flambda = true
#      ; spacetime = false
#      ; safe_string = true
#      ; exec_magic_number = "Caml1999X031"
#      ; cmi_magic_number = "Caml1999I031"
#      ; cmo_magic_number = "Caml1999O031"
#      ; cma_magic_number = "Caml1999A031"
#      ; cmx_magic_number = "Caml1999y031"
#      ; cmxa_magic_number = "Caml1999z031"
#      ; ast_impl_magic_number = "Caml1999M031"
#      ; ast_intf_magic_number = "Caml1999N031"
#      ; cmxs_magic_number = "Caml1999D031"
#      ; cmt_magic_number = "Caml1999T031"
#      ; natdynlink_supported = true
#      ; supports_shared_libraries = true
#      ; windows_unicode = false
#      }
#  }
$ /home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/coqc --config > /tmp/dune_7d4d0d_output
$ /home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/coqc --print-version > /tmp/dune_31d788_output
$ (cd _build/default && /home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/coqdep -boot -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/btauto -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/cc -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/derive -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/extraction -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/firstorder -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/funind -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ltac -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ltac2 -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/micromega -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/nsatz -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/number_string_notation -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ring -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/rtauto -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ssreflect -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ssrmatching -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/tauto -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/tutorial -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/zify -R /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/theories Coq -Q /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/user-contrib/Equations Equations -R . TestEquations -dyndep opt -vos Eqn.v) > _build/default/.TestEquations.theory.d
$ (cd _build/default && /home/palmskog/.opam/4.14.1+flambda+coq.8.16/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/btauto -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/cc -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/derive -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/extraction -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/firstorder -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/funind -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ltac -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ltac2 -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/micromega -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/nsatz -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/number_string_notation -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ring -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/rtauto -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ssreflect -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/ssrmatching -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/tauto -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/tutorial -I /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/../coq-core/plugins/zify -R /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/theories Coq -Q /home/palmskog/.opam/4.14.1+flambda+coq.8.16/lib/coq/user-contrib/Equations Equations -R . TestEquations Eqn.v)
> File "./Eqn.v", line 1, characters 0-40:
> Error: Can't find file equations_plugin.cmxs on loadpath.
>
[1]
ejgallego commented 1 year ago

I looked at the code that should add the -I for equations and indeed it is there, so the bug must be some kind of silly mistake on our part.

ejgallego commented 1 year ago

@Alizter a dune describe coq-theories or something like that could be helpful to debug this.

ejgallego commented 1 year ago

Bug confirmed by printing the list of inferred coqpaths:

name: Equations 
path: /home/egallego/.opam/coq-v8.16/lib/coq/user-contrib/Equations 
cmxs: []
ejgallego commented 1 year ago

The scanning code seems pretty bogus, first bug is:

let scan_vo_cmxs ~path dir_contents =
  let f (d, kind) =
    Format.eprintf "considering %s\n" d;
    match kind with
    (* Skip some directories as Coq does, for now '-' and '.' *)
    | _ when String.contains d '-' -> List.Skip
    | _ when String.contains d '.' -> Skip

The latter condition makes indeed us to scan all files as they contain a dot (examples: Foo.vo equations_plugins.cmxs) etc...

Once we disable that, there are quite a few additional bugs:

name: Equations.Prop 
 path: /home/egallego/.opam/coq-v8.16/lib/coq/user-contrib/Equations/Prop 
 vo: /home/egallego/.opam/coq-v8.16/lib/coq/user-contrib/Equations/CoreTactics.vo
     /home/egallego/.opam/coq-v8.16/lib/coq/user-contrib/Equations/Init.vo
     /home/egallego/.opam/coq-v8.16/lib/coq/user-contrib/Equations/Signature.vo 
 cmxs: /home/egallego/.opam/coq-v8.16/lib/coq/user-contrib/Equations/equations_plugin.cmxs

I've exhausted my time bugdet for this for today, but that should provide a lead on the fix.

ejgallego commented 1 year ago

I did produce a fix in the end, see new PR.