Ali Caglayan (Apr 27 2021 at 11:55): Ali Caglayan (Apr 27 2021 at 11:55):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
Ali Caglayan (Apr 27 2021 at 11:55):The coq submodule script probably needs to be updated
Ali Caglayan (Apr 27 2021 at 11:56):this is the message:
DUNE sources
COQDEP VFILES
DUNE sources
make[1]: *** [Makefile.build:378: coqocaml] Error 1
Error: no rule to make target coqocaml (or missing .PHONY)
make[1]: 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?
Théo Zimmermann (Apr 27 2021 at 12:00):Indeed, this target has probably been removed. Sorry for the trouble: HoTT passed in our own CI.
Ali Caglayan (Apr 27 2021 at 12:01):No worries, it looks like it is on our end then.
Ali Caglayan (Apr 27 2021 at 12:01):We are using this script to install coq through the submodule
Ali Caglayan (Apr 27 2021 at 12:01):https://github.com/HoTT/HoTT/blob/master/etc/install_coq.sh
Théo Zimmermann (Apr 27 2021 at 12:03):Hum I don't see coqocaml in this script but I do see coqlight which has also been removed...
Théo Zimmermann (Apr 27 2021 at 12:04):The targets should probably have been kept and mapped to what's closest to them now.
Théo Zimmermann (Apr 27 2021 at 12:08):What does it give if you replace this call to make coqlight coqide by dune build coq-core.install coqide-server.install coqide.install?
Gaëtan Gilbert (Apr 27 2021 at 12:10):files will still be in different place I think (_build/...)
Théo Zimmermann (Apr 27 2021 at 12:11):And actually coqlight also included the theories-light target, that is theory files in Init, Logic, Unicode and Arith. Not so sure it was really useful to HoTT though.
Théo Zimmermann (Apr 27 2021 at 12:12):BTW @Ali Caglayan does this Coq submodule still serve any purpose?
Ali Caglayan (Apr 27 2021 at 12:13):We are going to be deprecating its use soon but there are still people who are currently using it.
Ali Caglayan (Apr 27 2021 at 12:14):However I think it is fine to leave it as it is now, there is little need for any legacy support here
Ali Caglayan (Apr 27 2021 at 12:14):We can change some things round on our end
Théo Zimmermann (Apr 27 2021 at 12:16):What about keeping the submodule but not using it anymore for CI?
Ali Caglayan (Apr 27 2021 at 12:18):I think that's what we will end up doing
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:24):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 coqc and coqdep have been built.
Last updated: Oct 12 2024 at 12:01 UTC