Allow `.lagda` for library sources

[JacquesCarette]

Note: I don't mean mandate, I mean allow. So the library sources would become a mixture of .agda and .lagda (which is a bit of a pain, I know.)

Basically, I'm quite jealous of the 1lab and just how wonderful its internal documentation is. We need to give ourselves the power to do the same, and I don't think that using plain .agda file does that. Of course people can still write documentation, it's just not as nice. We need an environment that encourages it even more.

[jamesmckinna]

Aaaargh! (as a third option, beyond/beside/besides either "yes" or "no"...)

My instincts are to agree (but I've had no exposure to 1lab, despite your propagandising on its behalf), but in practice I seem to find writing .lagda horrible unless I really need to write a paper, and then I find writing the Agda interferes with writing the paper (we still don't seem to have proper Knuth-like 'weaving' literate-ness, unless that's my boundless ignorance talking again)... and I haven't experimented with the .md/.lagda.md alternatives.

My principal concern is not to let writing Agda for the library be 'burdened' by the desire, or need, to write commentary.

I hate what I am about to say, but in order to make any decision/progress on this, some honest like-for-like comparison of specimen modules (pre-existing, if that helps) needs to be done, and by more than one person, in order to get a sense of what might be 'best-of-breed' (given that once such a choice is made, that basically makes it de facto for everyone else downstream, and then social/community effects take over...)... and for me at the moment, inertia trumps experimentation (I've got PRs I want merged, and more on the way... ;-))

@JacquesCarette can you write something about why you like 1lab better than... anything else, say? And, if you can, attempt to marshal some dispassionate pro/contra points about it? And, FTR, I'm willing to be persuaded, but your

(which is a bit of a pain, I know.)

is the killer right now for me!

[jamesmckinna]

As a footnote, and in the spirit of the current status quo, two questions:

• why do we not permit 'long' comments {- ... -} in stdlib modules?
• why do existing 'literate' approaches privilege text over code? (given that, with a sufficiently expressive type system, we might imagine shifting that ... inclination... in the other direction)

and a reference to: https://github.com/agda/agda/issues/5541

[JacquesCarette]

I learned what displayed categories are by reading the code. The documentation is a work of art. (And has kept that style up with multiple authors.)

In fact, it uses .lagda.md which I have yet to work with myself. I need to try.

I completely agree, writing commentary should be entirely optional for the library. And the desire of some (like me) to write more should indeed not burden others with extra overhead. I agree that 'solutions' that increase that burden are not acceptable.

Why do I like the 1lab? Because the authors go out of their way to explain things - what they are doing, some of the design decisions, some intuitions, etc.

I definitely don't know why long comments are not allowed. And I think literate approaches privilege text as a subtle encouragement! In the sufficiently long run, the text will actually matter more than the code (but we're talking decades here - comes from my experience working on 20 year old code where the principals were all out of the picture).

Unsurprisingly, (as https://github.com/agda/agda/issues/5541 points out) I'm not the first to think about this. Maybe the topic should be 'Allow literate Agda sources' as I don't really care which mechanism is used.

[jamesmckinna]

'Allow (more) literate Agda sources'?

Lots of good points!

I would really like a survey of the possible mechanisms for enhanced documentation... it really feels as though we still fall far short of what Knuth originally conceived.

And as for code vs. text, I think I (still) believe that the 'self-documenting' (sic) nature of dependent types, despite the reality not quite living up to the slogan, sees me wanting the balance to go the other way (not least because ... marked-up documentation, in whatever form, will always needs post-processing, so I'd be happy for that to all be put into long comments, and leave the code to stand alone, without explicit bracketing...)

[jamesmckinna]

Echoes of #595 ? (Can the issues be brought together somehow?)

[JacquesCarette]

They certainly are related!

[Taneb]

The big difference between this and #595, as I see it, is that this issue is about setting up infrastructure to enable easier documentation. Not actually writing any documentation (yet)