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

[Wojciech Jedynak]

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