Persistent extension not persisting

Stream: lean4

[Patrick Massot]

I though I understood how environment extensions works but I realize that I didn't test persistence across files. If I create a project with
lake +leanprover/lean4:nightly-2022-08-15 new issue && cd issue && rm Issue.lean && mkdir Issue && cd Issue with
Extension.lean:

import Lean

open Lean

initialize myExt : SimplePersistentEnvExtension String (Array String) ←
  registerSimplePersistentEnvExtension {
    name := `mystuff
    addEntryFn := Array.push
    addImportedFn := Array.concatMap id
  }

open Elab Command in
elab "#liststuff" : command => do
  for stuff in myExt.getEntries (← getEnv) do
    dbg_trace stuff

elab "addStuff" msg:str : command => do
  modifyEnv (myExt.addEntry · msg.getString)

file1.lean:

import Issue.Extension

addStuff "Test"

#liststuff

file2.lean

import Issue.file1

#liststuff

then everything works fine in file1 but I don't get any output in file2

[Leonardo de Moura]

The implementation of #liststuff is incorrect. You should use myExt.getState instead of myExt.getEntries. The method getEntries returns the entries created in the current file.

[Patrick Massot]

Thank you very much. I opened https://github.com/leanprover/lean4/pull/1487. I know that documenting the whole file would be better but at least I didn't let this answer disappear.

[Sebastian Ullrich]

We already have getModuleEntries, which suggests getCurrentModuleEntries as a less ambiguous name