Vscode extension npm test

Stream: lean4

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

I cloned the vscode repo and followed the build and test process (on _windows_). When running npm test I get

 >  Lerna (powered by Nx)   Running target test for 2 projects failed

   Failed tasks:

   - lean4:test

Upon closer inspection the following error comes up as the first in the stack trace.

lean4: 16:59:07.213 - >>>>>>>>> testsRoot=...\lean\vscode-lean4\vscode-lean4\out\test\suite\pre-bootstrap
lean4: TypeError: Cannot read properties of undefined (reading 'describe')

[Shreyas Srinivas]

I have made sure my drive letter is upper-case. I read the other recommendation to purge the elan folder

[Shreyas Srinivas]

It says

Try wiping your .elan folder and start over running all tests in order using npm run tests. This
could fix some things, for example, if you have an incompatible default lean toolchain.

This seems a bit overkill. Where should I look to find which toolchain to set as default?

[Shreyas Srinivas]

Fwiw, the current default toolchain is leanprover/lean4:v4.1.0

[Shreyas Srinivas]

What's the fix for this?

[Notification Bot]

This topic was moved here from #lean4 > Vscode repo test by Shreyas Srinivas.

[Notification Bot]

This topic was moved here from #lean4 > Vscode extensionrepo test by Shreyas Srinivas.