MMTSyntaxPresenter presents OMIDs incorrectly short

[ComFreek]

Consider the meta datum keys in the following presented constant:

judgement  
     : (Pi [V:vocabulary] (Pi [Γ:(apply  Ctx V)] (arrow  (apply  Expr Γ) (arrow  (apply  Expr Γ) prop))))
  ❘ = (lambda [V:vocabulary] (lambda [Γ:(apply  Ctx V)] (lambda [e:(apply  Expr Γ)] (lambda [E:(apply  Expr Γ)] (apply  foo bar)))))
  ❘ role simplify
  ❘ @ jud
  ❘ @ judgment
  ❘ # 1 |- 2 ∶ 3 prec 100
  ❘ meta metakey1 ?MMTSyntaxPresenterTestBar
  ❘ meta metakey2 (f  x)
❙

They should actually be ?metakey1 and ?metakey2. I don't know where the code is wrong (probably in NotationBasedPresenter?), perhaps @Jazzpirate knows.

A ready and runnable unit test is at info.kwarc.mmt.api.presentation.MMTSyntaxPresenterTest in mmt-lf module (test directory)

(This is the only bug preventing FrameIT from outputting valid MMT surface syntax for the situation theory :smile:)

[Jazzpirate]

They should actually be ?metakey1 and ?metakey2.

...are you sure about that? That feels wrong to me...

This is the only bug preventing FrameIT from outputting valid MMT surface syntax

Are we sure FrameIT should output MMT surface syntax? That also feels wrong to me...

[ComFreek]

...are you sure about that? That feels wrong to me...

I now agree that meta metakey1 ... is correct, but still, what if the meta key comes from another theory that is not included?

With my latest changes to the unit test, https://github.com/UniFormal/MMT/blob/225edea57f6c9e43b44f598c3e25fc0aaf63b5e8/src/mmt-lf/test/scala/info/kwarc/mmt/api/presentation/MMTSyntaxPresenterTest.scala#L97-L105, the presenter still outputs meta metakey2 ... instead of meta ?MMTSyntaxPresenterTestBar?metakey2 ... where MMTSyntaxPresenterTestBar is a theory totally unrelated to the home of the constant that has these metadatums.

Are we sure FrameIT should output MMT surface syntax? That also feels wrong to me...

For debugging purposes, I am pretty sure. And perhaps later to save level state in a user-editable way.

[Jazzpirate]

So, the the first thing I notice is that the MMTSyntaxPresenter should actually use notations rather than names.

For the metakeys, they probably have no notations, so it uses the names instead. That's fine, since names are notations, too. It only gets problematic if there is more than one constant in scope with the same name. Then things get tricky...

Is that the case? Is there more than one metakey1?

[Jazzpirate]

Also, I just noticed:

what if the meta key comes from another theory that is not included?

then your theory is invalid and should throw errors when checking already. No guarantees what the presenter does to invalid theories ;)

[ComFreek]

So, the the first thing I notice is that the MMTSyntaxPresenter should actually use notations rather than names.

Well, in the paste above, I guess my handcrafted theory didn't have ur:?LF in-scope (transitive as either meta or included theory), thus the notations weren't picked up. But it does in general pick up notations, I verified that.

It only gets problematic if there is more than one constant in scope with the same name. Then things get tricky...

Is that the case? Is there more than one metakey1?

Not in my cases and I think colliding constant names is a general problem of the presenter. I haven't really encountered that personally and I don't have an agenda to make the presenter aware of cases that I don't even have a need for so far :smile:

No guarantees what the presenter does to invalid theories ;)

I see.

Thanks for your replies, closing this issue now!