Add website generated with the HTML backend like the stdlib? about cubical

[ayberkt]

This is not really an urgent matter and we can address it later. I tried looking at the CI machinery and it seems more complicated than I expected.

Perhaps, someone more familiar with it can tweak it to call agda --html and then tell Travis to publish the generated HTML. I think that should be all? If that's the case, this should be quite easy but as @ice1000 pointed out, GitHub Pages will have to be enabled.

[mortberg]

@ice1000 If we're going to do anything about this now might be a good time that we're all working on the library at the same time. Do you think we should do something now?

[mortberg]

Can you send me a link so that I can see what it looks like? Also, where would this be hosted?

[ice1000]

The stdlib: https://agda.github.io/agda-stdlib

Also we have literate Agda, which allowd us to have: https://ice1000.org/lagda/CubicalAgdaLiterate.html (it's a modified version of your writing! As a CuTT learner, I really appreciate your work!)

[ice1000]

Reminder: the codes in both links are clickable.

[ice1000]

As you can see from the stdlib's url, you'll know it's gonna be hosted on GitHub Pages.
It's free and https.

[mortberg]

This looks good. How often does the html pages get generated?

[ice1000]

@mortberg We can let the CI do the work. In agda-stdlib, we have a GH_TOKEN global variable that stores someone's GitHub token which has the rights to push to a branch of agda-stdlib.

[ice1000]

So every git-push will trigger the change of the website.

[ice1000]

I think we can start working on this.

[ayberkt]

@ice1000

I think we can start working on this.

I second this and can help set it up if an agreement is reached.

[ice1000]

You should @ @mortberg or @Saizan because they have admin access to this repo, I don't

[mortberg]

What do I need to do? I'm very busy with other things at the moment, so I won't have time to do any work on this until the end of the semester. But if it's just about giving some rights then I can try to do it quickly

[ice1000]

As well as Travis CI. You need to configure an access token for it

[ice1000]

HoTT-Coq has this: HoTT/Coq-HoTT#191

[ice1000]

Surely. When do we do that?

[mortberg]

Maybe Tuesday next week? Do we need to involve someone else?

Note that I'm really clueless about how these things work, but I'm of course happy to help out with providing whatever rights needed to set it up :-)

[ice1000]

I guess Tuesday works for me, let's see :) I'll try to reach you on AIM.

[ayberkt]

Until this issue is addressed, those who would like to browse cubical in HTML can use the pages that are automatically generated when I generate HTML from my development that uses cubical.

[ice1000]

Similarly I have this page

[brendanzab]

Just wanna say that this would be greatly appreciated! I've been really glad that the generated Agda Categories sources are available on Github Pages - it's much easier to navigate those as opposed to the sources on Github.

[brendanzab]

If you are already using github pages then you might be able to use this action to deploy in a pretty pain-free way (I don't think it even requires a token now). I'd recommend making a .github/workflows/cd-ubuntu.yaml file that runs on pushes to master, builds the HTML doc, then runs the JamesIves/github-pages-deploy-action to upload the output directory to pages. Here's an example of what I set up for another (non-Agda) project: https://github.com/brendanzab/ocaml-flake-example/blob/main/.github/workflows/cd.yml