-
Notifications
You must be signed in to change notification settings - Fork 134
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add website generated with the HTML backend like the stdlib? #17
Comments
Can you send me a link so that I can see what it looks like? Also, where would this be hosted? |
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!) |
Reminder: the codes in both links are clickable. |
As you can see from the stdlib's url, you'll know it's gonna be hosted on GitHub Pages. |
This looks good. How often does the html pages get generated? |
@mortberg We can let the CI do the work. In |
So every git-push will trigger the change of the website. |
I think we can start working on this. |
I second this and can help set it up if an agreement is reached. |
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 |
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 |
As well as Travis CI. You need to configure an access token for it |
HoTT-Coq has this: HoTT/Coq-HoTT#191 |
@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? |
Surely. When do we do that? |
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 :-) |
I guess Tuesday works for me, let's see :) I'll try to reach you on AIM. |
Until this issue is addressed, those who would like to browse |
Similarly I have this page |
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. |
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 |
So we can browse this project easier.
BTW I need an admin (like @UlfNorell) to enable gh-pages rendering for this repo.
The text was updated successfully, but these errors were encountered: