Adapt to https://github.com/rocq-community/micromega-plugin/pull/1 (tify)

[fajb]

PR rocq-community/micromega-plugin#1 generalises zify by tify T where T is a target type.
zify is therefore almost tify Z.

The PR removes introduced warnings and introduces a tify subcomponents.
It contains the existing Zify* files but could be complemented by Rify.v, Qify.v etc

Overlays (to be merged before the current PR)

• Prepare for https://github.com/rocq-prover/stdlib/pull/251 (micromega, tify) rocq#21842
• TODO coqutil
• TODO bedrock2

Overlays (to be merged in sync with the current PR)

• [tify] generalises [zify] for an arbitrary type. rocq-community/micromega-plugin#1
• Adapt to https://github.com/rocq-prover/stdlib/pull/251 equations#712
• proux01/itauto@4a3fd7c
• Adapt to https://github.com/rocq-prover/stdlib/pull/251 MetaRocq/metarocq#1264
• Adapt to https://github.com/rocq-prover/stdlib/pull/251 LPCIC/coq-elpi#998
• Adapt to https://github.com/rocq-prover/stdlib/pull/251 smtcoq/smtcoq#166
• Adapt to https://github.com/rocq-prover/stdlib/pull/251 impermeable/coq-waterproof#234

[SkySkimmer]

This makes stdlib incompatible with all released versions of rocq

[fajb]

Yes. What is the workaround?

• If the stdlib is not modified, the rocq ci fails because of deprecation warnings
• If the stdlib is updated, this uses things which did not exist

What I see possible is

• Do not generate deprecation warnings
• Do not update the stdlib

This is slow.

[SkySkimmer]

If the stdlib is not modified, the rocq ci fails because of deprecation warnings

Really? Deprecation warnings should not be fatal though.

[proux01]

Yes, we won't be able to merge this until long. I'm offering a solution.

[fajb]

From what I recall, at least the test-suite checks for the exact results. Warnings makes this fail.

[SkySkimmer]

Locally disable the warning then

[fajb]

Ok, I see. I can try to do that.

[andres-erbsen]

My opinion is that we should merge this instead of accruing technical debt to support unexpected combinations of rocq and stdlib. I raised this concern here when the stdlib split was proposed.

[andres-erbsen]

Is this failure also due to compat somehow?

Run NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "stdlib"
...
[at-level-200-changed,deprecated-since-9.3,deprecated,default]
...
File "./micromega/Tify.v", line 14, characters 13-26:
Error: The reference tify_elim_let was not found in the current environment.

[fajb]

I silenced globally the zify warnings.

When this is deemed the right time, the stdlib can enable them.

[SkySkimmer]

Global seems far too aggressive, please keep warning manipulation local.

[fajb]

I don´t thing you can because otherwise each call to e.g. lia will be cluttered with warnings.
Removing the warnings means updating the stdlib in an incompatible way.

PS: Another option, no deprecation warnings in the tify PR (for now). When things stabilise, enable them.

[SkySkimmer]

That sounds like the warning is badly implemented.

[SkySkimmer]

I guess it's a similar problem as rocq-prover/rocq#21877 where the warning should be at intern time not interp time.