Opam package erroring due to wrong file location

[MevenBertrand]

I have just been trying to use the opam package, but when trying to build a simple example, I get the following error:

Fatal error: exception Sys_error("/home/meven/.opam/autosubst-ocaml/share/autosubst/fintype.v: No such file or directory")
Raised by primitive operation at Stdlib.open_in_gen in file "stdlib.ml", line 398, characters 28-54
Called from Stdlib.open_in_bin in file "stdlib.ml" (inlined), line 406, characters 2-47
Called from Autosubst_lib__Program.read_file in file "lib/program.ml", line 74, characters 14-32
Called from Autosubst_lib__Program.copy_file in file "lib/program.ml" (inlined), line 102, characters 33-48
Called from Autosubst_lib__Program.gen_static_files.copy_static_file in file "lib/program.ml", line 130, characters 4-74
Called from Autosubst_lib__Program.gen_static_files in file "lib/program.ml", line 134, characters 20-48
Called from Autosubst_lib__Program.main in file "lib/program.ml", line 177, characters 9-75
Called from Stdlib__result.map in file "result.ml", line 25, characters 32-37
Called from Monadic__Result.MakeT.ResultMonad.bind in file "monadic/library/result.ml", line 31, characters 24-33
Called from Stdlib__result.map in file "result.ml", line 25, characters 32-37
Called from Monadic__Result.MakeT.ResultMonad.bind in file "monadic/library/result.ml", line 31, characters 24-33
Called from Dune__exe__Main.main in file "bin/main.ml", line 6, characters 12-35
Called from Dune__exe__Main in file "bin/main.ml", line 10, characters 9-16

It seems like the culprit is this line, which hardcodes that the files are to be found in the share/subst folder, while the opam installation puts them in share/coq-autosubst-ocaml.

[yforster]

Does it work if you change the path and compile manually? Maybe this is due to a change in opam? It seems to me like the comment above explains what is going on. If changing the path works, we can change the code and the layout in the repo to match the (maybe new) opam file layout

[MevenBertrand]

I could not find the files opam downloads to change & rebuild them manually, but using the other approach of renaming share/coq-autosubst-ocaml to share/autosubst in my opam installation, things seem to work fine.

[MevenBertrand]

My office mate suggests that this might be a dune change. The relevant information seems to be here regarding section vs section_root. So changing the dune recipe in share might be a solution. But changing the repo layout + this code line might be more robust (although there is probably a less hacky solution).

[TheoWinterhalter]

Hi. It seems to me the issue is not solved?
When I run autosubst I get

Fatal error: exception Sys_error("~/.opam/autosubst-ocaml/share/autosubst/unscoped.v: No such file or directory")

The real path is ~/.opam/autosubst-ocaml/share/coq-autosubst-ocaml/unscoped.v (notice how the second autosubst also has to be renamed to autosubst-ocaml).

[yforster]

Which branch are you working on?

https://github.com/uds-psl/autosubst-ocaml/blob/coq-8.13/lib/program.ml#L128C64-L128C64
https://github.com/uds-psl/autosubst-ocaml/blob/coq-8.14/lib/program.ml#L128C64-L128C64

Did you install from source or from opam?

[TheoWinterhalter]

I installed from opam using the instructions of the README (which installed Coq 8.13 in a fresh switch). (I also did opam update before so it's the latest available, ie. 1.0.0.)

[yforster]

Sorry, that's the problem. It seems I didn't release a new opam package.

If you clone, checkout coq-8.13 as branch, and do dune build, dune install you should be good to go

[TheoWinterhalter]

I see sorry.
EDIT: Can confirm it works.