Zulip Chat Archive

Stream: general

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: Dec 20 2023 at 11:08 UTC