[Agda] Documentation of the (not only) latest features

[Joe M]

Hello Wojciech Jedynak,

Really liked your version of the documentation. Clears up some of the
stuff that I was confused with.

Thanks
Joe

On Mon, Jul 25, 2011 at 6:00 AM,  <agda-request at lists.chalmers.se> wrote:
> Send Agda mailing list submissions to
>        agda at lists.chalmers.se
>
> To subscribe or unsubscribe via the World Wide Web, visit
>        https://lists.chalmers.se/mailman/listinfo/agda
> or, via email, send a message with subject or body 'help' to
>        agda-request at lists.chalmers.se
>
> You can reach the person managing the list at
>        agda-owner at lists.chalmers.se
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Agda digest..."
>
>
> Today's Topics:
>
>   1. Documentation of the (not only) latest features (Wojciech Jedynak)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Sun, 24 Jul 2011 17:00:39 +0200
> From: Wojciech Jedynak <wjedynak at gmail.com>
> Subject: [Agda] Documentation of the (not only) latest features
> To: agda at lists.chalmers.se
> Message-ID:
>        <CAOtUgQQmiuzkfdaDF=qYAW3BQGoe2pWemVCfSh0Xm6W4Hg7GMw at mail.gmail.com>
> Content-Type: text/plain; charset=ISO-8859-1
>
> Hello everybody!
>
> The agenda (in case you're busy):
> 1. Agda praise
> 2. Agda documentation complaints
> 3. Sample documentation update and call for comments
> 4. A simplistic *.lagda -> pmwiki converter
>
> 1. As a newcomer to the Agda-world I am very eager to read anything
> related to it. I'm visiting
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation
> on a daily basis and I learned a lot. The materials on general
> dependent programming related techniques (that seem to apply not only
> in Agda) are simply delightful.
> The emacs-mode is so useful and brilliant, that I'm having a hard time
> coming back to Haskell :>
>
> 2. On the other hand, the documentation on the Agda language itself
> seems outdated. I often consult the Reference Manual draft on the wiki
> (http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TOC).
> It's nicely structured and very convenient to use, but it wasn't
> obvious to me that it doesn't cover many features of Agda 2.2.6+.
>
> I was pretty surprised when I saw all those new record constructors
> and irrelevant fields for records in one of the recent papers :-)
> To give another example, I would have been still pattern matching like
> crazy, if not for the kind user on the IRC channel who told me about
> the rewrite feature -- it really made a huge difference. The last
> thing is that I noticed I still only use around 12 modules from the
> standard library, because it feels complicated and kinda inaccessible.
>
> 3. OK, enough of those complaints! I wrote about these issues because
> it's possible that others had (and others-of-others will have) similar
> experiences.
> I would like to help in improving the documentation. As a sample I
> have updated and slightly restructured the records page from the
> manual:
>
> Current version:
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Records
>
> Updated draft: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ForkedReferenceManual.Records
>
> I would like to ask for any comments: isn't it too long? too informal?
> too tutorial-like?
> What is the purpose of the ReferenceManual - should total beginners be
> able to read it?
> I saw that the original authors of the page didn't use the unicode
> style so I kept it this way as it is perhaps more beginner friendly
> (hey! I was scared at first when I saw all that latex-style unicode magic:D)
> (I didn't change the copy-pasted parts from the recent-changes
> documents though).
>
> 4. In the process I decided to try to generate the wiki page
> automatically from a literate agda file.
> This way the examples would be easy to maintain and test. For this
> convertion I wrote a quick & dirty Haskell
> file. Using this approach it should be relatively painless to write
> some examples of std-lib usage as literate agda and then
> generate nice wiki pages from them. If you think it would be
> worthwhile, please say so and I'll start documenting the stuff I've
> already figured out.
>
> Here is the source *.lagda file of manual page:
> https://github.com/wjzz/Agda-docs/blob/master/Manual/Records.lagda
>
> And the converter:
> https://github.com/wjzz/Agda-docs/tree/master/Converter
> https://github.com/wjzz/Agda-docs/blob/master/Converter/README
>
> Greetings,
> Wojciech Jedynak
>
>
> ------------------------------
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
> End of Agda Digest, Vol 71, Issue 11
> ************************************
>