[ close #3373 ] Implement the proposed feature

[ice1000]

Signed-off-by: ice1000 ice1000kotlin@foxmail.com

Everything has already been covered in #3373

[ice1000]

We can try render the user manual with our new HTML backend with --html-highlight=auto!

[ice1000]

Makes my day

[ice1000]

@vlopezj say something?

Just curious, what's your timezone? It's 4:48 a.m. here.

[ice1000]

CI passed! Yay!

[vlopezj]

@ice1000 It looks good; but I'll look at it in more detail this afternoon (I'm in Europe/Stockholm).

We can try render the user manual with our new HTML backend with --html-highlight=auto!

Yes, this is the way to go. There are however two issues that make it non-straightforward:

• We would need to process the .rst files for the documentation for each commit, using that commit's version of Agda. I don't know this would fit with the current Readthedocs building methodology.

  https://docs.readthedocs.io/en/latest/builds.html#how-we-build-documentation

• Read the docs also generates PDF files, which I assume do not support the HTML blocks.
  (But this is fine, we can keep generating the PDF from the original .lagda.rst files).

[gallais]

I don't know this would fit with the current Readthedocs building methodology.

Note that we could push the generated html to github and have it sit at agda.github.io.
We already do something similar for the standard library

[ice1000]

We would need to process the .rst files for the documentation for each commit, using that commit's version of Agda. I don't know this would fit with the current Readthedocs building methodology.

It shouldn't be a big problem to put the code-rendered rst files into the repo. It's possible to let Travis CI do this (although I don't know how to let Travis CI push commits into a repo without using a GitHub password). Why do we need to do it for each commit? Do you mean each commit since the very beginning or from now on?

[vlopezj]

The functions highlightOnlyCode and highlightedFileExt are specific to the HTML backend. They should go in Agda.Interaction.Highlighting.HTML.

[ice1000]

Sure! I thought it'll be used somewhere else when I first impl these but seems not.

[vlopezj]

As @gallais pointed out, it seems we are already doing essentially the same thing for the Agda standard library (generating HTML files from Agda and pushing them to github pages). For the user manual, we have two steps: generating .rst files, and then generating .html files from the .rst files.

It seems that this can be done with Travis. To avoid the need for a Github password, I think you can generate some form of token, give it to Travis, and then reference it from the .travis.yml file:

https://github.com/agda/agda-stdlib/blob/master/.travis.yml

If we have this, I think it will be easier to bypass read the docs completely and just publish HTML files directly under https://agda.github.io/docs .

@ice1000 In any case, the first step would be to have a Makefile rule (such as make user-manual-html-highlighted) that can actually generate the .rst files with the embedded HTML, and then build the HTML manual from them. Putting the result online will then be easy.

[ice1000]

@ice1000 In any case, the first step would be to have a Makefile rule (such as make user-manual-html-highlighted) that can actually generate the .rst files with the embedded HTML, and then build the HTML manual from them. Putting the result online will then be easy.

IMO It's a separated task. I like this idea but I'm not gonma do that in this PR.

[vlopezj]

IMO It's a separated task. I like this idea but I'm not gonma do that in this PR.

Makes sense.

Then it looks ready for merging (apart from the comment about highlightOnlyCode and highlightedFileExt). I assume the end result will be a single commit. You can rebase it on master instead of merging if you want to avoid creating an extra merge commit.

[ice1000]

@vlopezj Rebased on master, Added changelog, documentation and addressed your comment. Please take a look.

[ice1000]

CI failed because I deleted the branch too fast and they failed to pull them and build 😂