doc-gen build

Stream: general

[Rob Lewis]

FYI, doc-gen builds seem to be failing: https://github.com/leanprover-community/doc-gen/runs/5016395557?check_suite_focus=true

[Rob Lewis]

Haven't tried to diagnose yet, too late for me

[Gabriel Ebner]

I think that's a transient failure, it almost looks like an out of memory condition.

[Rob Lewis]

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]

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]

This presumably requires some changes with the python packages (since we can't globally install them from the workflow).

[Rob Lewis]

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]

Sorry for the spam, had to reenable the workflow for testing https://github.com/leanprover-community/doc-gen/pull/157

[Rob Lewis]

I think if you're the one to start the workflow, you're the one who will get spammed!

[Gabriel Ebner]

Okay, I've moved the docs to the hoskinson vms and it looks like everything went smoothly.