Stream: Hierarchy Builder devs & users

Topic: HB master with Coq 8.13.2 fails to compile examples/readme.v


view this post on Zulip Anton Trunov (Jun 29 2021 at 15:13):

I'd like to build a project on top of HB-mathcomp, however, HB's master branch fails to compile (and it looks like HB 1.1.0 is not enough to build HB-mathcomp):

File "./examples/readme.v", line 4, characters 0-228:
Error:
builtin rex.split: 2th argument: expected string got Loc.t: File "./examples/readme.v", line 4, column 228, characters 93-306:

(commit eba74981f33026b56609e954a8dacb67e64bd2e5)

view this post on Zulip Enrico Tassi (Jun 29 2021 at 15:28):

Thigs are currently broken, I hope to be able to:

view this post on Zulip Enrico Tassi (Jun 29 2021 at 15:28):

This combo works here... sorry for the mess

view this post on Zulip Anton Trunov (Jun 29 2021 at 15:48):

Thanks a lot, that combination saves the day for me! Btw, I just noticed a substantial slowdown between Mathcomp's hierarchy-builder+factory_sort_tac branch and Mathcomp's current master branch.
For coq-mathcomp-ssreflect package it's:

make -j3  29,71s user 4,84s system 138% cpu 24,872 total

vs

make -j3  78,65s user 4,94s system 119% cpu 1:10,22 total

I guess some slowdown is expected, although it's about 2.6x in this case.

view this post on Zulip Enrico Tassi (Jun 29 2021 at 16:12):

I know, I'm working on it...

view this post on Zulip Enrico Tassi (Jun 29 2021 at 16:14):

I guess most of the time is spent in order.v in your case

view this post on Zulip Anton Trunov (Jun 29 2021 at 16:26):

Oh, I see, thanks a lot for all your hard work!

view this post on Zulip Christian Doczkal (Jul 05 2021 at 08:30):

Enrico Tassi said:

Thigs are currently broken, I hope to be able to:

Any progress on this? I would like to fix my CI at some point. I'm not sure there is a version of my code that compiles both with released versions of Coq/mathcomp/coq-eli/HB and the current development versions. Well, as of this night, the development version of HB also does not compile on the mathcomp-dev images, so there is even less I can do.

view this post on Zulip Enrico Tassi (Jul 05 2021 at 11:47):

1 is done

view this post on Zulip Enrico Tassi (Jul 05 2021 at 11:47):

2, I hope to discuss with @Cyril Cohen tomorrow

view this post on Zulip Enrico Tassi (Jul 05 2021 at 11:47):

3 comes with one click after 2

view this post on Zulip Enrico Tassi (Jul 05 2021 at 11:48):

(I'm sorry to give a pinch, but CI is never green... it's a fact of life ;-)

view this post on Zulip Christian Doczkal (Jul 05 2021 at 12:02):

Enrico Tassi said:

(I'm sorry to give a pinch, but CI is never green... it's a fact of life ;-)

Well, my retort to this is that my CI was almost never red before I started using HB. The stack coq, elpi, coq-elpi, HB is quite brittle compared to just coq+mathcomp.

view this post on Zulip Enrico Tassi (Jul 05 2021 at 12:04):

Fair enough, but you are putting the bar quite high

view this post on Zulip Christian Doczkal (Jul 05 2021 at 13:03):

Guess I have been spoiled. But I am very happy to have mathcomp in between my work and Coq ;)

view this post on Zulip Cyril Cohen (Jul 05 2021 at 14:37):

@Christian Doczkal What I do not understand is: are you depending on the master version of HB right now?

view this post on Zulip Christian Doczkal (Jul 05 2021 at 14:40):

Well, I test against coq-dev/mathcomp-dev to see what's coming, and I am not aware of any other version of HB that compiles against coq-dev.

view this post on Zulip Cyril Cohen (Jul 05 2021 at 14:41):

I see! thanks for the clarification

view this post on Zulip Christian Doczkal (Jul 05 2021 at 14:41):

Sure, I could stop testing against coq-dev and only test against mathcomp-dev with a stable HB, but so far the other setting has been working well for all of my developments.

view this post on Zulip Cyril Cohen (Jul 05 2021 at 14:46):

Christian Doczkal said:

Sure, I could stop testing against coq-dev and only test against mathcomp-dev with a stable HB, but so far the other setting has been working well for all of my developments.

No I guess what you are doing is sensible, but I am not sure it is expected that the CI is always green, as long as you know why and what's coming up and can still anticipate before the release...

view this post on Zulip Christian Doczkal (Jul 05 2021 at 14:48):

What is frustrating is that it's been broken for three weeks and the only reason is that the new HB makes something that works an error rather than a warning, and the attribute to disable the warning causes an error in the stable version. So the fix could have been to simply downgrade the error to a warning. :neutral:

view this post on Zulip Christian Doczkal (Jul 08 2021 at 06:49):

Umm, after a build error last night, I am back to getting

  - Error:
  - HB: non forgetful inheritance detected.

https://github.com/coq-community/graph-theory/runs/3015865204?check_suite_focus=true#step:4:758

I thought #259 was supposed to have turned this into a warning. :confused:

view this post on Zulip Enrico Tassi (Jul 08 2021 at 07:13):

Master is ok, but we did not merge it into coq-master which is what you build. I will take care of it.

view this post on Zulip Enrico Tassi (Jul 08 2021 at 09:19):

done

view this post on Zulip Christian Doczkal (Jul 08 2021 at 16:17):

CI is green again, thanks! :+1:


Last updated: Jan 29 2023 at 16:02 UTC