leanprover / vscode-lean

Extension for VS Code that provides support for the older Lean 3 language. Succeeded by vscode-lean4 ('lean4' in the extensions menu) for the Lean 4 language.
Apache License 2.0
116 stars 49 forks source link

fix: some shutdown bugs found in CI testing with the lean3 extension. #292

Closed lovettchris closed 2 years ago

lovettchris commented 2 years ago

This doesn't fix them all, there is still one deeper unhandled exception inside lean-client-js-core or lean-client-js-node but I found a work around for that one...

 Uncaught Error: write EPIPE
        at afterWriteDispatched (internal/stream_base_commons.js:156:25)
        at writeGeneric (internal/stream_base_commons.js:147:3)
        at Socket._writeGeneric (net.js:785:11)
        at Socket._write (net.js:797:8)
        at writeOrBuffer (internal/streams/writable.js:358:12)
        at Socket.Writable.write (internal/streams/writable.js:303:10)
        at a.send (d:\git\leanprover\vscode-lean4\test\.vscode-test\extensions\jroesch.lean-0.16.45\out\extension.js:2:463916)
        at h.send (d:\git\leanprover\vscode-lean4\test\.vscode-test\extensions\jroesch.lean-0.16.45\out\extension.js:2:460013)
        at o.<anonymous> (d:\git\leanprover\vscode-lean4\test\.vscode-test\extensions\jroesch.lean-0.16.45\out\extension.js:2:462002)
        at Generator.next (<anonymous>)
        at d:\git\leanprover\vscode-lean4\test\.vscode-test\extensions\jroesch.lean-0.16.45\out\extension.js:2:459189
        at new Promise (<anonymous>)
        at r (d:\git\leanprover\vscode-lean4\test\.vscode-test\extensions\jroesch.lean-0.16.45\out\extension.js:2:458963)
        at o.send (d:\git\leanprover\vscode-lean4\test\.vscode-test\extensions\jroesch.lean-0.16.45\out\extension.js:2:461920)
        at t.InfoProvider.handleServerRequest (d:\git\leanprover\vscode-lean4\test\.vscode-test\extensions\jroesch.lean-0.16.45\out\extension.js:2:1001827)
        at t.InfoProvider.<anonymous> (d:\git\leanprover\vscode-lean4\test\.vscode-test\extensions\jroesch.lean-0.16.45\out\extension.js:2:1001463)
        at Generator.next (<anonymous>)
        at d:\git\leanprover\vscode-lean4\test\.vscode-test\extensions\jroesch.lean-0.16.45\out\extension.js:2:996397
        at new Promise (<anonymous>)
        at r (d:\git\leanprover\vscode-lean4\test\.vscode-test\extensions\jroesch.lean-0.16.45\out\extension.js:2:996142)
        at t.InfoProvider.handleMessage (d:\git\leanprover\vscode-lean4\test\.vscode-test\extensions\jroesch.lean-0.16.45\out\extension.js:2:1001062)
        at d:\git\leanprover\vscode-lean4\test\.vscode-test\extensions\jroesch.lean-0.16.45\out\extension.js:2:1000823
        at l.fire (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:64:1712)
        at S.$onMessage (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:94:75455)
        at i._doInvokeHandler (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:97:13801)
        at i._invokeHandler (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:97:13485)
        at i._receiveRequest (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:97:12147)
        at i._receiveOneMessage (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:97:11024)
        at d:\git\leanprover\vscode-lean4\test\.vscode-test\vscode-win32-archive-1.64.2\resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:97:8934
        at l.fire (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:64:1712)
        at s.fire (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:72:19002)
        at d:\git\leanprover\vscode-lean4\test\.vscode-test\vscode-win32-archive-1.64.2\resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:112:34390
        at l.fire (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:64:1712)
        at s.fire (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:72:19002)
        at a._receiveMessage (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:72:23583)
        at d:\git\leanprover\vscode-lean4\test\.vscode-test\vscode-win32-archive-1.64.2\resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:72:21117
        at l.fire (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:64:1712)
        at _.acceptChunk (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:72:15833)
        at d:\git\leanprover\vscode-lean4\test\.vscode-test\vscode-win32-archive-1.64.2\resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:72:14963
        at Socket.A (resources\app\out\vs\workbench\services\extensions\node\extensionHostProcess.js:112:13838)
        at addChunk (internal/streams/readable.js:309:12)
        at readableAddChunk (internal/streams/readable.js:284:9)
        at Socket.Readable.push (internal/streams/readable.js:223:10)
        at Pipe.onStreamRead (internal/stream_base_commons.js:188:23)