Anton Trunov (Jun 29 2021 at 15:13): 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)
Enrico Tassi (Jun 29 2021 at 15:28):Thigs are currently broken, I hope to be able to:
Enrico Tassi (Jun 29 2021 at 15:28):This combo works here... sorry for the mess
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.
Enrico Tassi (Jun 29 2021 at 16:12):I know, I'm working on it...
Enrico Tassi (Jun 29 2021 at 16:14):I guess most of the time is spent in order.v in your case
Anton Trunov (Jun 29 2021 at 16:26):Oh, I see, thanks a lot for all your hard work!
Christian Doczkal (Jul 05 2021 at 08:30):Enrico Tassi said:
Thigs are currently broken, I hope to be able to:
- release coq-elpi today https://github.com/LPCIC/coq-elpi/pull/257
- merge in HB master https://github.com/math-comp/hierarchy-builder/pull/252
- merge in MC/hierarchy-builder https://github.com/math-comp/math-comp/tree/hierarchy-builder+factory_sort_tac
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.
Enrico Tassi (Jul 05 2021 at 11:47):1 is done
Enrico Tassi (Jul 05 2021 at 11:47):2, I hope to discuss with @Cyril Cohen tomorrow
Enrico Tassi (Jul 05 2021 at 11:47):3 comes with one click after 2
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 ;-)
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.
Enrico Tassi (Jul 05 2021 at 12:04):Fair enough, but you are putting the bar quite high
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 ;)
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?
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.
Cyril Cohen (Jul 05 2021 at 14:41):I see! thanks for the clarification
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.
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...
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:
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:
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.
Enrico Tassi (Jul 08 2021 at 09:19):done
Christian Doczkal (Jul 08 2021 at 16:17):CI is green again, thanks! :+1:
Last updated: Oct 08 2024 at 14:01 UTC