Relative URIs sometimes not relative enough

[ComFreek]

• meta keys:

  theory MetaKeyTest : ur:?LF =
    symbol: type ❙
    usage: type ❘ meta ?symbol ?symbol ❙
  
    // only `meta ?MetaKeyTest?symbol ?symbol` works ❙
  ❚
  

- in includes:

theory OuterTheory =
  theory InnerTheory1 = ❚
  theory InnerTheory2 = include ?InnerTheory1 ❙ ❚

  // only `include ?OuterTheory?InnerTheory1` works ❙
❚

[Jazzpirate]

1. I can't say anything about metakeys, I have no idea how URI's are resolved there. It's quite possible that they should always be absolute.
2. The first example is perfectly intended, except if there isn't a typo in your example :D It should be ?OuterTheory/InnerTheory1, since that is the actual name of the theory. ?OuterTheory?InnerTheory1 is the URI coresponding to the declaration in ?OuterTheory that corresponds to the nested theory, which - as a declaration - is not technically a theory at all. It might be that it still works as syntactic sugar, but in my opinion it shouldn't. Would be interesting to see what happens if there are some actual constants in InnerTheory1 and whether they're even available in InnerTheory2 if you include the declaration.
   Either way ?InnerTheory1 alone should not work, since there's no theory by that name - but there could be one (outside of ?OuterTheory), which it would refer to if that existed.

[ComFreek]

Thanks. --> added documentation label: document how inclusions and nested modules have in a StackExchange Q&A

The issue on meta keys is still open.

[florian-rabe]

I've never specified relative to what the keys are resolved. I had a feeling that metadata might live in scopes somehow orthogonal to the rest, but I never followed up on that.