[isabelle-dev] Bad theory import "Main"

[Makarius]

On 24/04/17 14:36, Makarius wrote:
> On 23/04/17 18:10, Blanchette, J.C. wrote:
>>
>> *** No such file: "/Users/blanchette/isabelle/src/HOL/Library/Fraction_Field.thy"
>> *** The error(s) above occurred for theory "HOL-Lib.Fraction_Field" (line 17 of "/Users/blanchette/hgs/isafor/thys/ROOT")
> 
> The transition from unqualified theories to qualified theories is not
> smooth -- there can be intermediate situations, where certain sessions
> cannot import certain theories anymore.
> 
> The emerging tool "isabelle imports" tools helps to sort out the
> situation, but it requires some care to use it and I am still exploring
> the overall situation.

The situation is actually more basic: src/HOL/Library/Fraction_Field.thy
etc. were moved to a separate session in fc41a5650fb1 and thus you have
a broken IsaFoR still lying around by accident.

What I said about "isabelle imports" is not yet relevant (presently at
10f4a17e5928), because I did not move that far ahead yet -- although I
was pondering when to do it.

(Right now I have the impression that there is an aversion to any kind
of change on the ever changing isabelle-dev repository. We are between
the releases and now is the usual time for bigger reforms. Or are we
already in a state where big things can no longer happen?)


	Makarius