Stream: Coq devs & plugin devs

Topic: Docs are unavailable


view this post on Zulip RanDair Scott Porter (Mar 08 2021 at 21:53):

Can't open the package documentation: https://coq.github.io/doc/master/api/coq/index.html is blank for me.

view this post on Zulip Gaëtan Gilbert (Mar 08 2021 at 21:56):

https://coq.github.io/doc/master/api/coq-core/index.html

view this post on Zulip Gaëtan Gilbert (Mar 08 2021 at 21:56):

and https://coq.github.io/doc/master/api/coqide-server/index.html

view this post on Zulip Théo Zimmermann (Mar 09 2021 at 12:50):

Can we put some sort of header / summary that would avoid making the coq package empty but explain that this is a virtual package and where to look for the actual docs?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 09 2021 at 15:23):

Sure, we can add some header, or maybe even tell odoc that there is not ML there; note that one thing that I was wondering is how to package the test suite, in the sense that for example opam packages have the @runtest stuff, so maybe Coq would not be so trivial if we add it?

view this post on Zulip Théo Zimmermann (Mar 09 2021 at 15:24):

Oh, if we can tell odoc to exclude some packages, then we should do the same for the coq-doc and coq-stdlib packages.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 09 2021 at 15:26):

Likely there is a way, if not should be easy to add, there was a lot of discussion actually in the OCaml / dune ecosystem about doc packages but I didn't follow it, but I think indeed it is easy to see there are many things to do w.r.t. documentation and opam etc...


Last updated: Oct 16 2021 at 07:02 UTC