Ali Caglayan (May 06 2021 at 22:39): Ali Caglayan (May 06 2021 at 22:39):Hi when using the coqide shim I get this:
/home/ali/coq/_build/default/dev/shim/coqide-prelude: line 2: /home/ali/coq/_build/default/dev/shim//usr/local/bin/coqide: No such file or directory
I guess something is set up wrong?
Ali Caglayan (May 06 2021 at 22:39):The shims for coqtop work fine
Ali Caglayan (May 06 2021 at 22:43):For whatever reason the coqide shim looks like it is putting two // before usr
Ali Caglayan (May 06 2021 at 22:44):Could it be because I haven't built the stdlib?
Ali Caglayan (May 06 2021 at 23:29):Ah OK I didn't run ./configure!
Théo Zimmermann (May 07 2021 at 07:23):You're not supposed to need ./configure to use the shim. However, you should make sure it is built by running dune build dev/shim/coqide-prelude.
Emilio Jesús Gallego Arias (May 07 2021 at 11:27):Indeed it is always better to run the shim with dune exec -- shim to ensure its dependencies are built
Ali Caglayan (May 07 2021 at 12:11):Yeah, it seems I was missing some dependencies, but this wasn't visible from dune exec. After installing the dependencies, everything works fine.
Théo Zimmermann (May 07 2021 at 13:13):Indeed, unfortunately, the output of dune exec is quite limited.
Last updated: Oct 13 2024 at 01:02 UTC