agda
Port two Endomorphism submodules over to new Function hierarchy
Closes #2299
Needed to add some missing declarations in Algebra.Morphism.Structures to make it all go through.
Can we separate this PR out into a two parts, a set of backwards compatible changes, and a set of non-backwards compatible changes and then we can evaluate from there?
Sure. But I've never worried much about backwards compatibility, so I'm entirely sure which ones those are! I'd appreciate a little bit of guidance, and then I will do that.
Gah, I can't believe I missed these.
I think it's not so surprising, given that explicit pragmas had been inserted precisely to suppress the deprecation warnings... (hint: sometimes necessary, but probably harmful overall...)
In any case, the push to close #759 (before the v2.0 release) had been sufficiently effortful that there were bound to be 'loose ends'.
This one, in any case, only emerged when I started wanting to thinking about Endo at the Setoid level... I think it often requires change in one place to 'provoke' reconsideration of older decisions, so we shouldn't feel too bad about that?
The question remains: what should this PR actually look like? I'm having a hard time seeing the 'two parts' clearly, for some reason.
And yeah, there's a very high cost to having pragmas to suppress deprecation warnings. I would be more tempted to filter them out post-facto rather than with 'global' pragmas. [If we had more precise pragmas, that would work too.]
Re: @MatthewDaggitt 's "non-backwards compatible", I'm having trouble seeing what is such about @JacquesCarette 's "undeprecation" strategy. Or is something else going on that I have missed?
Hmm so in summary, I think the only reasonable way of doing this in a backwards compatible manner would be to create entirely new modules (I would tentatively suggest Function.Endomorphism.(Setoid/Propositional).New?) with the new definitions. Then in v3.0 we'll delete the current modules, and then switch the new ones in.
Suggested alternative: Call the new module/modules Endo.{Setoid|Propositional}? (and avoid the awful .New subhierarchy?)
Ok, this now should be backwards compatible! If you could re-review @MatthewDaggitt and @jamesmckinna ?
I think this now deals with all the comments from @jamesmckinna and @MatthewDaggitt and is no longer breaking either.
Looks good to me now! The HTML index run has failed... but hopefully that's a transient bug...
It's actually not - it is failing because of warnings. A deprecated module isn't allowed to use deprecated things lest warnings get issued. I had removed the warning suppression, sigh. Will have to restore it.
[This is probably something to file upstream - deprecated modules should be allowed to use other deprecated things, there is no need for a cascade of warnings!]
It's actually not - it is failing because of warnings. A deprecated module isn't allowed to use deprecated things lest warnings get issued. I had removed the warning suppression, sigh. Will have to restore it.
[This is probably something to file upstream - deprecated modules should be allowed to use other deprecated things, there is no need for a cascade of warnings!]
Two or three reactions to this:
- suppressing warnings in a deprecated module seems harmless, if annoying that it should prove necessary
- that it now does so is/seems to be a knock-on consequence of #2224 although the check on deprecated modules claims to ignore warnings... ~~, so is the list broken in some way?~~ during CI (but not during interactive development under
emacs;-)) - ~~maybe a clue to have (yet) another go at overhauling our CI ...?~~ UPDATED: no, you simply need to add
This module is DEPRECATED.to the module header(s)...GenerateEverything.hs:
-- based on detected comment in header
deprecated = let detect = List.isSubsequenceOf "This module is DEPRECATED."
in any detect hd
Re: #2394 See this commit for the details: easily incorporated on top of what you have here!
UPDATED: the only question in my mind would be whether or not in this PR to use the cong/homo names you have chosen, or else to choose 'proxy' names, ahead of them being replaced by their Algebra.Properties.* counterparts...
UPDATED: pushed that commit, so now there might be some tidying up to do (comparing Propositional, defining _^_ via flip _×_, whereas Setoid does it explicitly with arguments; retaining your names in Setoid, as above...) but whatever else should now be largely cosmetic?
I think the names are fine as they are (for the purposes of porting this). Made minor tweaks, but I think once the build comes back green, it can be merged.