Stream: Coq devs & plugin devs

Topic: coqide shim not working


view this post on Zulip 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?

view this post on Zulip Ali Caglayan (May 06 2021 at 22:39):

The shims for coqtop work fine

view this post on Zulip Ali Caglayan (May 06 2021 at 22:43):

For whatever reason the coqide shim looks like it is putting two // before usr

view this post on Zulip Ali Caglayan (May 06 2021 at 22:44):

Could it be because I haven't built the stdlib?

view this post on Zulip Ali Caglayan (May 06 2021 at 23:29):

Ah OK I didn't run ./configure!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 07 2021 at 13:13):

Indeed, unfortunately, the output of dune exec is quite limited.


Last updated: Oct 21 2021 at 21:03 UTC