[ #3366 ] File extension for output of HTML backend

[ice1000]

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

Everything is already covered in #3366 except:

• We need to discuss that whether the references in the generated HTML files should refer to files ending with HTML or make it customizable.

[ice1000]

This is a work in progress, don't merge right now.

[vlopezj]

@ice1000 Neat!

For your particular question, I think the file extension for the links should be .html, because in the end all the modules will turn into files with the .html extension.

However, I think we should think through at least one use case before developing this further. For instance:

---

Scenario A: Blogpost

1. Alice wants to write a blogpost with Agda code. She writes the blog post as a my-blog-post.lagda.md file. (1) She wants Agda to typecheck and highlight the Agda code as HTML, and she will then process the markdown into HTML using some other tool (f.ex. pandoc, a static site generator, or a JavaScript slide framework).
2. Case 1, and also in the blog post she uses other modules, whose code she wants to publish together with her blog post as HTML documents. Some of these other modules are .agda files. As for these modules, she wants to render them into a full HTML document.
3. Case 2., and also some of the additional modules are .lagda.md files. She wants Agda to output highlighted .md files for these modules which she can then process using some other tool.

---

Currently Agda will uniformly apply the same behavior to all files reachable from the given module, which prevents us from having different highlighting and file extension behavior for each module in the project.

Perhaps those of you who expressed interest in #3313 (@UlfNorell @gallais @asr @andreasabel and @nad ) and/or plan to use Agda on Markdown files can clarify your use cases, and see if Scenario A can be simplified or refined.

[ice1000]

Does Agda save information like whether a file is a lagda file?

[vlopezj]

Not that I know of…

On the other hand, many internal structures (names, tokens, …) are annotated with Position or Interval, which denote locations in files. I think that the C.TopLevelModuleName in Agda.Interaction.Highlighting.HTML has a Range that you can obtain by calling getRange on it. You can then obtain the file by calling rangeFile on the result. (See Agda.Syntax.Position).

Once you have the filename, it is easy to get the extension, and from there the HTML module can decide what to do.

There is already a list of supported literate file extensions in Agda.Syntax.Parser.Literate.literateProcessors, which specifies the logic about how the literate file should be parsed. The logic about how the --html flag should behave depending on the file extension can also be put there. That way we avoid having two separate lists of file extensions.

The function Agda.Syntax.Parser.parseFile already queries that list. If we are querying this list in two places, perhaps the local go definition can be stand-alone so that it can be shared between both uses.

[vlopezj]

If this works well, we could even do away with flags altogether, and just have --html automatically behave like --html-highlight=code for .lagda.md files.

I can't think of a use case where one would want to output an HTML file from a .lagda.md file without preserving the markdown part as-is.

EDIT: Also, it makes things complicated in case A.2 and A.3, because the different files involved would need different values for --html-highlight.

[ice1000]

Getting the file type from the file extension in the backend sounds like a hacky and ugly solution for me (although it should probably work).
I'd like to store this information during parsing (we already decided the file type during lexing! Why doing duplicated work? It's gonna introduce maintain burdens).

[ice1000]

Also, I'd recommend simply change the default value of html-highlight, instead of simply remove the option and pick a behavior that we think it's the best.

TBH I think the HTML backend + lAtEx frontend is also pointless, but it's still supported, and used a lot in the tests.

Other things to be considered:

• Do we need to put all HTML backend related flags into a "topic"?
• Do we need a short version for these flags?

[vlopezj]

Getting the file type from the file extension in the backend sounds like a hacky and ugly solution for me (although it should probably work).
I'd like to store this information during parsing (we already decided the file type during lexing! Why doing duplicated work? It's gonna introduce maintain burdens).

I agree is somewhat hacky. As you say, it will parse the same string twice, which is not very elegant.
If there is somewhere obvious to store this information it could be good to put it there and reuse it.

In any case, I think that parsing the filename twice is by itself is not much of an issue, as it is a cheap operation. What is more important is that the code that derives the file type from the file name is implemented in only one place. Then, even if that code happens to be called twice on the same input, the maintenance burden for the code itself is not increased.

Also, I'd recommend simply change the default value of html-highlight, instead of simply remove the option and pick a behavior that we think it's the best.

The difficulty is that the most sensible default value would change depending on the file type (e.g. all for .agda, and code for .lagda.md). If you want to keep the flag you could add a third option (e.g. by-filetype), that allows the HTML backend to pick the best one. This (by-filetype) could be the default behaviour.

One big reason for having the --html-highlight flag was that originally we didn't want to complicate the HTML backend to detect file types. However, if the HTML backend can discern whether the input is Markdown or plain agda, there are fewer use cases for specifying html-highlight=all or html-highlight=code. The html-highlight flag hasn't been released yet, so we are still in time to remove it if we decide it's not needed.

Do we need to put all HTML backend related flags into a "topic"?
Do we need a short version for these flags?

We'll see if we have 0, 1 or 2 flags in the end :)

[ice1000]

What is more important is that the code that derives the file type from the file name is implemented in only one place.

This is what I mean by maintain burden, imagine we're gonna change the file ext parsing logic, we'll have to modify two places. We should follow the DRY (don't repeat yourself) rule in software engineering 😂

[ice1000]

If you want to keep the flag you could add a third option (e.g. by-filetype), that allows the HTML backend to pick the best one.

I like this idea!

[ice1000]

I prefer auto rather than by-filetype

[vlopezj]

I prefer auto rather than by-filetype

Agreed, auto sounds much better.

(I'll now keep playing my Apple-esque role of removing options from the user and making everything work magically).

I think the file extension should also be automatic by default, so .agda and .lagda go to .html, but
.lagda.md goes to .md. That way things will work properly in projects with a mixture of .agda and .lagda.md files.

To avoid another flag, the extension produced by the HTML back-end can also be determined by --html-highlight. For instance, --html-highlight=all always produces a .html extension, and --html-highlight=code reuses the original extension. Thus, --html-highlight=auto will have .agda, .lagda, go to .html, and .lagda.md go to .md.

This is what I mean by maintain burden, imagine we're gonna change the file ext parsing logic, we'll have to modify two places.

Right. So then we can have the parsing logic implemented only in one place (for example, the literate parsing module), and then called again on each filename from the HTML back-end. Then we could stay DRY (at least, code-wise) even if each filename is parsed more than once.

[ice1000]

but
.lagda.md goes to .md. That way things will work properly in projects with a mixture of .agda and .lagda.md files.

Don't forget we support rst as well.

[ice1000]

So then we can have the parsing logic implemented only in one place (for example, the literate parsing module), and then called again on each filename from the HTML back-end.

Yes, this sounds better to me, but I still wonder if there's some way to store the information.

We can get some extra benifits like we can use the information in Emacs mode!

[ice1000]

src/full/Agda/Interaction/Highlighting/HTML.hs:157:40: error:
    • Variable not in scope: ext :: String
    • Perhaps you meant one of these:
        ‘text’ (imported from Text.Blaze.Html5)
        ‘text’ (imported from Agda.Utils.Pretty)
        ‘exp’ (imported from Prelude)

[nad]

Does Agda save information like whether a file is a lagda file?

Adding such a field to interfaces (Agda.TypeChecking.Monad.Base.Interface) would be easy.

[nad]

TBH I think the HTML backend + lAtEx frontend is also pointless, but it's still supported, and used a lot in the tests.

I think we test these things because there isn't (yet) an easy way to turn off the HTML tests, and unlike the LaTeX tests the HTML tests run quickly, so no one has bothered to implement a way to turn them off. (And if this combination is supported, then it makes sense to test it.)

[nad]

Do we need a short version for these flags?

No?

[ice1000]

I've found the related code is really badly written, there's a lot of misleading dead codes and some possible refactoring leftovers.
I've gone through a lot of files and I think I'm very close to what I want.
This PR will also improve the maintainability of the file extension detection part -- I've refactored some existing code.

But that's all my personal opinion, I know it may not fit you guys' flavor. Maybe I have some misunderstanding of the code base. Feel free to give any suggestions, I'm very willing to learn from you.

[ice1000]

I'm gonna push a commit after my local changes passes compilation, then tweak the tests.

[ice1000]

@vlopezj Please take a look

[ice1000]

I'm not sure about this, I'm just following the pattern. I hope I'm doing it correctly.

[ice1000]

Ditto

[ice1000]

@vlopezj That's cool! Thanks

[ice1000]

Hi, I see this test failure locally:

-\\[\AgdaEmptyExtraSkip]%
-\>[0]\AgdaComment{-- A comment with some TeX ligatures:}\<%
-\\
-\>[0]\AgdaComment{-- --, ---, ?`, !`, `, ``, ', '', <<, >>.}\<%
-\\
-%
-\\[\AgdaEmptyExtraSkip]%
-\>[0]\AgdaFunction{Θ₁}\AgdaSpace{}%
-\AgdaSymbol{:}\AgdaSpace{}%
-\AgdaPrimitiveType{Set}\AgdaSpace{}%
-\AgdaSymbol{→}\AgdaSpace{}%
-\AgdaPrimitiveType{Set}\<%
-\\
-\>[0]\AgdaFunction{Θ₁}\AgdaSpace{}%
-\AgdaSymbol{=}\AgdaSpace{}%
-\AgdaSymbol{λ}\AgdaSpace{}%
-\AgdaBound{A}\AgdaSpace{}%
-\AgdaSymbol{→}\AgdaSpace{}%
-\AgdaBound{A}\<%
-\\
-%
-\\[\AgdaEmptyExtraSkip]%
-\>[0]\AgdaFunction{a-name-with--hyphens}\AgdaSpace{}%
-\AgdaSymbol{:}\AgdaSpace{}%
-\AgdaSymbol{∀}\AgdaSpace{}%
-\AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
-\AgdaSymbol{:}\AgdaSpace{}%
-\AgdaPrimitiveType{Set}\AgdaSymbol{\}}\AgdaSpace{}%
-\AgdaSymbol{→}\AgdaSpace{}%
-\AgdaBound{A}\AgdaSpace{}%
-\AgdaSymbol{→}\AgdaSpace{}%
-\AgdaBound{A}\<%
-\\
-\>[0]\AgdaFunction{a-name-with--hyphens}\AgdaSpace{}%
-\AgdaBound{ff--fl}\AgdaSpace{}%
-\AgdaSymbol{=}\AgdaSpace{}%
-\AgdaBound{ff--fl}\<%
-\\
-%
-\\[\AgdaEmptyExtraSkip]%
-\>[0]\AgdaFunction{ffi}\AgdaSpace{}%
-\AgdaSymbol{:}\AgdaSpace{}%
-\AgdaPostulate{String}\<%
-\\
-\>[0]\AgdaFunction{ffi}\AgdaSpace{}%
-\AgdaSymbol{=}\AgdaSpace{}%
-\AgdaString{"--"}\<%
-\end{code}
-Note that the code is indented.
-
-\end{document}
+LATEX_COMPILE_FAILED with pdflatex

I don't know what's happening. Can you help?

[ice1000]

Maybe it's just a problem of my installed xElAtEx. Let's see if it still occurs on CI.

[ice1000]

I see -- maybe I don't have a valid pdflAtEx. I'll install one and try later

[ice1000]

I created some tests for the command line flags. Will PR after the merge of this PR

[ice1000]

As you can see the only test failure is caused by the change of the generated file extension.
This is already fixed on a local branch.

[ice1000]

@vlopezj Please review. I see some CI already passed.
If it looks good to you, you should merge this.

[nad]

I think it makes sense to refactor the commits before merging, getting rid of commits called "Fix typo" and "Address comments".

I created some tests for the command line flags. Will PR after the merge of this PR

Please include the tests right away.

[ice1000]

Please include the tests right away.

The tests are already included in this PR. It's because this PR actually breaks existing tests (the one added in #3313), so I just moved all the test related changes here.

I'll refractor commits after you guys review this

[ice1000]

Because CI takes hours to build, I don't want to make force pushes to hide success builds

[nad]

I suggest that you run (most of) the tests locally: make test.

[ice1000]

I suggest that you run (most of) the tests locally: make test.

I run it before I commit! But CI builds are more convincing.

[vlopezj]

@ice1000 Glad to see it passes the CI build.
Can you merge the commits together then? As usual, 1-2 commits is ideal, but you can use 3-4 if you think it's necessary.

I created some tests for the command line flags. Will PR after the merge of this PR

The tests are already included in this PR.

I didn't fully understand this… Are the tests included already, or do you plan to submit more tests in a future PR?
I agree with @nad, it's better if we can merge all the tests at the same time as we merge the feature.

[ice1000]

I didn't fully understand this… Are the tests included already, or do you plan to submit more tests in a future PR?

It's included

[vlopezj]

Perfect 👍
Then I'll just wait for the refactored commits.

[ice1000]

@vlopezj I think it's fine to merge right now.

[ice1000]

Since everything is already reviewed, I consider it proper to merge it directly.