I have been working on a LaTeX-backend which does precise syntax highlighting (like the HTML-backend) and code alignment using the polytable package (like lhs2TeX).

Here is a sample input and output file:

https://personal.cis.strath.ac.uk/stevan.andjelkovic/LaTeXBackend.lagda https://personal.cis.strath.ac.uk/stevan.andjelkovic/LaTeXBackend.pdf

There are still some rough edges which needs to be fixed. I was hoping to work on this (possibly with others) during the AIM week. I can't be there in person, but I'd happily collabortate over IRC -- that's why I'm attaching what I got so far in here.

Some problems I know of:

• Empty \begin{code} \end{code} blocks cause problems, and the current hack with isReallyEndCode isn't nice nor working properly. Perhaps it's better to modify the parser to give those tokens a special status (making them not be grouped together with comments).

• Agda.fmt could probably be improved by somebody who knows LaTeX.

• Alignment and indenting fails sometimes (even though the output LaTeX code is very similar to the output of lhs2TeX.) This could be missing polytable code, or missing code environment bits in Agda.fmt (currently have I just stolen some bits from lhs2TeX, without knowing what they do).

Possible extensions:

• Inference rule style pretty printing of datatypes.

• Links to definitions a la HTML-backend?

• ...

currently have I just stolen some bits from lhs2TeX

lhs2TeX is GPL-ed, and Agda is not, so please don't use any lhs2TeX code.

An alternative would be to write a stand-alone program, and invoke Agda as a library.

By the way, something like this seems potentially very useful!

Have you thought about formatting of code snippets embedded in regular text?

lhs2TeX is GPL-ed, and Agda is not, so please don't use any lhs2TeX code.

To clarify; only Agda.fmt uses bits from lhs2TeX. This is just tex code used to define the code environment and it's not GPLed:

https://github.com/kosmikus/lhs2tex/blob/5dfc54070d893baf7ae71c0620097ce76f4b56a6/LICENSE

But like I said, while it seems to (mostly) work, it should probably be rewritten by somebody who understands it anyways.

Have you thought about formatting of code snippets embedded in regular text?

The backend only formats typechecked code (using the highlighting info produced by the typechecker). Snippets can be manually formatted using the predefined latex commands from Agda.fmt. I updated the sample files above to show an example of this.

I don't think it's worth the trouble trying to make the backend do this at this point -- because I don't see a simple solution and it doesn't save that much work. I think a better long term solution would be to make literate Agda be able to typecheck snippets somehow...

Stevan, the exception just grants you the right to "include the files [...] literally in other documents [...]". I don't think this patch should be applied as long as Agda.fmt is part of it. Unless, of course, you get agreement from the lhs2TeX copyright holders.

Comment deleted

IANAL, but FWIW, my intention was certainly that it should be possible to use Agda.fmt as done here.

If it's still a problem, here is a patch which removes everything taken from lhs2tex. The output doesn't look as good, but I'm sure somebody who knows latex (and hasn't looked at the lhs2tex code) can fix this in a matter of minutes.

Attaching a new patch, here are the changes:

• Begin/end code block should now be robust.

• Removed lhs2tex code from Agda.fmt, renamed it into agda.sty.

• \usepackage{agda} should now be used instead of \input{Agda.fmt}.

• If this package isn't found by the LaTeX environment, then a default version is copied in from Agda's datadir into the current dir.

• Alignment and indentation seems to work, even though the indentation code is a bit messy.

• Data.Text is used instead of strings

• Added release notes.

Could it be made a branch of hub.darcs.net/ulfnorell/Agda ?

Is this ready to be tested and pushed?

I think so. I been using it for a couple of days and it seems to work.

Some comments:

• This looks very promising!

• Please include a complete (but small) example in the release notes, including comments describing the features you've implemented. I think the description should be moved to "Tools" (you can create a new section for it).

• The alignment feature seems to insert extra, unnecessary white space.

• Add one or more test cases.

• Please add the following code to checkOpts:

  | not (atMostOne $ interactive ++ [optGenerateLaTeX]) = Left "Choose at most one: --latex/--interactive/--interaction.\n"

• Does --latex apply to all files, or only to the top-most one? This isn't clear from your documentation.

• Should --latex require that all (or the top-most) file is a .lagda file?

• Can you provide a cut-down agda.sty which is more tool-agnostic? I think I'd like to use this feature with XeLaTeX (which has better support for Unicode).

• Some more space above and below the (formatted) code blocks would be nice.

• I think we should add a flag --latex-dir.

• Why does agda --latex Test.lagda (sometimes?) print "./agda.sty"?

• Identifiers are not hyperlinked. Is this intentional? Optional, optionally invisible hyperlinking might be nice. ( "What is this strange symbol supposed to mean? I don't think I've seen it before." "Oh, it was defined on the previous page.")

• It seems as if >>= is typeset somewhat strangely.

• It's nice that underscores are handled straight out of the box. When you write something like ⊙⟦, are you sure that the same amount of whitespace is used between _ and ⊙ as between ⟦ and _?

• Perhaps it would also be nice to add support to --html/--latex/--dependency-graph to the Emacs mode (but not in this patch).

Another tweak: text == 0.11.* seems to work on GHC 7.6.

• The alignment feature seems to insert extra, unnecessary white space.

Yes, this happend after I removed the lhs2tex bits from agda.sty. I think it's related to how polytable works. I don't know how to fix it.

• Does --latex apply to all files, or only to the top-most one? This isn't clear from your documentation.

Only the top-most one -- like lhs2tex and unlike the HTML backend. To me it doesn't make sense to latex 30 modules of the standard library just because you import Data.Vec or whatever.

• Should --latex require that all (or the top-most) file is a .lagda file?

It requires the top-most file to be literate Agda. The idea is that you pass the output to latex, so it has to have \begin{document} etc in it.

• Can you provide a cut-down agda.sty which is more tool-agnostic? I think I'd like to use this feature with XeLaTeX (which has better support for Unicode).

Sorry, but what part of it is tool specific?

The \DeclareUnicodeCharacters should be sent upstream to the ucs package maintainer, I'll do that once I compiled a list of characters which often occure.

• Some more space above and below the (formatted) code blocks would be nice.

The idea is that you should be able to tweak things in agda.sty to your taste. I think you can change the code environment code to achieve this.

• Why does agda --latex Test.lagda (sometimes?) print "./agda.sty"?

The latex backend checks if agda.sty is available to the latex environment, by calling:

rawSystem "kpsewhich" [ defaultStyFile ]

If it isn't then the default agda.sty is copied to the current directory from Agda's data-dir. The idea being that if you don't like the default formatting you can keep your own agda.sty on the system, perhaps with more spacing around code blocks or perhaps using less colours than the default one.

I added some additional output to make this more clear.

• Identifiers are not hyperlinked. Is this intentional? Optional, optionally invisible hyperlinking might be nice. ( "What is this strange symbol supposed to mean? I don't think I've seen it before." "Oh, it was defined on the previous page.")

I don't think this makes sense. What if you import things from the standard library and you don't want the standard library as an appendix to your document? Even if you try to only hyperlink things that are in scope or something like that, you still got the following problem. If you want to define things, but hide them in the document, e.g.:

\AgdaHide{ \begin{code} module M where \end{code} }

\begin{code} open M \end{code}

Where is M hyperlinked to?

• It seems as if >>= is typeset somewhat strangely.

You will want to do some postprocessing off the output. lhs2tex has a default %format rule for bind:

\newcommand{\bind}{\mathbin{>!!!>\mkern-6.7mu=}} %format >>= = "\bind "

But there are plenty other things you will want to postprocess:

⟦⟧Type into ⟦⟧{Type} Γ ⊢ Σ ‿ t ∶ T into Γ ⊢{Σ} t ∶ T apa^[bepa] into apa^{bepa} etc

I think I'll just use perl for this, but I can see how a simpler interface a la %format might be useful. Not sure how to provide a simpler interface that is as flexible as perl regexes though.

• It's nice that underscores are handled straight out of the box. When you write something like ⊙⟦, are you sure that the same amount of whitespace is used between _ and ⊙ as between ⟦ and _?

I don't know, try? Nothing special is done to underscores, they are just escaped.

• Perhaps it would also be nice to add support to --html/--latex/--dependency-graph to the Emacs mode (but not in this patch).

Not sure I understand what that means.

• Please include a complete (but small) example in the release notes, including comments describing the features you've implemented. I think the description should be moved to "Tools" (you can create a new section for it).

Fixed.

Once I figure out how to use it properly to produce (modular) documents, I will write a short tutorial.

• I think we should add a flag --latex-dir.

Fixed.

• Add one or more test cases.

Fixed, not sure if it passes though -- make test doesn't seem to work?

• Please add the following code to checkOpts:

  | not (atMostOne $ interactive ++ [optGenerateLaTeX]) = Left "Choose at most one: --latex/--interactive/--interaction.\n"

Fixed.

• Another tweak: text == 0.11.* seems to work on GHC 7.6.

Fixed.

Yes, this happend after I removed the lhs2tex bits from agda.sty. I think it's related to how polytable works. I don't know how to fix it.

Perhaps you could ask Andres.

Sorry, but what part of it is tool specific?

At least ucs (including \DeclareUnicodeCharacter), fontenc and inputenc.

• Some more space above and below the (formatted) code blocks would be nice.

The idea is that you should be able to tweak things in agda.sty to your taste. I think you can change the code environment code to achieve this.

I think the default should be changed. The current (or at least former) default puts the code write after the preceding text, which IMO is ugly.

The latex backend checks if agda.sty is available to the latex environment, by calling:

rawSystem "kpsewhich" [ defaultStyFile ]

I suggest that you use some other procedure which does not print anything on stdout/stderr.

I don't think this makes sense. [...] Where is M hyperlinked to?

In this case I would probably not want to include a link. I don't know how hard it is to support this behaviour, though.

• It seems as if >>= is typeset somewhat strangely.

You will want to do some postprocessing off the output.

What I meant was that the >> part of bind looked strange: the bounding boxes of the two characters overlap. I see now that this is caused by the use of \textsf.

• It's nice that underscores are handled straight out of the box. When you write something like ⊙⟦, are you sure that the same amount of whitespace is used between _ and ⊙ as between ⟦ and _?

I don't know, try?

I suspect that the answer is no, but I'm not quite sure.

• Perhaps it would also be nice to add support to --html/--latex/--dependency-graph to the Emacs mode (but not in this patch).

Not sure I understand what that means.

It might be nice to be able to produce the .tex file using an Emacs command.

Sorry, but what part of it is tool specific?

At least ucs (including \DeclareUnicodeCharacter), fontenc and inputenc.

It would make things less usable out of the box for people who just got normal latex? Is it possible to include those things depending on what latex environment is used? Something like:

if (DEFINED XeLaTeX) ; else \usepackage{ucs}, etc ?

• Some more space above and below the (formatted) code blocks would be nice.

The idea is that you should be able to tweak things in agda.sty to your taste. I think you can change the code environment code to achieve this.

I think the default should be changed. The current (or at least former) default puts the code write after the preceding text, which IMO is ugly.

I have not experienced this, but then I haven't used it much yet.

The latex backend checks if agda.sty is available to the latex environment, by calling:

rawSystem "kpsewhich" [ defaultStyFile ]

I suggest that you use some other procedure which does not print anything on stdout/stderr.

I think it's better with the output I just added (it's more clear what is going on -- rather than things happening silently in the background).

I don't think this makes sense. [...] Where is M hyperlinked to?

In this case I would probably not want to include a link. I don't know how hard it is to support this behaviour, though.

It's hard to know if the user has hidden things away (as there are several ways of doing this).

--

Anyways, I think I will leave it there for now -- I need to write a report, and the current implementation seems sufficient for the purpose.

I'm aware of the shortcomings, and it's good that they have been recorded here in the tracker -- I'll try to fix them over time and meanwhile I welcome others to help out!

Is it possible to include those things depending on what latex environment is used?

Probably. This can be fixed later.

I think the default should be changed. The current (or at least former) default puts the code write after the preceding text, which IMO is ugly.

I have not experienced this, but then I haven't used it much yet.

Perhaps you don't include code in your paragraphs. I \begin{code} do : note \end{code} the omission of blank lines around the code block.

If you plan to change agda.sty in backwards-incompatible ways in the future, then this should perhaps be documented.

I think it's better with the output I just added (it's more clear what is going on -- rather than things happening silently in the background).

You should at least abide by -v0. Perhaps you can use Agda.Compiler.CallCompiler.callCompiler.

I think the default should be changed. The current (or at least former) default puts the code write after the preceding text, which IMO is ugly.

I have not experienced this, but then I haven't used it much yet.

Perhaps you don't include code in your paragraphs. I \begin{code} do : note \end{code} the omission of blank lines around the code block.

I see, I haven't used it this way.

If you plan to change agda.sty in backwards-incompatible ways in the future, then this should perhaps be documented.

I can't see how backwards-compatibility can be broken by changes in agda.sty, but I added a disclaimer in the release notes anyways.

I think it's better with the output I just added (it's more clear what is going on -- rather than things happening silently in the background).

You should at least abide by -v0. Perhaps you can use Agda.Compiler.CallCompiler.callCompiler.

Thanks for the tip, fixed.

I've pushed your patch. Please open new tickets for any outstanding issues.