switch opam ci to docker

[gares]

No description provided.

[gares]

This is where the stdlib is:

...
/home/runner/work/coq-elpi/coq-elpi/_opam/lib/coq/theories/Strings/BinaryString.vo
/home/runner/work/coq-elpi/coq-elpi/_opam/lib/coq/theories/Strings/PrimStringAxioms.vo
find: ‘/proc/tty/driver’: Permission denied
/home/runner/work/coq-elpi/coq-elpi/_opam/lib/coq/user-contrib/Ltac2/Pattern.vo
/home/runner/work/coq-elpi/coq-elpi/_opam/lib/coq/user-contrib/Ltac2/Std.vo
/home/runner/work/coq-elpi/coq-elpi/_opam/lib/coq/user-contrib/Ltac2/RedFlags.vo
...

@proux01 is it supposed to be in coq/ (not rocq)?

[proux01]

Yes, it is still coq, this hasn't been renamed yes (and I fer we'll have a hard time doing that renaming with dune).

[gares]

The error is now different:

dune build  -p coq-elpi @install
Error: path outside the workspace:
../../../_opam/lib/coq-core/plugins/ltac/ltac_plugin.cmxs from
default/theories
-> required by _build/default/theories/elpi.glob
-> required by _build/install/default/lib/coq/user-contrib/elpi/elpi.glob
-> required by _build/default/coq-elpi.install
-> required by alias install

I think it was a recent change to coqdep to spit recursive dependencies.
Am I right @SkySkimmer ?

The peculiarity here could be that setup-ocaml puts the opam root in ./, next to _build, eg inside dune's workspace