Commit 2026-10-20 08:03 bbe3db28

feat: enable Verso if no syntax or doc-gen changes (#45031) This PR enables Verso docstrings in the 1352 files where this is possible without making any syntactical changes to the file, and the doc-gen output is identical. So we get some nice Verso features like syntax highlighting and (opt-in, because no roles are assigned yet) code checking. Note that doc-gen doesn't support Verso yet so all docstrings get converted back to Markdown before rendering in doc-gen (and indeed this PR should have the diff be exactly identical): for now you'll see Verso's features in the editor or while compiling only. This PR contains all the files from #44830 which do not show up on a diff on the doc-gen output. To replicate, follow the steps to get a doc-gen diff in #44830, and then:

• diff -rq doc-*-filtered > verso-doc-diff.txt
• Delete tactics.html from verso-doc-diff.txt
• Check out the Mathlib master branch (here commit 67013005101cbec00f56fd1bb726fe675744bb7a)
• git checkout verso-migrate-identical -- .
• < verso-doc-diff.txt sed 's|^Files doc-master-2026-10-13-filtered/(.).html and.$|\1.lean|' | xargs git restore --staged
• git commit