Stream: Coq devs & plugin devs

Topic: HoTT failing on CI


view this post on Zulip Pierre-Marie Pédrot (Nov 09 2020 at 11:08):

HoTT has been failing on our ci for a few days, with the following error.

File "./coq/theories/Init/Prelude.v", line 14, characters 0-44:
Error:
File not found on loadpath : numeral_notation_plugin.cmxs

view this post on Zulip Pierre-Marie Pédrot (Nov 09 2020 at 11:08):

Any idea why, and what caused this?

view this post on Zulip Gaëtan Gilbert (Nov 09 2020 at 11:11):

waiting for overlay

view this post on Zulip Pierre-Marie Pédrot (Nov 09 2020 at 11:11):

Aha.

view this post on Zulip Pierre-Marie Pédrot (Nov 09 2020 at 11:12):

What is taking so long for the overlay to be merged?

view this post on Zulip Ali Caglayan (Nov 09 2020 at 13:36):

So the CI is failing on one job currently. This is to do with coqdpdgraph

view this post on Zulip Ali Caglayan (Nov 09 2020 at 13:39):

My guess is 8.13 changes something in the api causing this line in dpdgraph to fail: https://github.com/Karmaki/coq-dpdgraph/blob/f12bf892561ccffe5382d97ae2684a7dae326e64/searchdepend.mlg#L54

view this post on Zulip Ali Caglayan (Nov 09 2020 at 13:39):

@Yves Bertot Can you confirm this to be the issue?

view this post on Zulip Théo Zimmermann (Nov 09 2020 at 13:41):

Which version of dpdgraph do you install? The dev one or the latest release? Because the dev version already received compatibility patches for Coq 8.13 I believe.

view this post on Zulip Ali Caglayan (Nov 09 2020 at 13:43):

Yeah it looks like we need to bump the submodule

view this post on Zulip Ali Caglayan (Nov 09 2020 at 13:47):

okay I've created a pr for bumping the submodule

view this post on Zulip Ali Caglayan (Nov 09 2020 at 13:47):

Once it is green I will merge it and reset the ci for the overlay

view this post on Zulip Ali Caglayan (Nov 09 2020 at 13:56):

OK, I've pushed a commit to the overlay, hopefully everything will be green this time.

view this post on Zulip Ali Caglayan (Nov 09 2020 at 14:42):

I've merged the overlay

view this post on Zulip sameer gupta (Mar 27 2021 at 17:05):

Not sure if this is the right place to post this, but I got kinda sorta inducted into development of type-holes for code completion : r nd group, any tips to make progress are welcome

view this post on Zulip Gaëtan Gilbert (Mar 27 2021 at 17:54):

what's the problem?

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2021 at 08:31):

HoTT has been failing again with /bin/bash: etc/coq-scripts/github/reportify-coq.sh: No such file or directory, anyone has an idea of the reason?

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2021 at 08:32):

if I read correctly, https://github.com/HoTT/HoTT/pull/1465 should solve it, right?

view this post on Zulip Ali Caglayan (Apr 20 2021 at 08:45):

I've merged that PR

view this post on Zulip Pierre-Marie Pédrot (Apr 20 2021 at 08:48):

Thanks!


Last updated: Oct 16 2021 at 03:02 UTC