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.
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
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
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)
dune exec -- coqide should work
Nice works like a charm!
Last updated: Dec 07 2023 at 17:01 UTC