Skip to content
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

Package Documentation Brainstorm #6

Open
mattam82 opened this issue Dec 25, 2024 · 4 comments
Open

Package Documentation Brainstorm #6

mattam82 opened this issue Dec 25, 2024 · 4 comments
Labels
packages About the Rocq Opam Packages

Comments

@mattam82
Copy link
Member

We need to think about how we want to handle package documentation and linking to it from the website

@mattam82 mattam82 added the packages About the Rocq Opam Packages label Dec 25, 2024
@palmskog
Copy link
Contributor

palmskog commented Dec 25, 2024

For the record, I've come to the conclusion that it's a bad idea to host package version coqdoc inside a GitHub repo, e.g., in a gh-pages branch using GitHub Pages, since it grows the repo size and is a pain to maintain without very good automation. What I think would be feasible:

  • if they want, project maintainers generate and continually deploy coqdoc for their main/master branch inside their repo
  • Coq Platform has automation to build and deploy coqdoc documentation for all its packages and put it in a repo like what is done with the Stdlib documentation
  • the centrally generated documentation for Platform packages is linked in their opam packages and appear on the rocq-prover website

@silene
Copy link

silene commented Dec 27, 2024

I don't think we need to do anything about documentation. Most (all?) packages already have a homepage field; some even have a doc field. These URLs could be used in place of the disparaging "no documentation" warning.

Also, limiting the platform documentation to only the things generated by coqdoc would be a net regression, especially for people who actually bother writing some structured documentation, e.g., https://flocq.gitlabpages.inria.fr/theos.html

@palmskog
Copy link
Contributor

palmskog commented Dec 27, 2024

Fine by me if some packages generate their own documentation and make it available through doc or homepage.

But for Platform packages, I think documentation should be handled in a consistent way, e.g., doc always leads to relevant generated coqdoc/ocamldoc documentation. And most Platform maintainers don't have cycles and/or motivation to set this up. So some central way of hosting coqdoc/ocamldoc HTML linked to in doc could be used for those packages, i.e., those that don't want to set up their own solution. Ideally the HTML could be generated directly from the opam package using with-doc option.

@gares
Copy link
Member

gares commented Dec 27, 2024

IMO the best option is to let git*.com host the doc, and provide tools and templates to help people set things up.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
packages About the Rocq Opam Packages
Projects
None yet
Development

No branches or pull requests

4 participants