Stream: Coq devs & plugin devs

Topic: How to link other projects in ci


view this post on Zulip Ali Caglayan (Dec 18 2021 at 08:45):

I am writing an overlay for ci-metacoq but I can't get dune exec coqide to find ci-equations, how do I link it?

view this post on Zulip Ali Caglayan (Dec 18 2021 at 08:51):

cc @Gaëtan Gilbert

view this post on Zulip Enrico Tassi (Dec 18 2021 at 08:57):

hum, if you make ci-metacoq then equations is installed in _build, so coqide will see it

view this post on Zulip Paolo Giarrusso (Dec 18 2021 at 09:01):

After you patch _CoqProject by hand, yes?

view this post on Zulip Paolo Giarrusso (Dec 18 2021 at 09:02):

(unless the makefiles do that for you?)

view this post on Zulip Paolo Giarrusso (Dec 18 2021 at 09:06):

-Q _build/default/path/to/equations/theories Equations is the kind of thing I must usually add, for each -Q/-R option.

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:11):

So I make ci-metacoq and the installation step for equations gets done

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:11):

There is not problem whilst building metacoq

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:12):

just when I try dune exec -- dev/shim/coqide-prelude on a file

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:12):

I'm guessing I am not passing the correct -R/-Q?

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:12):

Cannot find library Equations.Init in loadpath (while searching for a .vos file)

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:13):

I'm doing something like this:

 dune exec -- dev/shim/coqide-prelude _build_ci/metacoq/pcuic/theories/PCUICRename.v -R _build/install/default/lib/coq/user-contrib/Equations/ Equations

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:14):

So equations is definitely installed in _build/install/default/lib/coq/user-contrib/Equations/ but I have no idea how to get coqide to see this

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:18):

ah got it

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:19):

I had to pass -I and -R together

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:19):

working now thanks for the help

view this post on Zulip Enrico Tassi (Dec 18 2021 at 09:28):

hum, I guess 15220 shall help, no -I will be needed.
Do you really need -R?

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:31):

Yes, it cannot find Equations.Init

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:32):

Or there is no path bound to Equations

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:32):

Cannot load Equations.Init:
no physical path bound to
Equations

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:33):

Which makes sense, I don't see how coqide can know where equations is installed

view this post on Zulip Ali Caglayan (Dec 18 2021 at 09:33):

The only reason make works is because we explicitly pass the option no?

view this post on Zulip Enrico Tassi (Dec 18 2021 at 09:36):

It is in a standard path, which should be automatically mapped,IMO. boh ..

view this post on Zulip Enrico Tassi (Dec 18 2021 at 09:36):

maybe the shim has a bug

view this post on Zulip Enrico Tassi (Dec 18 2021 at 09:37):

@Gaëtan Gilbert surely knows better

view this post on Zulip Gaëtan Gilbert (Dec 18 2021 at 09:59):

don't use the shims for overlays
the shim is meant to be used with a partial build, eg when you do dune build theories/Program/Program.vo dune will create the _build/default file but not the _build/install/default/... file
if you dune build _build/install/default/lib/coq/theories/Program/Program.vo dune will put Program.vo there but IIRC not its dependencies, if you want them the only way I know is to do dune build and interrupt it once it starts building new stuff, IMO the shim is much nicer ;)
but when making overlays you want to fully dune build (or dune build coq-stdlib.install) so that's not a problem, and the binaries in _build/install/default/bin are the ones that know where to find the installed stuff (since coq-makefile installs in _build/install/default/.../user-contrib)

view this post on Zulip Gaëtan Gilbert (Dec 18 2021 at 10:08):

tldr dune exec -- coqide should work

view this post on Zulip Ali Caglayan (Dec 18 2021 at 20:46):

Nice works like a charm!


Last updated: Feb 06 2023 at 20:02 UTC