yamma/unify : No result returned

[tirix]

Hi Glauco!

I'm sorry I have not yet been able to get a unification proposal. Here is the detailed trace extract:

[18:52:49 GMT+0200 (Central European Summer Time)] createLabelToParseNodeForThreadMap - 97%
[18:52:49 GMT+0200 (Central European Summer Time)] createLabelToParseNodeForThreadMap - 98%
[18:52:50 GMT+0200 (Central European Summer Time)] createLabelToParseNodeForThreadMap - 99%
[Trace - 18:52:59] Sending request 'yamma/unify - (6)'.
Params: [
    "file:///Users/Thierry/Git/set.mm/test.mmp"
]

[Trace - 18:52:59] Received response 'yamma/unify - (6)' in 8ms.
No result returned.

[Trace - 18:52:59] Received request 'workspace/applyEdit - (15)'.
Params: {
    "edit": {
        "changes": {
            "file:///Users/Thierry/Git/set.mm/test.mmp": []
        }
    }
}

[Trace - 18:52:59] Sending response 'workspace/applyEdit - (15)'. Processing request took 1ms
Result: {
    "applied": false
}

It seems unify does not return any result.

[glacode]

How is your test.mmp code?

If a label is to be inferred, you should wait a couple of minutes before "step derivation" is ready.

It has to parse every statement in set.mm, and it is done in a "true" separate working thread.

I could split it in chunks so that "simple" derivation are available early.

The two minutes are paid only once, when set.mm is loaded.

[tirix]

Here's the test.mmp I've used:

$( <MM> <PROOF_ASST> THEOREM=sacgr  LOC_AFTER=?

* Supplementary angles of congruent angles are themselves congruent.
  Theorem 11.13 of [Schwabhauser] p. 98.  (Contributed by Thierry
  Arnoux, 30-Sep-2020.)

h1::dfcgra2.p                                          |- P = ( Base ` G )
h2::dfcgra2.i                                          |- I = ( Itv ` G )
h3::dfcgra2.m                                           |- .- = ( dist ` G )
h4::dfcgra2.g                                           |- ( ph -> G e. TarskiG )
h5::dfcgra2.a                                           |- ( ph -> A e. P )
h6::dfcgra2.b                                           |- ( ph -> B e. P )
h7::dfcgra2.c                                           |- ( ph -> C e. P )
h8::dfcgra2.d                                           |- ( ph -> D e. P )
h9::dfcgra2.e                                           |- ( ph -> E e. P )
h10::dfcgra2.f                                          |- ( ph -> F e. P )
h11::sacgr.x                                            |- ( ph -> X e. P )
h12::sacgr.y                                            |- ( ph -> Y e. P )
h13::sacgr.1                                            |- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
h14::sacgr.2                                               |- ( ph -> B e. ( A I X ) )
h15::sacgr.3                                                 |- ( ph -> E e. ( D I Y ) )
h16::sacgr.4                                                |- ( ph -> B =/= X )
h17::sacgr.5                                               |- ( ph -> E =/= Y )

!qed:?:r19.29vva                                  |- ( ph -> <" X B C "> ( cgrA ` G ) <" Y E F "> )

I'm positioned on the last, qed line and press Ctrl+U. I've tried different options with/without exclamation mark, question mark, label.

[glacode]

The extension is not working, you should get an error diagnostic here at the first line

$(

Yamma doesn't use the mmj2

$( THEOREM=sacgr LOC_AFTER=?

approach, it automatically generates

$theorem test

as a first line and (if the comment is missing)

• MissingComment

as a second line.

It looks like something went wrong with my last two commits (marketplace related)

If I revert to commit

3361d6822d460eb65435cfd92eb36d830ed1b005

it works.

[glacode]

Thierry,

please try version 0.0.3 and let me know

(I replaced the language id from yamma to Yamma and that screwed up everything)

I have to understand how to get Yamma in the marketplace without uppercasing the language id (I guess there should be a Title field or something like that)

[tirix]

Yes it worked with version 0.0.3!

I can see unification, hovers, and syntax highlighting working. Thanks for your help!

I'm closing this issue, and I'll try out more!