jomdoc validate --symlinks has a problem with nested theories.

[kohlhase]

If we run linktest on  https://svn.omdoc.org/repos/omdoc/trunk/examples/logics/pl0.omdoc, we get

WARN : redundant import /Users/kohlhase/vc/svn/omdoc.org/omdoc/trunk/examples/logics/qbf.omdoc#qbf
 in theory /Users/kohlhase/vc/svn/omdoc.org/omdoc/trunk/examples/logics/pl0.omdoc#and-prop.thy
----------------------------------------------------
 WARN : redundant import /Users/kohlhase/vc/svn/omdoc.org/omdoc/trunk/examples/logics/qbf.omdoc#qbf
 in theory /Users/kohlhase/vc/svn/omdoc.org/omdoc/trunk/examples/logics/pl0.omdoc#xor-prop.thy
----------------------------------------------------
 WARN : redundant import /Users/kohlhase/vc/svn/omdoc.org/omdoc/trunk/examples/logics/qbf.omdoc#qbf
 in theory /Users/kohlhase/vc/svn/omdoc.org/omdoc/trunk/examples/logics/pl0.omdoc#tnd.thy
----------------------------------------------------
 WARN : redundant import /Users/kohlhase/vc/svn/omdoc.org/omdoc/trunk/examples/logics/qbf.omdoc#qbf
 in theory /Users/kohlhase/vc/svn/omdoc.org/omdoc/trunk/examples/logics/pl0.omdoc#or-prop.thy
----------------------------------------------------
 WARN : redundant import /Users/kohlhase/vc/svn/omdoc.org/omdoc/trunk/examples/logics/qbf.omdoc#qbf
 in theory /Users/kohlhase/vc/svn/omdoc.org/omdoc/trunk/examples/logics/pl0.omdoc#implies-prop.thy

but as far as I can tell, they are legitimate; indeed, if I take the import statements out, linktest will complain about missing imports.

[dmisev]

But there seems to be a circular imports:

dimitar@debian:~/kwarc/omdoc/examples/logics$ jomdoc transform --flatten-theories pl0.omdoc
Circular imports found in theory file:/home/dimitar/kwarc/omdoc/examples/logics/pl0.omdoc#pl0
/home/dimitar/kwarc/omdoc/examples/logics/pl0.omdoc#pl0 <-
/home/dimitar/kwarc/omdoc/examples/logics/qbf.omdoc#qbf <-
/home/dimitar/kwarc/omdoc/examples/logics/pl0.omdoc#pl0
jomdoc: circular imports found, terminating flattening

--flatten-theories works in a bit different way than validate --imports, I still haven't changed the validation to use this.

I'm just not sure if this is actually a circle, A is the outer theory (= pl0.omdoc#pl0), B is an inner theory of A which imports C (C = qbf.omdoc#qbf), where C imports again A?

[kohlhase]

Dimiatar,

thanks for the analysis, I see the picture as the following (please forgive my ASCII art:

I
|\
| Q
|/
P

wherer Q=QBF and P=PL0 and I is the inner theory in P. By definition I imports P (since it is inner) and Q imports P as declared and I imports Q as declared. So validate --imports is correct to say that we have a redundant import (the left vertical one). But it erraneously reports a missing import if we remove that (I guess it does not take the (I imports P by definition of inner theories) into account.

Indeed there is not cycle here, the --flatten-theories gets it wrong.

[dmisev]

But this is a bit confusing when you say I imports P by definition. I always thought it's the other way around (P imports I) since P actually contains I, and I inherits from P everything up to the point where it's defined in P, this is how it works in jomdoc. I'm quite confused now :)

[kohlhase]

Maybe we only have a misunderstanding of what "A imports B" means? For me that means that all statements and symbols in B are visible in A as well. With your explanation this is what you understand the situation to be as well.

Having agreed on this, I think you will also agree that there must still be some problem with the implementation as in my explanation above right?