Topic: doc-gen build
Rob Lewis (Feb 01 2022 at 04:41):
FYI, doc-gen builds seem to be failing: https://github.com/leanprover-community/doc-gen/runs/5016395557?check_suite_focus=true
Rob Lewis (Feb 01 2022 at 04:42):
Haven't tried to diagnose yet, too late for me
Gabriel Ebner (Feb 01 2022 at 09:00):
I think that's a transient failure, it almost looks like an out of memory condition.
Rob Lewis (Feb 01 2022 at 19:13):
It's happened the last 8 (at least) doc builds, I keep getting emailed about it. We might just be hitting some memory cap
Rob Lewis (Feb 02 2022 at 14:52):
Is it possible to move doc-gen builds to the Hoskinson/Freiburg build servers for now? I won't have time to debug doc-gen this week. That could be an easy patch if it is a memory issue
Gabriel Ebner (Feb 02 2022 at 16:41):
This presumably requires some changes with the python packages (since we can't globally install them from the workflow).
Rob Lewis (Feb 04 2022 at 13:49):
I've disabled the doc build for now. It hasn't built in two days and is spamming me every two hours. I won't have time to look into it until Sunday at the earliest.
Gabriel Ebner (Feb 04 2022 at 14:08):
Sorry for the spam, had to reenable the workflow for testing https://github.com/leanprover-community/doc-gen/pull/157
Rob Lewis (Feb 04 2022 at 14:15):
I think if you're the one to start the workflow, you're the one who will get spammed!
Gabriel Ebner (Feb 04 2022 at 15:40):
Okay, I've moved the docs to the hoskinson vms and it looks like everything went smoothly.
Last updated: Aug 03 2023 at 10:10 UTC