Hi, since the dune buildsystem was merged our ci cannot build with coq master: https://github.com/HoTT/HoTT/pull/1469/checks?check_run_id=2447558725
The coq submodule script probably needs to be updated
this is the message:
DUNE sources COQDEP VFILES DUNE sources make: *** [Makefile.build:378: coqocaml] Error 1 Error: no rule to make target coqocaml (or missing .PHONY) make: Leaving directory '/home/runner/work/HoTT/HoTT/coq-HoTT' make: *** [Makefile.make:122: submake] Error 2 $ exit 2 $ exit 2 Error: Process completed with exit code 2.
@Emilio Jesús Gallego Arias do you know what is going on?
Indeed, this target has probably been removed. Sorry for the trouble: HoTT passed in our own CI.
No worries, it looks like it is on our end then.
We are using this script to install coq through the submodule
Hum I don't see
coqocaml in this script but I do see
coqlight which has also been removed...
The targets should probably have been kept and mapped to what's closest to them now.
What does it give if you replace this call to
make coqlight coqide by
dune build coq-core.install coqide-server.install coqide.install?
files will still be in different place I think (_build/...)
coqlight also included the
theories-light target, that is theory files in
Arith. Not so sure it was really useful to HoTT though.
BTW @Ali Caglayan does this Coq submodule still serve any purpose?
We are going to be deprecating its use soon but there are still people who are currently using it.
However I think it is fine to leave it as it is now, there is little need for any legacy support here
We can change some things round on our end
What about keeping the submodule but not using it anymore for CI?
I think that's what we will end up doing
I indeed removed the
light targets because they were quite adhoc and I was trying to reduce the number of targets to test; I'd recommend instead depending on what you actually need, coqdep will get most deps right, so usually all that you need is to ensure
coqdep have been built.
Last updated: Dec 01 2023 at 06:01 UTC