HTML Rendered Online Docs

[maxsnew]

We should make a gh-pages and automated deployment so that we can browse the library in glorious clickable HTML.

Check out the following for how cubical does it:

• Html in gh-pages agda/cubical#687
• Release for Agda 2.8.0 agda/cubical#1222
• fixup: make generate-everything.sh predicative agda/cubical#1241

[stschaef]

Can you make me an administrator of the repo so that I can set up a gh-pages via the settings page (which is currently inacessible)

[maxsnew]

I can't give you admin rights because it's my personal repo apparently. We can make an org I guess. You can just tell me what to do in the meantime

[stschaef]

Apologies for a bit of some git spam. I was trying to debug why the deployment wasn't triggering, and I thought it was because the action was triggered via a PR and not a push, so I push right to main a moment ago

But my hypothesis was wrong, as PRs do also triggered push events.

Currently, the deployment failed due a permissions error. It seems that the github pages deploy workflow isn't permissioned to push to to the gh-pages branch. I suspect this may be because it tries to force push, which IIRC you may have restricted for the repo. I believe changing permissions somewhere in the settings may fix this, I am also looking to see what else may be causing the failure

[stschaef]

Not an issue with force pushing. I fixed the deployment permissions error on the CI branch, and the docs should be accessible now. They are on the gh-pages branch, although I'm having an issue accessing the proper URLs

Will update this when I figure out how to access, update here, then merge the final workflow file into main

[stschaef]

Oh, I just had some malformed urls

Here's a link to the base level docs

http://maxsnew.com/cubical-categorical-logic/TestEverything

I'll make a better README to act as a project root, and we should probably put a link to these docs in the README/repo sidebar