Marc Huisinga
Marc Huisinga
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,...
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 fixes the issue :) Compilation seems to be much quicker as well.
I am closing this issue for now. Please let me know if it comes up again, and I will re-open it.
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:...
I cannot reproduce this issue anymore on 01-10 (it may be due with the disabled `precompileModules` on master, not sure).
One potential issue is that you can get deadlocks using `modify` this way, right?
A common access pattern if `modify` allows `IO` would be to use `modify` on one `IO.Ref` and within that use `modify` on another `IO.Ref`. If another call site uses these...
Note that two tests in the Lean 4 test suite accidentally test false positives. See the `linterUnusedVariables.lean` diff at https://github.com/leanprover/lean4/pull/3082/files#diff-a33d4a408eca48eae24f881090327a42577735140184b3485ec87f08af36a8cc