Make Tactician depend on coq-core

[LasseBlaauwbroek]

With Coq's package split, the coq-tactician-stdlib package is now obsolete.

[LasseBlaauwbroek]

Mhm, there are still some issues with this, it seems. Converting to draft until coq/coq#16510 is addressed.

[palmskog]

@LasseBlaauwbroek looks like there are a bunch of fundamental build errors here, possibly related to Dune. Can you please take a look if they can be fixed in repo?

[LasseBlaauwbroek]

@palmskog I'm not entirely sure what you mean. I'm trying to resolve the compilation issues in coq/coq#16510. Do you mean you want this PR closed until the upstream issues are fixed? If so, feel free to close.

[LasseBlaauwbroek]

Thanks to the release of Dune 3.5 this should be ready now. CI is almost green, except for a strange, unrelated failure of coq.8.14.dev. I cannot reproduce this locally. Any ideas?

#=== ERROR while installing coq.8.14.dev ======================================#
# context              2.1.2 | linux/x86_64 | ocaml-base-compiler.4.14.0 | file:///builds/coq/opam-coq-archive/core-dev
# path                 ~/opam-root-4.14.0-2.1.2-sandbox/4.14.0/.opam-switch/build/coq.8.14.dev
# command              /usr/bin/make install
# exit-code            2
# env-file             ~/opam-root-4.14.0-2.1.2-sandbox/log/coq-138529-032261.env
# output-file          ~/opam-root-4.14.0-2.1.2-sandbox/log/coq-138529-032261.out
### output ###
# /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build install
# make[1]: Entering directory '/builds/coq/opam-coq-archive/opam-root-4.14.0-2.1.2-sandbox/4.14.0/.opam-switch/build/coq.8.14.dev'
# DUNE      sources
# dune install --display quiet  --mandir=""/builds/coq/opam-coq-archive/opam-root-4.14.0-2.1.2-sandbox/4.14.0/man"" --prefix="/builds/coq/opam-coq-archive/opam-root-4.14.0-2.1.2-sandbox/4.14.0" coq-core
# Entering directory '/builds/coq/opam-coq-archive'
# File "opam-root-4.14.0-2.1.2-sandbox/4.14.0/bin/dune", line 1, characters 0-0:
# Error: Invalid dune file
# make[1]: *** [Makefile.install:56: install-dune] Error 1
# make[1]: Leaving directory '/builds/coq/opam-coq-archive/opam-root-4.14.0-2.1.2-sandbox/4.14.0/.opam-switch/build/coq.8.14.dev'
# make: *** [Makefile.make:122: submake] Error 2
The former state can be restored with:
    /usr/local/bin/opam switch import "/builds/coq/opam-coq-archive/opam-root-4.14.0-2.1.2-sandbox/4.14.0/.opam-switch/backup/state-20221022162552.export"
'opam install coq-tactician.8.14.dev -y -v -v --with-test' failed.

[palmskog]

@LasseBlaauwbroek there are several failing jobs here, can you take a look?

[LasseBlaauwbroek]

@palmskog As in the message above, the failing jobs are due to coq.8.14.dev failing. I'm unsure why and I cannot reproduce this locally. In any case, it is unrelated to this PR.

[palmskog]

OK, since this is extra-dev, let's merge then.

[ejgallego]

That bug is due to dune detecting the workspace root in a place with an opam switch; then when dune scans the dirs for dune projects it will choke on the dune binary.

In general the CI should not setup the workspace like this.

[LasseBlaauwbroek]

@ejgallego Do you know why this only happens with 8.14 and not any other Coq version?

[ejgallego]

@LasseBlaauwbroek we likely did update Coq makefiles to avoid this problem in 8.15

[LasseBlaauwbroek]

I see. Well, probably not a huge issue anyway, since it is localized to the opam-coq-archive CI.

In any case, I'm happy that this was finally completed! I believe that this PR has been in the making for close to two years now :-) Thanks @ejgallego and everyone else who has worked to make this possible!