agda
Fix the mentions of defunct `README` modules
In Data.Nat.Tactic.RingSolver we tell people to
See README.Nat for examples of how to use this solver
But README.Nat does not exist anymore. We probably meant to point to
README.Tactic.RingSolver instead.
Ideally this kind of sanity check should be part of GenerateEverything.
And, less ideally because not machine-checkable, advice in HACKING or style-guide on checking this manually?
Or: for every module X, which mentions a README.* module, associate an additional module... X.READMEs (?) which only imports X and all the READMEs that X mentions? Can this (easily) be done automagically by GenerateEverything?
Any solution to this really ought to be automatable, otherwise it's going to grow into a nightmare.
If our source files were literate, the the reference would be a proper link, which would have broken and thus we would have known to fix it. Is that maybe the best path forward?
That would be a big upgrade in ux (making stdlib literate), but also at a big cost, not least in (working out to to trade off) the perhaps-competing forces in the design of the library?
I was thinking it would be done incrementally, i.e. simply start by allowing .lagda as input. In fact, we should take a serious look at all of the 1lab's infrastructure -- it is much nicer than stdlib's and sure seems to work well.
Suggest closing this after #2285 in favour of opening a fresh issue on README/CI?
Agreed, once there is such a fresh issue, this one should be closed.