modifyEnv and environment extensions in v4.19.0

Stream: general

[Joseph Tooby-Smith]

As part of PhysLean we have TODO items which are collected using an enviroment extension set up with the following code:

Set up enviroment extension

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import Lean.Elab.Command
/-!

# Basic underlying structure for TODOs.

-/

namespace PhysLean
open Lean

/-- The information from a `TODO ...` command. -/
structure todoInfo where
  /-- The content of the note. -/
  content : String
  /-- The file name where the note came from. -/
  fileName : Name
  /-- The line from where the note came from. -/
  line : Nat
  /-- The tag of the TODO item -/
  tag : String

/-- Environment extension to store `todo ...`. -/
initialize todoExtension : SimplePersistentEnvExtension todoInfo (Array todoInfo) ←
  registerSimplePersistentEnvExtension {
    name := `todoExtension
    addEntryFn := fun arr todoInfor => arr.push todoInfor
    addImportedFn := fun es => es.foldl (· ++ ·) #[]
  }

/-- Syntax for the `TODO ...` command. -/
syntax (name := todo_comment) "TODO " str str : command

/-- Elaborator for the `TODO ...` command -/
@[command_elab todo_comment]
def elabTODO : Elab.Command.CommandElab := fun stx =>
  match stx with
  | `(TODO $t $s) => do
    let str : String := s.getString
    let tag : String := t.getString
    let pos := stx.getPos?
    match pos with
    | some pos => do
      let env ← getEnv
      let fileMap ← getFileMap
      let filePos := fileMap.toPosition pos
      let line := filePos.line
      let modName := env.mainModule
      let todoInfo : todoInfo := { content := str, fileName := modName, line := line, tag := tag }
      modifyEnv fun env => todoExtension.addEntry env todoInfo
    | none => throwError "Invalid syntax for `TODO` command"
  | _ => throwError "Invalid syntax for `TODO` command"

end PhysLean

An example of a TODO item in PhysLean is:

TODO "6VZJH" "For the classical harmonic oscillator find the velocity when it passes through
  zero."

There are many such items.

An example bit of code for collecting the TODO items is:

Collection code

import PhysLean.Meta.Basic
import PhysLean.Meta.TODO.Basic
import Mathlib.Lean.CoreM
import PhysLean.Meta.Informal.Post
import PhysLean.Meta.Informal.SemiFormal
/-!

# Checks for duplicate TODO tags

-/

open Lean System Meta PhysLean


def tagsFromTODOs : MetaM (Array String) := do
  let env ← getEnv
  let todoInfo := (todoExtension.getState env)
  -- pure (todoInfo.qsort (fun x y => x.fileName.toString < y.fileName.toString)).toList
  pure (todoInfo.map fun x => x.tag)

unsafe def informalTODO (x : ConstantInfo) : CoreM String := do
  let tag ← Informal.getTag x
  return tag

unsafe def tagsFromInformal : CoreM (Array String) := do
  (← AllInformal).mapM (fun x => Informal.getTag x)

unsafe def tagsFromSemiformal  : CoreM (Array String) := do
  let env ← getEnv
  let semiInformalInfos := (wantedExtension.getState env)
  pure (semiInformalInfos.map fun x => x.tag)

unsafe def tagDuplicateTest : MetaM Unit := do
  let tags := ((← tagsFromTODOs) ++ (← tagsFromInformal) ++ (← tagsFromSemiformal)).toList
  if !tags.Nodup then
    let duplicates := tags.filter (fun tag => tags.count tag > 1) |>.eraseDups
    println! duplicates
    panic! s!"Duplicate tags found: {duplicates}"
  pure ()

unsafe def main (args : List String) : IO UInt32 := do
  initSearchPath (← findSysroot)
  println! "Checking for duplicate tags."
  let _ ← CoreM.withImportModules #[`PhysLean] (tagDuplicateTest).run'
  println! "Finish duplicate tag check."
  pure 0

The problem is that this no longer works. In particular let todoInfo := (todoExtension.getState env) returns an array of zero size. I believe this all worked fine on v4.18.0, in particular let todoInfo := (todoExtension.getState env) returned a non-zero array, and the code has not been modified since then.

Does anyone know the cause/ a possible solution?

[Joseph Tooby-Smith]

(suspect this is something related to #general > v4.19.0-rc2 @ 💬 )

[David Renshaw]

Try using Lean.importModules with loadExts := true. https://leanprover-community.github.io/mathlib4_docs/Lean/Environment.html#Lean.importModules

[David Renshaw]

... instead of withImortModules.

[Joseph Tooby-Smith]

Ok, thanks David, the following seems to work:

I changed:

unsafe def main (args : List String) : IO UInt32 := do
  initSearchPath (← findSysroot)
  println! "Checking for duplicate tags."
  let _ ← CoreM.withImportModules #[`PhysLean] (tagDuplicateTest).run'
  println! "Finish duplicate tag check."
  pure 0

to

open Core
unsafe def main (args : List String) : IO UInt32 := do
  initSearchPath (← findSysroot)
  println! "Checking for duplicate tags."
  let env ← importModules (loadExts := true) #[`PhysLean] {} 0
  let fileName := ""
  let options : Options := {}
  let ctx : Core.Context := {fileName, options, fileMap := default }
  let state := {env}
  let _ ← (Lean.Core.CoreM.toIO · ctx state) do (tagDuplicateTest).run'
  println! "Finish duplicate tag check."
  pure 0

in my last code block. Not sure this is the cleanest way of doing things within the context of my overall code though, but this is ok.

(For my reference the PR which breaks this is this)