nightly#180 adaptations for nightly-2026-02-16-rev1

Stream: nightly-testing

[Kim Morrison :bot:]

chore: adaptations for nightly-2026-02-16-rev1 nightly#180

Please review this PR. At the next toolchain release this diff will land in 'master'.

(This message wasn't posted automatically because of a SIGPIPE bug in create-adaptation-pr.sh — see #35434 for the fix.)

[Kim Morrison]

This is the insane 3000+ file PR that adds set_option backward.isDefEq.respectTransparency false where needed after lean#12179.

[Kim Morrison]

I'm working on making the git history inspectable.

Step 1. squash it all into one commit! b1638f2181cbf354d0502152a3600eb8cf99faaa
Step 2. insert the history of the lean-pr-testing-12179 branch underneath that commit in a rebase
Step 3. hopefully not mess up the rebase conflicts...

[Kim Morrison]

Okay, the git history now reflects the history from lean-pr-testing-12179.

There are lots of manual commits, that ideally would be reviewed.

There are two big commits, both labelled x: ./fix_backward_defeq.py, which are automatically generated and should consist solely of adding lines set_option backward.isDefEq.respectTransparency false in.

And then https://github.com/leanprover-community/mathlib4-nightly-testing/pull/180/commits/5643160dcddd2b50ff488ec0ed1e44bb7fde404e is "everything else" in this PR that was not on lean-pr-testing-12179. (And LGTM: it's just set_options on stuff added to master after lean-pr-testing-12179 was completed.)

[Kim Morrison]

Kim Morrison said:

There are two big commits, both labelled x: ./fix_backward_defeq.py, which are automatically generated and should consist solely of adding lines set_option backward.isDefEq.respectTransparency false in.

Well, I didn't get this exactly right, but the violations are minor. This script reports the following harmless violations of the rule.

[Kim Morrison]

And so the diffs that still need review are

• https://github.com/leanprover-community/mathlib4/compare/a4e165b66acf5ab6885a6626761038fa1481a7a8...56c60f6c08bae0f2993a09a6fe520930ed43595d
  and

• https://github.com/leanprover-community/mathlib4/compare/1cb8bd3125e325528b17bfdc074b2658875dcbce...c3881bfbbaed0330d031701f7265bf80e073fed0

[Kim Morrison]

And those look fine, except that I need to add another commit deleting the fix_backward_defeq.py script, which probably should be salvaged and turn into something general, because it is kind of awesome that it managed to automatically edit 1000s of files in Mathlib, managing all the rebuilds necessary.

Oh, and that I am opinionated about whitespace in some non-standard ways. :woman_shrugging:

[Kim Morrison]

Note that I have removed some @[simp]annotations which are both not used in the Mathlib, and which the simpNF linter now complains about.

[Kim Morrison]

Okay, I am happy with this. I am going to start cutting v4.29.0-rc1, and will plan to merge this, if it hasn't already been, in time for it to be ready for Mathlib to move over.

[Johan Commelin]

I reviewed everything except the two big auto-generated commits.

[Johan Commelin]

My takeaways:

• Adding and removing the script could have been transient: commits
• It would be great if there was a script that confirmed that a certain range of commits did nothing but add lines that start with set_option yayayada false + optional in + optional -- comment.
• All the changes that are not of the above form look good to me.
• Except that one simp seems to be removed without adaptation note.

[Kim Morrison]

• Except that one simp seems to be removed without adaptation note.

Can you help me find that one?

[Kim Morrison]

Johan Commelin said:

• It would be great if there was a script that confirmed that a certain range of commits did nothing but add lines that start with set_option yayayada false

See above, there's a script in a gist for doing this (at least the inflexible version with no comment)

[Johan Commelin]

Aah, nice. I suppose we could try to generalize the x: framework to make it possible to run such scripts as part of CI. But maybe that's over-complicating a framework that doesn't even work correctly right now.

[Johan Commelin]

Kim Morrison said:

• Except that one simp seems to be removed without adaptation note.

Can you help me find that one?

https://github.com/leanprover-community/mathlib4-nightly-testing/pull/180#discussion_r2815363611

[Kim Morrison]

Johan Commelin said:

Kim Morrison said:

• Except that one simp seems to be removed without adaptation note.

Can you help me find that one?

https://github.com/leanprover-community/mathlib4-nightly-testing/pull/180#discussion_r2815363611

It already has an adaptation note a few lines higher.

[Kim Morrison]

Johan Commelin said:

Aah, nice. I suppose we could try to generalize the x: framework to make it possible to run such scripts as part of CI. But maybe that's over-complicating a framework that doesn't even work correctly right now.

These x: commits would certainly not be reproducible in CI. They took many hours on much faster machine.

[Kim Morrison]