Environment extensions in importModules

Stream: lean4

[Mario Carneiro]

Test/A.lean:

import Lean
open Lean

initialize fooAttr : TagAttribute ← registerTagAttribute `foo "foo"

Test.lean:

import Test.A
open Lean

unsafe def main : IO Unit := do
  Lean.initSearchPath "/home/mario/.elan/toolchains/leanprover--lean4---nightly/lib/lean/:build"
  withImportModules [{ module := `Test.A : Import }] {} 0 fun env => ()

result:

$ build/bin/Test
uncaught exception: invalid environment extension, 'foo' has already been used

I don't see where the conflict is here, since withImportModules should presumably be working from a clean environment, not containing the declarations in the ambient environment (i.e. the one in the CommandElabM used to elaborate main). There are no diamonds or anything either

[Mario Carneiro]

I have no idea if this is related, but if Test.lean doesn't import Test.A and just imports Lean, then it segfaults at runtime

[Leonardo de Moura]

Pushed a fix for it. The example above should now work using master.