<div dir="ltr"><div><div><div><div>First of all, I really like the idea of having different flavors of literate Agda (besides only LaTeX). It will be really useful for people writing blog posts, online documentation, etc. Thanks to those implementing it.<br><br></div>But I also think "double extensions" should be avoided, and one reason for avoiding them is that external tools might get (very) confused.<br><br>Text editor, standalone highlighters, plugins for CMS's, all of these tools that now assume that ".{,l}agda = Agda" and ".tex = TeX" will have to change their assumptions.<br><br></div>It would be interesting, for example, that Literate Agda in LaTeX style is shown in a text editor with Agda highlighting. If "double extensions" are adopted, then a text editor might see the ".tex" extension, ignore what comes before, and show only TeX highlighting (ignoring the possibility of highlighting the Agda fragments).<br></div>Even though we control the "official" Emacs mode, forcing these extension <-> filetype associations upstream to other tools would be too much effort.<br><br></div>So, I think Agda should either leave ".lagda" as meaning "literate Agda" in a broad sense (with all possible styles of code blocks), or, have different extensions for each code block style, but which DO NOT conflict with widespread existing filetypes.<br><div><br><div>Sorry for bikesheding,<br></div><div><div><div><div><div><div class="gmail_extra"><br clear="all"><div><div dir="ltr"><div><div>João Paulo Pizani Flor, M.Sc <<a href="mailto:j.p.pizaniflor@uu.nl" target="_blank">j.p.pizaniflor@uu.nl</a>><br></div>Promovendus - Departement Informatica<br></div>Faculteit Bètawetenschappen - Universiteit Utrecht<br></div></div>
<br><div class="gmail_quote">On Mon, Oct 13, 2014 at 10:01 AM, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I am against overloading a file extension like .lagda. I do not see why it is necessary. Since file extensions can be longer than 3 characters (as it was in good old DOS times), we do not have to be frugal.<br>
<br>
.lagda should be reserved for latex-agda, and we can have new extensions for other literate Agda variants.<br>
<br>
Note that inferring the file format also has to be implemented for the emacs-mode and all other front-ends to Agda. I shortage of (willing) emacs-lisp programmers in our team, I'd like to avoid anything that complicates the emacs-mode.<br>
<br>
>From <a href="https://code.google.com/p/agda/issues/detail?id=508#c10" target="_blank">https://code.google.com/p/<u></u>agda/issues/detail?id=508#c10</a><br>
I would like to see different flavors of literate Agda have distinct file extension, such that no guessing is needed. Maybe:<br>
<br>
.agda.tex -- for LaTeX-style<br>
.<a href="http://agda.md" target="_blank">agda.md</a> -- for markdown style<br>
.agda.txt -- for Bird-style<br>
<br>
I am not sure if having a double extension is a good idea, though. Maybe<br>
<br>
.agda-tex<br>
.agda-md<br>
.agda-txt<br>
<br>
instead?<br>
<br>
In general, agda-* could be reserved for a version of literate Agda.<br>
<br>
Cheers,<br>
Andreas<span class=""><br>
<br>
On 13.10.2014 06:55, Ulf Norell wrote:<br>
</span><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">
I'm also in favour of the first solution. Using double extensions is not<br>
really standard practice and might confuse both users and tools. Also,<br>
it sounds like inferring the format won't be that hard.<br>
<br>
/ Ulf<br>
<br>
On Sun, Oct 12, 2014 at 11:51 PM, Andrés Sicard-Ramírez<br></span><span class="">
<<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a> <mailto:<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>>> wrote:<br>
<br>
<br>
On 12 October 2014 06:28, Pepijn Kokke <<a href="mailto:pepijn.kokke@gmail.com" target="_blank">pepijn.kokke@gmail.com</a><br></span><span class="">
<mailto:<a href="mailto:pepijn.kokke@gmail.com" target="_blank">pepijn.kokke@gmail.com</a><u></u>>> wrote:<br>
<br>
Try to infer the literate format from the file, making it<br>
explicit with Agda command-line arguments if necessary.<br>
<br>
<br>
+1<br>
<br>
<br>
--<br>
Andrés<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br></span>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><span class=""><br>
<br>
<br>
<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br>
</span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a></font></span><div class="HOEnZb"><div class="h5"><br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div></div></div></div></div></div></div></div>