Zulip Chat Archive

Stream: lean4

Topic: Environment extensions in importModules


Mario Carneiro (Aug 16 2021 at 20:39):

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 (Aug 16 2021 at 20:42):

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 (Aug 17 2021 at 01:05):

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


Last updated: Dec 20 2023 at 11:08 UTC