Importing aesop yields "invalid environment extension, 'coe' has already been used" error

[mhuisi]

Following the instructions in the "Adding Aesop to Your Project" section of the README in a fresh project with the leanprover/lean4:nightly-2022-10-03 nightly, importing aesop yields an invalid environment extension, 'coe' has already been used error.

[JLimperg]

I'm afraid I can't reproduce. My test setup:

lean-toolchain:

leanprover/lean4:nightly-2022-10-03

lakefile.lean:

import Lake
open Lake DSL

package repro {
  -- add package configuration options here
}

@[defaultTarget]
lean_lib Repro {
  -- add library configuration options here
}

require aesop from git "https://github.com/JLimperg/aesop"

Repro.lean:

import Aesop

example : 1 + 1 = 2 := by
  aesop

lean_packages/manifest.json (auto-generated):

{"version": 2,
 "packages":
 [{"url": "https://github.com/JLimperg/aesop",
   "rev": "c9c533eb40a1b8aeee8278252aff75e9c91ed639",
   "name": "aesop"},
  {"url": "https://github.com/leanprover/std4",
   "rev": "8dc73e59a2e682260bd4b92c0ddee14d36fc6518",
   "name": "std"}]}

With this, lake build succeeds without errors.

[mhuisi]

To be clear, lake build succeeds, but then opening the project and subsequently Repro.lean using VSCode yields the error. OTOH, doing the same for a different library seems to work, e.g. Std4 by itself.

[JLimperg]

Can't reproduce this either -- I can open Repro.lean in VSCode and Emacs and it typechecks without issues. My best guess is that your environment got subtly broken somehow, so I would nuke some combination of ~/.elan, VSCode and lean_packages and start from scratch.

[mhuisi]

Hm. Nuking all the build directories (I had tried this by itself before) + elan unfortunately didn't resolve the issue either. Perhaps it has something to do with the fact that I'm using W10? Very strange regardless.

All my files are identical to yours.

EDIT: In any case, it seems less and less likely that this is an Aesop issue.

[Kha]

Does it happen without precompilation as well? https://github.com/JLimperg/aesop/blob/master/lakefile.lean#L6

[mhuisi]

That fixes the issue :) Compilation seems to be much quicker as well.

[Kha]

Trading compilation time for run time is the central idea, yes :) . If I had to guess, I would say that std4's coe extension is loaded both by the precompiled code and by interpreted .olean code. Not sure why yet, but a platform-specific bug somewhere in there is at least thinkable.

[JLimperg]

Okay, interesting. I'll mention in the README that there's a possible issue on Windows. Thanks for the report!

[tydeu]

@Kha @JLimperg I encountered this same bug a while back myself in Alloy. The problem is with PresistentEnvExtension, the extensions is seen both in the precompiled shared object and by the the interpreted import which results in a clash. To get around this, when registering a persistent extension, one can check whether an extension with the same name already exists and return it instead. This is unsafe, but works. See findOrRegisterPersistentExtension in Alloy for an example check and these extensions for the actual use.

As this appears to need a std4 change, it might be best to loop @digama0 into this issue and potentially create a similar issue on the std4 repository (or even to upstream this change into the Lean 4 core's environment registration).

[Kha]

Let's please fix the actual bug instead of adding workarounds.

[tydeu]

@Kha Ah, sorry, from this issue and my experience, I was under the impression it just part of how Windows loads module shared objects. I guess the idea is that there is some platform-specific problem with the Windows module load process that causes it run the initializer twice or already have the extension in the persistent environment reference map?

[Kha]

Yes, as I wrote above.

[tydeu]

@Kha Ah. I saw that issue, and while the 128 module limit problem you found was interesting, I was a little confused as to why that would be causing this bug. For example, Alloy most certainly does not have more than 128 precompiled modules so it should not be hitting that limit yet still has this problem. Maybe I should move this discussion over there then? I was posting here to give a workaround if someone really needs precompiled modules to work in the presence of this issue in the meantime (like Alloy does). I also wanted to highlight that the problem (in my experience) comes specifically from name clashes in persistent environment extension registration / map.

[Kha]

Yes, let's continue the discussion there. Any help by Windows users is appreciated.

[JLimperg]

Aesop master now uses the 11-19 Lean nightly, which contains a fix for this issue. @mhuisi could you try enabling precompileModules again to see whether it works now?

[mhuisi]

The language server yields

error: external command `c:\Users\mhuisi\.elan\toolchains\leanprover--lean4---nightly-2022-11-19\bin\leanc.exe` exited with code 1

when opening Repro.lean. Building Repro from scratch yields a bunch of errors of the following form:

C:\Users\mhuisi\Desktop\Repro> lake build
Building Aesop.Check
Building Std.Tactic.Unreachable
Building Aesop.Nanos
Building Std.Lean.TagAttribute
Building Std.Classes.Dvd
Building Std.Tactic.OpenPrivate
Building Std.Classes.BEq
Building Std.Tactic.GuardExpr
Building Std.Tactic.SeqFocus
Building Std.Tactic.ByCases
Building Std.Tactic.TryThis
Building Std.Lean.Parser
Building Std.Lean.Meta
Building Std.Lean.Tactic
Building Std.Util.TermUnsafe
Building Std.Lean.NameMapAttribute
Building Std.Data.List.Init.Lemmas
Building Std.Util.ExtendedBinder
Building Std.Control.ForInStep.Basic
Building Std.Data.Option.Init.Lemmas
Building Std.Tactic.HaveI
Building Std.Tactic.RCases
Building Std.Lean.Command
Building Std.Data.DList
Building Std.Data.Fin.Lemmas
Building Std.Tactic.CoeExt
Building Std.Util.LibraryNote
Building Std.Tactic.SqueezeScope
Building Aesop.Percent
Building Aesop.Rule.BranchState
Building Aesop.Options
Building Aesop.Search.Expansion.Simp.Basic
Building Aesop.Tracing.Init
Compiling Std.Classes.Dvd
Compiling Std.Classes.BEq
error: > c:\Users\mhuisi\.elan\toolchains\leanprover--lean4---nightly-2022-11-19\bin\leanc.exe -c -o .\lean_packages\std\build\ir\Std\Classes\Dvd.o .\lean_packages\std\build\ir\Std\Classes\Dvd.c -O3 -DNDEBUG
error: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command `c:\Users\mhuisi\.elan\toolchains\leanprover--lean4---nightly-2022-11-19\bin\leanc.exe` exited with code 1
Compiling Aesop.Check
error: > c:\Users\mhuisi\.elan\toolchains\leanprover--lean4---nightly-2022-11-19\bin\leanc.exe -c -o .\lean_packages\std\build\ir\Std\Classes\BEq.o .\lean_packages\std\build\ir\Std\Classes\BEq.c -O3 -DNDEBUG
error: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command `c:\Users\mhuisi\.elan\toolchains\leanprover--lean4---nightly-2022-11-19\bin\leanc.exe` exited with code 1
Compiling Std.Tactic.Unreachable
Compiling Aesop.Nanos
error: > c:\Users\mhuisi\.elan\toolchains\leanprover--lean4---nightly-2022-11-19\bin\leanc.exe -c -o .\lean_packages\aesop\build\ir\Aesop\Check.o .\lean_packages\aesop\build\ir\Aesop\Check.c -O3 -DNDEBUG
error: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command `c:\Users\mhuisi\.elan\toolchains\leanprover--lean4---nightly-2022-11-19\bin\leanc.exe` exited with code 1
Compiling Std.Tactic.OpenPrivate
[many more errors]

This is with the same lakefile from before (with @[default_target] instead of @[defaultTarget]) and leanprover/lean4:nightly-2022-11-19. The manifest reflects that it's using the versions of aesop and std4 that it should. Just importing the most recent Std4 and trying to build it works without issues.

[Kha]

leanc failing must be some new, unrelated kind of regression :thinking:

[JLimperg]

I've seen these "no such file or directory" errors before when the VSCode extension compiles dependencies (on MacOS). However, I've not seen them in lake build or the Emacs mode before. They seemed to be transient as well, possibly some race condition.

[mhuisi]

I cannot reproduce this issue anymore on 01-10 (it may be due with the disabled precompileModules on master, not sure).

[JLimperg]

Thanks for trying again! Let's see if this comes back once we turn precompileModules back on. (This is currently blocked on Lake).