Remove stale (1.x) deprecation warnings and their associated names

[silas-hw]

Any deprecation warning mentioning 'v1.x' has been removed, alongside their associated name or module, as @JacquesCarette requested. Some entire modules were removed as well if they were marked as deprecated.

This only had a few follow on breakages that needed fixing too:

• Some mentions of Algebra.Morphism.Definitions.Morphism needed to be changed to F.Carrier -> T.Carrier
• ^-semigroup-morphism and ^-monoid-morphism needed their signatures updating to use IsMagmaHomomorphism and IsMonoidHomomorphism respectively, which is also invovled needing new proofs. The former involved adding a new lemma named cong-IsRelHomomorphism and placed in a new module called Relation.Binary.Morphism.Construct.PropositionalEquality
  • The new lemma can be renamed and moved, or even in-lined, if needed

I also patched two warnings I got but I believe those were from building with the latest version of Agda as opposed to the latest release, so can revert those too if needed.

[jamesmckinna]

I think some of these changes are erroneous... I'll look at them properly in the morning.

Specifically, I think some of the exports of #2980 seem to have been reverted by this PR?

Data.List.Fresh seems to have a v1.4 warning marked as v2.4, which if correct should not be removed.

The Morphism patches seem to suggest that deprecated names had previously slipped past the warning mechanisms, and if so should be looked at carefully.

The Data.Record issue has been answered elsewhere (see #2986), and should not be patched with a LIE... in any case this PR should be run against v2.8 of Agda, not the current master branch.

A number of v2.0 PRs introduced warning suppressions in order to accommodate v1.x era deprecations, and these should be carefully revisited to see if such warning suppression is still needed.

Mildly troubling on a first skim read.

[silas-hw]

I'll revert everything I did by mistake by using 2.9 in the morning, which should only be the pattern attribute and eta equality pragma. Sorry about that.

I'l look into the v2.0 suppressions too, I was unaware of those.

In terms of #2980 I think it was just_≈?_ that was removed. On my end it seemed like there was a deprecation warning attached to it, but I may have been mistaken.

[silas-hw]

It was _≈?_ from Data.Char.Properties, and an import of that. It did have a v1.x deprecation warning, unless you mean something else @jamesmckinna ?

[jamesmckinna]

It was _≈?_ from Data.Char.Properties, and an import of that. It did have a v1.x deprecation warning, unless you mean something else @jamesmckinna ?

Well... this one is a slightly sad case of 'forgetting the lessons of history' (as stdlib maintainers/developers we are condemned to repeat them):

• Indeed, v1.x originally used the _≈?_ notation, which was then deprecated in favour of... other things
• BUT v3.0 reinstates this choice! PR [ refactor ] v2.4-admissible version of #2952 #2980 and the subsequent Update deprecation warnings in v2.4 for #2980 #3010 / [ fix ] Update deprecation warnings to v3.0 #3028 / [ fix ] more loose ends from #3010 / #3028 #3029

So, rather in the way that git itself can be very annoying in making you repeat commits when resolving merge conflicts etc., here is an annoying case where 'just' removing v1.x deprecations is unfortunately not the whole story!

Shoutout to @MatthewDaggitt and @JacquesCarette for the 'best' approach to resolving this? ideally, merging #3029 first?

[jamesmckinna]

As with some of the other items I queried (eg Data.List.Fresh), it's also probably worth looking at the blame history of each file just to try to build a mental model of what's there, and why. This may also help with the v2.0-era warning suppressions?

[jamesmckinna]

Thanks very much for this first PR, which does valuable infrastructural work.

Apologies for my initial reaction, but hopefully the review comments help explain such reactions!

[silas-hw]

Should have fixed most things, other than those more open to discussion with other maintainers.

[silas-hw]

I'll check through the suppressions and such now. Perhaps best to review after I've sorted those out too, unless it's more suitable for a separate PR.

[silas-hw]

I could only find 1 suppression hiding a 1.x warning (removed in latest commit). The rest were all hiding 2.x or 3.x warnings.

[jamesmckinna]

Let's run this, and see what comes back from testing.

• I still think that the Data.Char.Properties might need some more work.
• I'd dearly like to eliminate the Data.Nat.Properties *morphism definitions in favour of better ones UPDATED as I suspected, deleting the dprecations even makes these objects undefined, and the warnings aren't triggered because they arise from syntax declarations which don't (seem to) give rise to WARNING_ON_USE!?
• Will review again once the tests run.

[JacquesCarette]

FYI: test-stdlib failed on Function/Endomorphism/Setoid checking for the existence of IsSemigroupMorphism. But this did not fail when typechecking! Is there something different about test-stdlib's environment?

[JacquesCarette]

One minor thing - but I am otherwise happy with the state of this PR as it stands now.

[JacquesCarette]

Suggested change

	using (_≈?_;_≟_; _≡?_; _<?_; _≤?_; _≡ᵇ_) public
	using (_≈?_; _≟_; _≡?_; _<?_; _≤?_; _≡ᵇ_) public

[jamesmckinna]

And in fact, for backwards-compatibility with the v3.0 fieldname/operation name changes in #2980 we actually need also to export _==_. Sorry if that hadn't been clearer earlier in my ramblings:

Suggested change

	using (_≈?_;_≟_; _≡?_; _<?_; _≤?_; _≡ᵇ_) public
	using (_≈?_; _≟_; _≡?_; _<?_; _≤?_; _≡ᵇ_; _==_) public

This is the change I alluded to earlier under Data.Char.*... and then we can deprecate all of these 'old' names once we get to v4.0 (or even v3.999999 if we're feeling bold).

[JacquesCarette]

@jamesmckinna said:

* I still think that the `Data.Char.Properties` might need some more work.

Details? I did not see anything obvious. And for this PR or a subsequent one?

* I'd dearly like to eliminate the `Data.Nat.Properties` `*morphism` definitions in favour of better ones UPDATED as I suspected, deleting the dprecations even makes these objects undefined, and the warnings aren't triggered because they arise from `syntax` declarations which don't (seem to) give rise to `WARNING_ON_USE`!?

Subsequent PR or required here?

[jamesmckinna]

So the -morphism changes required by the now-failing tests are, I think best addressed two-fold

• for this PR, simply comment out the code (it should never have lasted this long!), but clearly the failing test code needs looking at ... UPDATED actually the redefinitions of the homomorphisms in Dat.Nat.Properties is probably the better approach on reflection, but should be documented as a Non-backwards-compatible change in the CHANGELOG, preferably with a comment under Highloights about the removal of all the old dead code?
• for a subsequent PR, we need to lift up the existing -cong and -homo proofs in Algebra.Properties.RawRing.Exp to witness actually having an IsMonoidHomomorphism of the right kind, and similarly (I think!?) Algebra.Properties.RawMagma.Mult (or Sum?) for an IsMagmaHomomorphism ...

Tragically, even the old design is Just Plain Wrong under our new approach of defining IsXHomomorphism structures on the Raw bundles of the underlying algebras X. As a consequence of which, IsSemigroupHomomorphism no longer makes any sense at all, only IsMagmaHomomorphism... and any such thing automatically will preserve any instances of assoc which happen to hold, so there's actually no way to stipulate that as 'extra structure'.

[jamesmckinna]

Regarding the failing test, remember @JacquesCarette that for Reasons (I think @gallais explained it to me, but I'm not sure I successfully internalised the explanation), we also recheck even deprecated modules as part of the testing workflow (I've been caught out by this before), as a result of which, PRs can require to edit deprecated definitions and modules in order to still typecheck OK.

The failure in Function.Endomorphism.Setoid arises from ... the concept which I observe above is no longer even well-formed, namely IsSemigroupHomomorphism. The module is deprecated, so we can simply remove the offending definition altogether, I think? But @silas-hw you'll need to add that to the list of modules touched by this PR.

The irony that this is a v2.1 deprecation is... not lost on me.