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?
cc @Gaëtan Gilbert
hum, if you make ci-metacoq
then equations is installed in _build
, so coqide will see it
After you patch _CoqProject by hand, yes?
(unless the makefiles do that for you?)
-Q _build/default/path/to/equations/theories Equations
is the kind of thing I must usually add, for each -Q/-R option.
So I make ci-metacoq
and the installation step for equations gets done
There is not problem whilst building metacoq
just when I try dune exec -- dev/shim/coqide-prelude
on a file
I'm guessing I am not passing the correct -R/-Q?
Cannot find library Equations.Init in loadpath (while searching for a .vos file)
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
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
ah got it
I had to pass -I
and -R
together
working now thanks for the help
hum, I guess 15220 shall help, no -I will be needed.
Do you really need -R?
Yes, it cannot find Equations.Init
Or there is no path bound to Equations
Cannot load Equations.Init:
no physical path bound to
Equations
Which makes sense, I don't see how coqide can know where equations is installed
The only reason make works is because we explicitly pass the option no?
It is in a standard path, which should be automatically mapped,IMO. boh ..
maybe the shim has a bug
@Gaëtan Gilbert surely knows better
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)
tldr dune exec -- coqide
should work
Nice works like a charm!
Last updated: Oct 13 2024 at 01:02 UTC