Zulip Chat Archive
Stream: mathlib4
Topic: 11-20 nightly mathlib3port
Jireh Loreaux (Nov 21 2022 at 06:27):
@Gabriel Ebner it seems that the CI for the mathlib3port nightly didn't run on 11-20. Wanted to mention it in case it needs fixing.
Gabriel Ebner (Nov 21 2022 at 06:27):
Thanks for pinging me!
Gabriel Ebner (Nov 21 2022 at 06:28):
I've fixed the issue three hours ago: https://github.com/leanprover-community/mathport/commit/89e6545211bf76f3f20d2c2d3e7c57f64776c962
Gabriel Ebner (Nov 21 2022 at 06:28):
Relevant lake issue: https://github.com/leanprover/lake/issues/137
Jireh Loreaux (Nov 21 2022 at 23:09):
@Gabriel Ebner I still don't see any synport output on the mathlib3port repo, but I do see that mathport CI has the predata built for the last two days. Do we need to run mathport ourselves to get the synport output? Or is there some place else I should be looking for it?
Gabriel Ebner (Nov 21 2022 at 23:13):
Sorry, same bug as yesterday. https://github.com/leanprover/lake/issues/137
Jireh Loreaux (Nov 21 2022 at 23:24):
Oh sorry, I didn't realize that it wasn't fixed yesterday. That's fine, thanks!
Gabriel Ebner (Nov 22 2022 at 17:53):
Just to give you an update: the whole mathport CI is broken ATM. The fix is blocked on https://github.com/leanprover/lake/pull/138 For now I've removed aesop as a workaround. I hope we can get a proper fix out before Thanksgiving.
Scott Morrison (Nov 22 2022 at 17:55):
No problem. For now aesop is only being used in my (unpublished) category_theory branch, which probably won't want merging before thanksgiving. :-) I'm glad I added aesop ahead of time, though!
Gabriel Ebner (Nov 22 2022 at 17:57):
Unfortunately, the mathlib bump broke mathport in a different way. :exhausted:
Gabriel Ebner (Nov 22 2022 at 18:54):
@Mario Carneiro This was due to the using_well_founded change. Apparently sometimes the extra node is not added to the parent AST. See https://github.com/leanprover-community/mathport/commit/176fcb59a30cd5403c8dac26162ed1ea02e161a9
Mario Carneiro (Nov 22 2022 at 19:02):
do you have an example? That was the reason the code didn't work before, so this indicates that the lean bugfix is insufficient
Mario Carneiro (Nov 22 2022 at 19:04):
I'm okay with using opt' for now but nodes are not supposed to have varying size, that's a lean bug
Mario Carneiro (Nov 22 2022 at 19:28):
Gabriel Ebner (Nov 22 2022 at 20:05):
example
Yes, already init.core has plenty.
Last updated: Dec 20 2023 at 11:08 UTC