last declaration added to `Environment`

Stream: lean4

[Damiano Testa]

Is there a way to pop the last declaration added to the environment?

I know that the environment stores declarations in (roughly) HashMaps, but I was wondering if, by any chance, the latest declaration was still available somehow.

In fact, I would like to access the last non-autogenerated declaration. Here is an example:

import Lean.Log

@[simp]
theorem easy : True := .intro

open Lean in
#eval do
  let env ← getEnv
  logInfo env.pop
-- does not work, but ideally it would output
-- `easy`

[Mario Carneiro]

No, the data is not retained. previous zulip discussion

[Damiano Testa]

Ok, thanks! I guess that the whatsnew in approach is the closest to what I was hoping for, then.

[Alex J. Best]

You could sort the constants in the current file by their declarationranges I guess to find the lowest one in the file?

[Damiano Testa]

I kind of solved my problem: I compile one command at a time, so there is exactly one "visible", the others are auto-generated (if any). I catch the visible, by matching the explicit name and the others... well they do not have a range, but I pretend that there is at most one.

[Damiano Testa]

Since this was for the deprecation tool, the main use case is

• a command adds a single declaration
• the command adds a lemma and a to_additive version.

For more complicated stuff... it just goes with what it has.

[Damiano Testa]

You can take a look at the PR and feel free to comment/ask questions!

#10864