-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Allow .lagda
for library sources
#2379
Comments
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 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
is the killer right now for me! |
As a footnote, and in the spirit of the current status quo, two questions:
and a reference to: agda/agda#5541 |
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 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 agda/agda#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. |
'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...) |
Echoes of #595 ? (Can the issues be brought together somehow?) |
They certainly are related! |
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) |
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.The text was updated successfully, but these errors were encountered: