Fix coqdoc section titles

[jdchristensen]

I realized that I was using things like (** * text here *) incorrectly, causing headings to be much too long in the generated html documentation, so I fixed my mistakes. While I was at it, I found a few other places to fix.

Is there a way to preview the coqdoc html documentation before merging?

[Alizter]

@jdchristensen no preview unfortunately, however the built artefacts can be downloaded when the job is finished. That's how we inspected doc stuff before. I'll link it here when they finish.

[jdchristensen]

@Alizter Can I build the docs locally (easily)?

[Alizter]

@jdchristensen Yes, if you want to build with Dune you can do dune build @doc. It will probably complain about odoc but just ignore that. You will find the html files in _build/default/theories/HoTT.html/.

[jdchristensen]

I added instructions on comments to STYLE.md. Despite the instructions in that file, I manually updated the TOC at the top, since I don't have doctoc installed. Hope I did it right...

[jdchristensen]

I silenced all of the warnings coqdoc was generating, which were in fact valid warnings. Many of the pages look better now.

The only other issue I noticed is that some Category library comments use unicode, and the charset in the html files (both the toc and the individual files) isn't set to utf, so the unicode symbols appear garbled. Is it easy to change the generated html to use unicode?

[Alizter]

@jdchristensen Don't worry about the TOC too much, we can fix it when we come across it.

[Alizter]

Regarding unicode, I think it might be possible but I'll have to look into it later. Please open an issue about it.

[jdchristensen]

Regarding unicode, I think it might be possible but I'll have to look into it later. Please open an issue about it.

The docs say that you need to pass one of -utf8 or --utf8. In Makefile.coq.local-early, I see that -utf8 is specified. I can't see where dune is calling coqdoc, though.

[jdchristensen]

@jdchristensen Don't worry about the TOC too much, we can fix it when we come across it.

I tried viewing this PR's STYLE.md on github, and the TOC link worked fine, so all is good.

[Alizter]

@jdchristensen To pass flags to Dune (>=3.8) you need to use the coqdoc_flags field of the coq.theory stanza. I forgot that I even implemented this. Haha.

• feature(coq): add coqdoc_flags field to coq.theory ocaml/dune#7676

[Alizter]

FTR, there is this extension on VSCode that I was using the get the TOC. I checked myself and your version is fine.

[jdchristensen]

@jdchristensen To pass flags to Dune (>=3.8) you need to use the coqdoc_flags field of the coq.theory stanza.

I have verified that make correctly passes -utf8, so the html docs are good as produced by the CI. I don't understand your instructions above. Do you want to explain more or just push a separate fix of this yourself?

[Alizter]

@jdchristensen something like this:

--- a/theories/dune
+++ b/theories/dune
@@ -8,7 +8,8 @@
  (name HoTT)
  (package coq-hott)
  (modules :standard)
- (flags -noinit -indices-matter -color on))
+ (flags -noinit -indices-matter -color on)
+ (coqdoc_flags :standard --utf8))

You'll have to do the same for contrib and tests if you want to pass the same args (prob not). :standard just expands to --toc IIRC so you can omit it if you want to and replace or append it with the other flags you need. I didn't check.

[jdchristensen]

Currently make passes -interpolate -utf8 --no-externals $(COQDOCEXTRAFLAGS) (so it allows extra flags from the environment).

[Alizter]

@jdchristensen AFAICT we don't use that anywhere in the CI or anywhere else.

[Alizter]

Actually here is the same thing in Dune:

diff --git a/theories/dune b/theories/dune
index e033640d..b249275d 100644
--- a/theories/dune
+++ b/theories/dune
@@ -8,7 +8,8 @@
  (name HoTT)
  (package coq-hott)
  (modules :standard)
- (flags -noinit -indices-matter -color on))
+ (flags -noinit -indices-matter -color on)
+ (coqdoc_flags -interpolate -utf8 --no-externals %{env:COQDOCEXTRAFLAGS=}))

 ; TODO: Tests

[Alizter]

@jdchristensen Sorry if I was not clear earlier. I think you can remove :standard and just do the change I've mentioned above this comment.

[jdchristensen]

%{env:COQDOCEXTRAFLAGS=}

This causes: coqdoc: : no such file. With the change I just pushed, utf8 works properly. For some reason, the produced files seem quite different from what make produces, e.g. the order of things in the toc is different, and lots more. But I don't really feel like investigating further...

[Alizter]

@jdchristensen That's completely fine. We don't use the coqdoc feature of Dune. I opened an issue about it #1733 but didn't do anything further. You can think of it as another way to check doc locally. But the CI is the main builder of doc. We could clean up our infra and add CI previews etc. however I don't have too much time to sink into this. Currently most of my time for HoTT is playing around with the new 0gpd yoneda :)

[jdchristensen]

I think I'm done now!