Crash - The USubstitutionBuilder is trying to build a build a ParseNode [...]

[tirix]

I sometimes encounter this issue when using Yamma:

[Trace - 14:23:42] Sending request 'yamma/unify - (67)'.
[Trace - 14:23:42] Received response 'yamma/unify - (67)' in 6ms.
Error! The USubstitutionBuilder is trying to build a build a ParseNode, but the given substitution does not contain a substitution value for the logical variable 'ph'
/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/mmp/MmpSubstitutionApplier.js:54
            throw new Error(`Error! The USubstitutionBuilder is trying to ` +
                  ^

Error: Error! The USubstitutionBuilder is trying to build a build a ParseNode, but the given substitution does not contain a substitution value for the logical variable 'ph'
    at MmpSubstitutionApplier.createParseNodeForLogicalVariable (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/mmp/MmpSubstitutionApplier.js:54:19)
    at MmpSubstitutionApplier.createParseNode (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/mmp/MmpSubstitutionApplier.js:78:51)
    at /Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/mmp/MmpSubstitutionApplier.js:64:57
    at Array.forEach (<anonymous>)
    at MmpSubstitutionApplier.createParseNodeForInternalNode (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/mmp/MmpSubstitutionApplier.js:63:53)
    at EHypsDerivation.buildFormulaForCurrentEHypProofStep (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/stepDerivation/EHypsDerivation.js:78:75)
    at EHypsDerivation.searchCurrentEHypWithoutAdditionalVarsToBeUnified (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/stepDerivation/EHypsDerivation.js:87:53)
    at EHypsDerivation.searchEHypsRecursive (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/stepDerivation/EHypsDerivation.js:113:18)
    at EHypsDerivation.searchEHyps (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/stepDerivation/EHypsDerivation.js:128:18)
    at StepDerivation.tryEHypsDerivation (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/stepDerivation/StepDerivation.js:44:25)
[Info  - 14:23:43] Connection to server got closed. Server will restart.

In that case the server restarts. Usually it encounters exactly the same issue, and after 5 restarts, VSCode disables it.

[tirix]

Here is a minimal MMP file generating this issue:

$theorem crash

* MissingComment

10::                |- ( ph <-> ( ps /\ th ) )
20:10:biimpar      
qed::              |- ( et -> ph )

Here, biimpar is not the right theorem to apply to derive, but I'm being punished too harshly for that. I expect that instead of crashing, Yamma should raise a problem.

[glacode]

Definetely, it shouldn't crash... :-)

Now I'm in the middle of developing the mm > mmp converter (the mmj2 ctrl+g counterpart), then I will focus on the run time errors you've submitted. Thank you for the simple example, a perfect candidate for a new unit test.

[glacode]

For the time being, I've not been able to reproduce the crash.

It shows the expected warnings/errors

May it be the case that you got a "previous" crash? (when the extension is reactivated, its behavior is unpredictable)

Do you get a crash even if this is the first .mmp you open?

[tirix]

Ok, indeed I tried with just that .mmp opened, and it did not crash.

Then I tried opening and unifying dimkerim.mmp first (success), then unifying crash.mmp, with both editor views opened at the same time, and I reproduced the crash.

In the trace below you'll see the first successful unification for dimkerim (38ms), then the swap to the other editor, then the second unification and the failure. When I'm opening the second view, Yamma goes through a createLabelToParseNodeForThreadMap which I've elided.

[Trace - 22:45:22] Received response 'textDocument/codeAction - (22)' in 554ms.
[Trace - 22:45:22] Sending request 'textDocument/hover - (23)'.
[Trace - 22:45:22] Received response 'textDocument/hover - (23)' in 0ms.
[Trace - 22:45:25] Sending request 'yamma/unify - (24)'.
[Trace - 22:45:25] Received response 'yamma/unify - (24)' in 38ms.
[Trace - 22:45:26] Received request 'workspace/applyEdit - (15)'.
[Trace - 22:45:26] Sending response 'workspace/applyEdit - (15)'. Processing request took 7ms
validateFullDocument - this.mmParser:[object Object]
before mmpParser.parse()
after mmpParser.parse()
[Trace - 22:45:26] Received notification 'textDocument/publishDiagnostics'.
[Trace - 22:45:26] Received notification 'yamma/movecursor'.
[Trace - 22:45:26] Sending request 'textDocument/codeAction - (25)'.
I am back to the Main thread!!!!!!!
Worker thread!!!!: labelToFormulaMap.size = 97776
[22:44:18 GMT+0200 (Central European Summer Time)] createLabelToParseNodeForThreadMap - 1%
[22:44:18 GMT+0200 (Central European Summer Time)] createLabelToParseNodeForThreadMap - 2%
[.../...]
[22:45:23 GMT+0200 (Central European Summer Time)] createLabelToParseNodeForThreadMap - 98%
[22:45:24 GMT+0200 (Central European Summer Time)] createLabelToParseNodeForThreadMap - 99%
[Trace - 22:45:28] Received response 'textDocument/codeAction - (25)' in 2487ms.
[Trace - 22:45:29] Sending request 'textDocument/codeAction - (26)'.
[Trace - 22:45:29] Received response 'textDocument/codeAction - (26)' in 1ms.
[Trace - 22:45:29] Sending request 'textDocument/codeAction - (27)'.
[Trace - 22:45:29] Received response 'textDocument/codeAction - (27)' in 0ms.
[Trace - 22:45:31] Sending request 'textDocument/semanticTokens/full - (28)'.
connection.languages.semanticTokens.on1
connection.languages.semanticTokens.on2
[Trace - 22:45:31] Received response 'textDocument/semanticTokens/full - (28)' in 89ms.
[Trace - 22:45:36] Sending request 'yamma/unify - (29)'.
[Trace - 22:45:36] Received response 'yamma/unify - (29)' in 1ms.
Error! The USubstitutionBuilder is trying to build a build a ParseNode, but the given substitution does not contain a substitution value for the logical variable 'ph'
/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/mmp/MmpSubstitutionApplier.js:54
            throw new Error(`Error! The USubstitutionBuilder is trying to ` +
                  ^

Error: Error! The USubstitutionBuilder is trying to build a build a ParseNode, but the given substitution does not contain a substitution value for the logical variable 'ph'
    at MmpSubstitutionApplier.createParseNodeForLogicalVariable (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/mmp/MmpSubstitutionApplier.js:54:19)
    at MmpSubstitutionApplier.createParseNode (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/mmp/MmpSubstitutionApplier.js:78:51)
    at /Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/mmp/MmpSubstitutionApplier.js:64:57
    at Array.forEach (<anonymous>)
    at MmpSubstitutionApplier.createParseNodeForInternalNode (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/mmp/MmpSubstitutionApplier.js:63:53)
    at EHypsDerivation.buildFormulaForCurrentEHypProofStep (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/stepDerivation/EHypsDerivation.js:78:75)
    at EHypsDerivation.searchCurrentEHypWithoutAdditionalVarsToBeUnified (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/stepDerivation/EHypsDerivation.js:87:53)
    at EHypsDerivation.searchEHypsRecursive (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/stepDerivation/EHypsDerivation.js:113:18)
    at EHypsDerivation.searchEHyps (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/stepDerivation/EHypsDerivation.js:128:18)
    at StepDerivation.tryEHypsDerivation (/Users/Thierry/.vscode/extensions/glacode.yamma-0.0.4/server/out/stepDerivation/StepDerivation.js:44:25)
[Info  - 22:45:37] Connection to server got closed. Server will restart.

[glacode]

I see. When it writes

I am back to the Main thread!!!!!!!

it means it has completed all parse trees, and then it can perform step derivation (filling missing labels)

(as far as I can tell, it takes 1 minutes and 6 seconds, on your machine)

So, the problem arises when step derivation is tried (if you unify earlier, it doesn't crash because it skips the "step derivation" attempt).

I have managed to reproduce the crash by waiting for 'step derivation' to become available.

Now I can look into it :-)

Thanks a lot. Glauco

[glacode]

Version 0.0.5 should have resolved the issue at hand.

Furthermore, I'd like to mention the new feature "$getproof ". Although it is still a work in progress and not flawless yet, it shows promise.

[tirix]

That sounds great! I'll try it ASAP.

[glacode]

the last commit does NOT address this issue, it addresses issue #6 (my mistake in the commit message)

[glacode]

@tirix isn't this issue fixed by ver. 0.0.5 ?

[tirix]

I have not seen this issue recently when using Yamma, so it can be closed. Thank you!