[isabelle-dev] Must the AFP be used as a component? (was: Reasons mira crashes)

[Lars Noschinski]

On 14.12.2012 10:12, Lars Noschinski wrote:
> On 14.12.2012 09:40, Lars Noschinski wrote:
>> On 28.11.2012 10:11, Lars Noschinski wrote:
>>> Hi everyone,
>>>
>>> mira still crashes from time to time. Sometimes, it is not a programming
>>> error, but some external error condition which could maybe be handled
>>> more gracefully:
>>
>> Next error condition: Isabelle fails to produce any heap image. I have
>> no idea what failed there (the commit on which it failed seems to be
>> working and the crash ),
>
> First I thought, the reason it failed was that it was still using an old
> version of Mira (16f40e322e50) from 9 months ago, still unaware of the
> changes related to the components. But even after updating the mira
> repository and restarting, it still fails.

Found the reason of the failure now. Mira executes

/bin/isabelle build -s -v -j 6 -d $PATH_TO_AFP/thys/ -g AFP

which then terminates with

Session Open_Induction (AFP)
Undefined environment variable: AFP
Finished at Fri Dec 14 10:41:25 CET 2012
0:00:17 elapsed time, 0:00:21 cpu time, factor 1.23

before anything was built (hence no data to collect for Mira, hence the 
crash).

The reason is that Open_Induction/ROOT (and also 
Open_Induction/Open_Induction.thy) relies on $AFP being set, which is 
only the case if AFP is registered as a component (which is not the case 
for Mira).

@Gerwin: Since you made the ROOT file, what was the intention of using 
$AFP instead of ../ used in all other theories?

Also, I wonder why this did not occur before ...

OT:  I just saw this: What is the reason for mira writing

    init_components "$COMPONENT/contrib" 
"$ISABELLE_HOME/Admin/components/main"

instead of

    init_components "$ISABELLE_HOME/contrib" 
"$ISABELLE_HOME/Admin/components/main"

to the settings file?

   -- Lars