Re: [isabelle] using AFP

On 16.06.2014 20:04, Viorel Preoteasa wrote:
> Isabelle opens Complete_Lattice_Prop.thy, and this file does not have
> errors. Only the test file has the error. I tried some other random
> theory from AFP, and I get exactly the same behavior.

The AFP is nothing special from Isabelle's point of view. Does this
behaviour occur also with other imports (which are not in the same
directory as your theory)?

Does this behaviour occur if you specify the full path to the AFP-entry
instead of using $AFP (if you used $AFP before)?
Does this behaviour occur if you copy the files to another directory?

I am pretty sure your problem has a simple solution, but it is hard to
debug such things remotely ;)

> In the theory panel the the Test file is marked with red. When
> opening the test file Isabelle asks to open the files on which Test
> dependents,
> However after opening them it asks again about opening one of these
> files.
This happens sometimes for me, too. This seems to be a minor race
condition, but I never saw any negative consequences (except seeing the
dialog multiple times).

  -- Lars

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.