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
Any idea why, and what caused this?
waiting for overlay
Aha.
What is taking so long for the overlay to be merged?
So the CI is failing on one job currently. This is to do with coqdpdgraph
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
@Yves Bertot Can you confirm this to be the issue?
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.
Yeah it looks like we need to bump the submodule
okay I've created a pr for bumping the submodule
Once it is green I will merge it and reset the ci for the overlay
OK, I've pushed a commit to the overlay, hopefully everything will be green this time.
I've merged the overlay
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
what's the problem?
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?
if I read correctly, https://github.com/HoTT/HoTT/pull/1465 should solve it, right?
I've merged that PR
Thanks!
Last updated: Oct 13 2024 at 01:02 UTC