<div dir="ltr"><span style="font-family:arial,sans-serif;font-size:13.333333969116211px">Dear all,</span><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">I&#39;ve implemented a pre-processor to &quot;unlit&quot; various styles of literate code, i.e. LaTeX-style, bird tags, Markdown-style code blocks, etcetera. I&#39;m currently trying to integrate it into Agda. There are currently two proposals for how to do this.</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">The first is the following:</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">Try to infer the literate format from the file, making it explicit with Agda command-line arguments if necessary. </blockquote><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"> </blockquote><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">This would mean that, for instance, if the &quot;unlit&quot; program would encounter a &quot;\begin{code}&quot; tag, it would assume the literate Agda file was was written in LaTeX style, if it encountered a &quot;```&quot; fence it would assume Markdown, etcetera... </blockquote><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">(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.)</blockquote><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"> </blockquote><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">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.</blockquote><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"> </blockquote><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">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&#39;m guessing this would never be necessary.</blockquote><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">The second proposal is the following:</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">Each style of literate Agda would have its own extension. For instance: LaTeX-style would &quot;.agda.tex&quot;, Markdown would use &quot;.<a href="http://agda.md">agda.md</a>&quot; and Bird-style would use &quot;.agda.txt&quot;. </blockquote><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"> </blockquote><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">The advantages of this approach is that there is no inference needed, as the format will be unambiguously specified in the extension. </blockquote><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"> </blockquote><blockquote class="gmail_quote" style="font-family:arial,sans-serif;font-size:13.333333969116211px;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">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 &quot;.agda.tex&quot; 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. </blockquote><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">I&#39;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.</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px"><br></div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">Regards,</div><div style="font-family:arial,sans-serif;font-size:13.333333969116211px">Pepijn</div></div>