why `whatsnew`?

Stream: lean4

[Asei Inoue]

why whatsnew command is not defined with name #whatsnew?
this seems to be a diagnostic command.

[Asei Inoue]

I have many times typed #whatsnew and got a syntax error. I just can't remember it.

[Damiano Testa]

I suspect that this is because whatsnew is a fairly "old" command, that might have been initially meant for debugging only (maybe?) and possibly before there was a convention of prefixing commands with #.

[Joachim Breitner]

Note that not all commands are prefixed with # - after all, def is a command. The rule tbst I once heard is that commands that don't change the environment get a # (e.g. #eval, #print)

[Asei Inoue]

is PR welcome?

[Mauricio Collares]

In general, PRs to core are not welcome unless a RFC issue is opened first and it core developers comment positively on it. There are exceptions to the rule, though.

[Asei Inoue]

OK. I will open an issue

[Asei Inoue]

In general, PRs to core are not welcome

whatsnew is in Mathlib

[Asei Inoue]

I guess you could ask on Zulip if we could rename whatsnew command to #whatsnew.

[Kyle Miller]

@Joachim Breitner Though #eval can modify the environment! It accepts CommandElabM values.

[Mauricio Collares]

Asei Inoue said:

In general, PRs to core are not welcome

whatsnew is in Mathlib

Ah, my bad! I just looked at the channel name and forgot to check.

[Joachim Breitner]

Kyle Miller said:

Joachim Breitner Though #eval can modify the environment! It accepts CommandElabM values.

I didn’t know that (or maybe repressed it). Is there a reason to use #eval here instead of run_cmd (besides that the latter is younger)?

[Eric Wieser]

example also seems like a counterexample to this "# iff changes the environment" rule

[Joachim Breitner]

Good point.

[Joachim Breitner]

It’s just a rule I picked up somewhere, don’t know where, so certainly not authorative. But do we have a better explanation for when to use #?

[Kyle Miller]

In mathlib it's sort of "commands that shouldn't stick around in the library"

[Eric Wieser]

Is the rule just "be as conservative as you can, because any command keyword you claim will end up illegal in terms; prepend a # if in doubt"?

[Joachim Breitner]

Kyle Miller said:

In mathlib it's sort of "commands that shouldn't stick around in the library"

I thought about this, but then #guard_msgs comes to mind. I guess that shouldn’t stick around the library, and tests are different.

[Kyle Miller]

Yeah, that's a distinction I'm drawing

[Kyle Miller]

I've felt like it would be nice to remove run_cmd etc in favor of #eval (it's now defined in terms of #eval after all), but I suppose that run_cmd doesn't try pretty printing its result, so it's library material.

[Eric Wieser]

#guard_msgs is consistent with #guard_expr at least

[Joachim Breitner]

For me at least, having the run_xxx commands was a great win, because I could never remember the syntax involving #eval and some ( to me strange) show SomeMonad using do idiom or whatever that was.

[Kyle Miller]

You generally don't need to write show ... now, though the inference isn't perfect.

[Joachim Breitner]

And the use case “test running some code” and ”do some persistent changes to the environment ” are so fundamentally different that I'd actually prefer different commands, where #eval is always side-effect free (disregarding direct IO)

[Kyle Miller]

If I'm experimenting with some elaboration code, I wouldn't want to have to switch from #eval to run_cmd just to use elabCommand

[Joachim Breitner]

Oh, read access to the environment based on the monasin question is fine, it's just the final persisting of the effect that I'm surprised by.

[Joachim Breitner]

(TBH, all my experimentation starts with the suitable run_cmd or run_meta anyways, I only used #eval for pure calculations. But that largely due to ignorance of what's possible, and habit.)

[Kyle Miller]

I mean "just to use elabCommand and observe its results afterwards"

[Joachim Breitner]

Fair enough! Different habits, I guess? I certainly didn't want to imply that that needs to change or anything like that. I should probably try using it myself!

[Asei Inoue]

Would #whatsnew or #whatsnew be more appropriate?