feat: extend #whats_new to parse without in

[joneugster]

#whats_new executes all remaining commands before analysing them. This uses the built-in keyword in, so that #whats_new in keeps its current behaviour.

---

I think this would increase language consistency, but besides that, it's not yet clear to me, if this is desired, so I mark this as RFC for now...

[github-actions]

PR summary 8bfd702638

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 8bfd702).

• +1 new declarations
• −1 removed declarations

-Mathlib.WhatsNew.«command#whats_newIn__»
+Mathlib.WhatsNew.«command#whats_new__»

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 8bfd702638
Reference commit 2ed733ad3e

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[joneugster]

no, I don't think this is doing what I thought it would be doing :/

[thorimur]

Ah yeah, the issue here, as you might have realized, is that in this implementation the commands fed to #whats_new have to be parsed as arguments on the syntax level for #whats_new to control them, whereas in does not re-parse, but just runs the command before in and then runs all the ones after (in a section).

I think there's a way to achieve this with stateful linters and environment extensions... 🤔 #whats_new would store (some data about) its scope (and its syntax) in an environment extension. A linter would read that scope data and compare it to its current scope. As soon as the current scope was outside of the stored scope (or at the end of the file), log on the stored #whats_new syntax, and save a state saying that the next run of the stateful linter doesn't need to do this.

[joneugster]

yeah at that point a simple macro, instead of using the builting in, seems easier...

@[inherit_doc Mathlib.WhatsNew.whatsNewStx]
macro "#whats_new " "in" ppLine cmd:command : command =>
  `(command| #whats_new $cmd)