Github Actions

[bryangingechen]

This workflow builds mathlib docs for each commit pushed to any branch and additionally deploys the built docs to the web for each commit to master. (This way we don't have to manually trigger a build on mathlib to update the docs.)

[gebner]

I think it is a good idea to have CI here as well. I'm not so sure I like the duplication of the deployment logic and responsibility. I'm pretty sure we'll forget to update one of them in the future.

[bryangingechen]

Good point. As far as reducing deployment logic, I can try to make one script (merging ci.sh here and deploy_docs.sh in mathlib) that we can run both here and in mathlib's workflow. Would it be better to host that here or in mathlib?

Edit: I haven't done any work on this yet, but I've decided it makes more sense to put a script that builds mathlib docs in the mathlib scripts. We can revisit this down the line as doc-gen evolves.

[bryangingechen]

OK, this now uses the deploy_docs.sh script from mathlib.

[gebner]

It looks like there was a problem with authentication (CI has failed on master):

git push -f origin HEAD:master
remote: Invalid username or password.
fatal: Authentication failed for 'https://github.com/leanprover-community/mathlib_docs.git/'

[bryangingechen]

@gebner Yeah, I noticed this yesterday: 885b7e5#commitcomment-39774481

Basically, I forgot to add the secret before this PR was merged.