Stream: Coq devs & plugin devs

Topic: coq master for HoTT not working


view this post on Zulip 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

view this post on Zulip Ali Caglayan (Apr 27 2021 at 11:55):

The coq submodule script probably needs to be updated

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 27 2021 at 11:56):

@Emilio Jesús Gallego Arias do you know what is going on?

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 27 2021 at 12:01):

No worries, it looks like it is on our end then.

view this post on Zulip Ali Caglayan (Apr 27 2021 at 12:01):

We are using this script to install coq through the submodule

view this post on Zulip Ali Caglayan (Apr 27 2021 at 12:01):

https://github.com/HoTT/HoTT/blob/master/etc/install_coq.sh

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Apr 27 2021 at 12:10):

files will still be in different place I think (_build/...)

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Apr 27 2021 at 12:12):

BTW @Ali Caglayan does this Coq submodule still serve any purpose?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Apr 27 2021 at 12:14):

We can change some things round on our end

view this post on Zulip Théo Zimmermann (Apr 27 2021 at 12:16):

What about keeping the submodule but not using it anymore for CI?

view this post on Zulip Ali Caglayan (Apr 27 2021 at 12:18):

I think that's what we will end up doing

view this post on Zulip 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 16 2021 at 07:02 UTC