I have the weirdest problem with this error. I get it from a bare bones "cmd.exe" on my machine and in my github ci on "windows-latest". But if I run the test in VS code using my Extension Tests - lean3 launch configuration it runs fine, and if I run it from a Visual Studio Developer Command prompt it runs fine (but I should totally not need a vs developer prompt to run these tests). The repro is this:
I have the weirdest problem with this error. I get it from a bare bones "cmd.exe" on my machine and in my github ci on "windows-latest". But if I run the test in VS code using my Extension Tests - lean3 launch configuration it runs fine, and if I run it from a Visual Studio Developer Command prompt it runs fine (but I should totally not need a vs developer prompt to run these tests). The repro is this:
The test begins, it downloads a test version of vscode, vscode launches, but then the mocha.run blows up with this error:
My tests are "ui: tdd" tests which is specified in my index.ts so I'm not sure why it's even looking for
describe
...But here's the most ridiculous part. If I run this
then type this:
Then the tests run fine, no problem with mocha. Even weirder, if I do this:
Then type:
It seems to have something to do with the casing of the "D:" drive letter? If I run "pushd D:\git\leanprover\vscode-lean4" then the test fails...