[Agda] Expanding literate Agda

[João Paulo Pizani Flor]

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.

But I also think "double extensions" should be avoided, and one reason for
avoiding them is that external tools might get (very) confused.

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.

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).
Even though we control the "official" Emacs mode, forcing these extension
<-> filetype associations upstream to other tools would be too much effort.

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.

Sorry for bikesheding,

João Paulo Pizani Flor, M.Sc <j.p.pizaniflor at uu.nl>
Promovendus - Departement Informatica
Faculteit Bètawetenschappen - Universiteit Utrecht

On Mon, Oct 13, 2014 at 10:01 AM, Andreas Abel <abela at chalmers.se> wrote:

> 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.
>
> .lagda should be reserved for latex-agda, and we can have new extensions
> for other literate Agda variants.
>
> 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.
>
> From https://code.google.com/p/agda/issues/detail?id=508#c10
>   I would like to see different flavors of literate Agda have distinct
> file extension, such that no guessing is needed.  Maybe:
>
> .agda.tex -- for LaTeX-style
> .agda.md -- for markdown style
> .agda.txt  -- for Bird-style
>
> I am not sure if having a double extension is a good idea, though.  Maybe
>
> .agda-tex
> .agda-md
> .agda-txt
>
> instead?
>
> In general, agda-* could be reserved for a version of literate Agda.
>
> Cheers,
> Andreas
>
> On 13.10.2014 06:55, Ulf Norell wrote:
>
>> I'm also in favour of the first solution. Using double extensions is not
>> really standard practice and might confuse both users and tools. Also,
>> it sounds like inferring the format won't be that hard.
>>
>> / Ulf
>>
>> On Sun, Oct 12, 2014 at 11:51 PM, Andrés Sicard-Ramírez
>> <asr at eafit.edu.co <mailto:asr at eafit.edu.co>> wrote:
>>
>>
>>     On 12 October 2014 06:28, Pepijn Kokke <pepijn.kokke at gmail.com
>>     <mailto:pepijn.kokke at gmail.com>> wrote:
>>
>>         Try to infer the literate format from the file, making it
>>         explicit with Agda command-line arguments if necessary.
>>
>>
>>     +1
>>
>>
>>     --
>>     Andrés
>>
>>     _______________________________________________
>>     Agda mailing list
>>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>     https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141013/c870b85f/attachment.html