Patrick Nicodemus (Apr 04 2023 at 18:12): Patrick Nicodemus (Apr 04 2023 at 18:12):I wanted to write some Elpi code that interfaces with Coq, so I wanted to import some of the libraries here - https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-command-template.elpi
I added the lines of code:
accumulate "/home/patrick/coq/elpi/coq-elpi/elpi/elpi-reduction".
accumulate "/home/patrick/coq/elpi/coq-elpi/elpi/elpi-ltac".
because I was not sure what the proper way was to access those files.
This gives me an error:
Error: File "/home/patrick/.opam/ocaml-base-compiler/.opam-switch/build/coq-elpi.1.16.0/./elpi/elpi-ltac.elpi", line 5, column 0, character 303:duplicate type abbreviation for open-tactic. Previous declaration: File "/home/patrick/coq/elpi/coq-elpi/elpi/elpi-ltac.elpi", line 5, column 0, character 303:
This error does not make sense. The file path it is talking about does not exist. The only thing in the folder ocaml-base-compiler/.opam-switch is Trakt. I don't know where coq-elpi is installed but it's not there.
Patrick Nicodemus (Apr 04 2023 at 18:12):I am using VSCode with Enrico's extension.
Paolo Giarrusso (Apr 05 2023 at 09:42):that .opam-switch path is likely the one where coq-elpi existed _when it was built_
Paolo Giarrusso (Apr 05 2023 at 09:44):some compiled artifact might have stored that path? but I'm less sure what else is going on
Enrico Tassi (Apr 05 2023 at 12:29):The libraries accumulated in the template files are automatically loaded when you define an Elpi Tactic or Elpi Command.
This is why the error talks about a duplicate type abbreviation, you are loading the files twice.
Enrico Tassi (Apr 05 2023 at 12:31):When you write Elpi Command foo. the contents of elpi-command-template are loaded for you, when you write Elpi Tactic bar. then elpi-tactic-template is loaded. If you need an empty program, write Elpi Program baz. (not recommended).
Patrick Nicodemus (Apr 05 2023 at 16:12):Enrico Tassi said:
The libraries accumulated in the template files are automatically loaded when you define an Elpi Tactic or Elpi Command.
This is why the error talks about a duplicate type abbreviation, you are loading the files twice.
Ok! Is it possible to access the libraries in the template files from a *.elpi file? For modularity I would rather not have everything in a *.v file.
Last updated: Oct 13 2024 at 01:02 UTC