[Agda] Expanding literate Agda

[Pepijn Kokke]

Dear all,

I've implemented a pre-processor to "unlit" various styles of literate
code, i.e. LaTeX-style, bird tags, Markdown-style code blocks, etcetera.
I'm currently trying to integrate it into Agda. There are currently two
proposals for how to do this.

The first is the following:

Try to infer the literate format from the file, making it explicit with
> Agda command-line arguments if necessary.



This would mean that, for instance, if the "unlit" program would encounter
> a "\begin{code}" tag, it would assume the literate Agda file was was
> written in LaTeX style, if it encountered a "```" fence it would assume
> Markdown, etcetera...

(I would personally prefer that a bird tag would also indicate Markdown,
> because the two formats integrate so well and are already used in this
> manner in the Haskell community.)



The advantages of this approach is that it can easily be integrated into
> the current Agda, and all literate files would have the .lagda extension.



In the case where it is desirable to mix formats in a strange way (i.e. mix
> bird tags and LaTeX or even LaTeX blocks and Markdown blocks) command-line
> arguments could be passed to Agda explicitly stating the literate
> style---though I'm guessing this would never be necessary.


The second proposal is the following:

Each style of literate Agda would have its own extension. For instance:
> LaTeX-style would ".agda.tex", Markdown would use ".agda.md" and
> Bird-style would use ".agda.txt".



The advantages of this approach is that there is no inference needed, as
> the format will be unambiguously specified in the extension.



The problem with this approach is that it will require modifications to
> many parts of the Agda ecosystem. For instance, the code that resolves
> module names to files would have to change to also take ".agda.tex" and
> such into consideration. The same modifications would probably have to be
> made for the Emacs (and other) editing mode. This would constitute many
> (trivial) changes across the Agda codebase.


I'd like to hear your thoughts on these different approaches, or---if you
have proposals of dealing with this in a different manner---how you would
solve this problem.

Regards,
Pepijn
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141012/4d436708/attachment.html