search

glacode / yamma

VSCode extension for Metamath
10 stars 2 forks source link

Maximum Call Stack Size Exceeded #9

Open tirix opened 1 year ago

tirix commented 1 year ago

This is an extract of the errors I get when trying to work on ~footex:

[Trace - 01:31:43] Sending request 'textDocument/hover - (213)'.
/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/server/out/mmp/MmpProofStep.js:307
                proof === null || proof === void 0 ? void 0 : proof.unshift(...proofForEHypUStep);
                                                                    ^

RangeError: Maximum call stack size exceeded
    at MmpProofStep.proofArray (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/server/out/mmp/MmpProofStep.js:307:69)
    at MmpProofStep.proofArray (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/server/out/mmp/MmpProofStep.js:306:107)
    at MmpProofStep.proofArray (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/server/out/mmp/MmpProofStep.js:306:107)
    at MmpProofStep.proofArray (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/server/out/mmp/MmpProofStep.js:306:107)
    at MmpProofStep.proofArray (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/server/out/mmp/MmpProofStep.js:306:107)
    at MmpProofStep.proofArray (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/server/out/mmp/MmpProofStep.js:306:107)
    at MmpProofStep.proofArray (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/server/out/mmp/MmpProofStep.js:306:107)
    at new UCompressedProofStatement (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/server/out/mmp/UCompressedProofStatement.js:31:64)
    at MmpUnifier.buildProofStatementIfProofIsComplete (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/server/out/mmp/MmpUnifier.js:80:40)
    at MmpUnifier.unify (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/server/out/mmp/MmpUnifier.js:95:14)
[Info  - 01:31:44] Connection to server got closed. Server will restart.
[Error - 01:31:44] Request textDocument/hover failed.
Error: Connection got disposed.
    at Object.dispose (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/connection.js:1044:27)
    at Object.dispose (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-languageclient/lib/common/client.js:73:35)
    at LanguageClient.handleConnectionClosed (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-languageclient/lib/common/client.js:2424:42)
    at LanguageClient.handleConnectionClosed (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-languageclient/lib/node/main.js:155:15)
    at closeHandler (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-languageclient/lib/common/client.js:2411:18)
    at CallbackList.invoke (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/events.js:55:39)
    at Emitter.fire (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/events.js:117:36)
    at closeHandler (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/connection.js:256:26)
    at CallbackList.invoke (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/events.js:55:39)
    at Emitter.fire (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/events.js:117:36)
    at IPCMessageReader.fireClose (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/messageReader.js:40:27)
    at ChildProcess.<anonymous> (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/node/main.js:33:45)
    at ChildProcess.emit (node:events:525:35)
    at maybeClose (node:internal/child_process:1121:16)
    at Socket.<anonymous> (node:internal/child_process:479:11)
    at Socket.emit (node:events:513:28)
    at Pipe.<anonymous> (node:net:757:14)
[Error - 01:31:44] Request textDocument/hover failed.
Error: Connection got disposed.
    at Object.dispose (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/connection.js:1044:27)
    at Object.dispose (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-languageclient/lib/common/client.js:73:35)
    at LanguageClient.handleConnectionClosed (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-languageclient/lib/common/client.js:2424:42)
    at LanguageClient.handleConnectionClosed (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-languageclient/lib/node/main.js:155:15)
    at closeHandler (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-languageclient/lib/common/client.js:2411:18)
    at CallbackList.invoke (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/events.js:55:39)
    at Emitter.fire (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/events.js:117:36)
    at closeHandler (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/connection.js:256:26)
    at CallbackList.invoke (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/events.js:55:39)
    at Emitter.fire (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/events.js:117:36)
    at IPCMessageReader.fireClose (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/common/messageReader.js:40:27)
    at ChildProcess.<anonymous> (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.7/client/node_modules/vscode-jsonrpc/lib/node/main.js:33:45)
    at ChildProcess.emit (node:events:525:35)
    at maybeClose (node:internal/child_process:1121:16)
    at Socket.<anonymous> (node:internal/child_process:479:11)
    at Socket.emit (node:events:513:28)
    at Pipe.<anonymous> (node:net:757:14)
[Trace - 01:31:44] Sending request 'initialize - (0)'.
[Trace - 01:31:44] Received response 'initialize - (0)' in 201ms.
[Trace - 01:31:44] Sending notification 'initialized'.
[Trace - 01:31:44] Sending notification 'textDocument/didOpen'.

It's probably not necessary to fix this issue, it's due to a theorem which also messes up with metamath-exe, but I wanted to log it here anyway.

glacode commented 1 year ago

this one is really interesting. I'm going to look into it

glacode commented 1 year ago

Hi @tirix ,

how is that the proof for ~ragperp does not list

$d ph u

that should be required by ralrimivva at step 65 ?

Am I missing something simple, here?

Thanks in advance Glauco

glacode commented 1 year ago

how is that the proof for ~ragperp does not list

$d ph u

As I expected, mmj2 also adds

$d ph u

tirix commented 1 year ago

So the reason why not all distinct variables declarations were set is probably the following: to start with the proof, I used the "$get-theorem" command, which works fine, except that it does not add those distinct variables.

I probably added some, but not all, when I started working on splitting the proof.

It looks like you already have a correction for that special case, that's great!

glacode commented 1 year ago

I mean, the

$d ph u

seems to be missing in the set.mm file, but it validates, so the statement must be in an outer scope.

Is this the case? Can you find it in an outer scope?

tirix commented 1 year ago

Oh I see. I'll check later.

tirix commented 1 year ago

Ok, so after careful check I can confirm that the $d ph u is indeed present in the frame, just above~ isperp. The website seems to miss it when it renders, I think that's a bug of the website.

Interestingly, I have not found in either metamath-exe or metamath-knife any option to display the distinct variables list for a given theorem.