Re: [isabelle] Refinement Framework exceeds resources ?

Hi Walther,

It does not help to start Isabelle in the right directory. You really have to specify the path to the ROOTS file of the AFP, either with -d or by adding it to some of the ROOTS files that are searched automatically. Security_Protocol_Refine works because it does not depend on other AFP entries.


On 27/10/17 10:37, Walther Neuper wrote:
Hi Andreas,

Thank you for hints!

I tried them and now suspect, that the reason for the problem is caused
by updating my computer from ubuntu 14.04 LTS to 16.04 yesterday.

Hoping that there are hints possible, how to spot the problem, I
describe my trials:
The screen shot, though, looks as if Isabelle cannot resolve the
imports. Have you told Isabelle at startup about the ROOT files in the
AFP, e.g., like this?

isabelle jedit -d <path-to-thys-dir-of_AFP>
I started Isabelle from the directory where the respective ROOT resides
and got stuck the same way again (shown in the attachment, I'd never
tried on the old ubuntu version).

So I created $ISABELLE_USER_HOME/etc/settings according to this
It looks as if the memory allocated to Isabelle/jEdit is too low. I
have the line

JEDIT_JAVA_OPTIONS="-Xms2048m -Xmx8192m -Xss8m"

in my settings file ($ISABELLE_USER_HOME/etc/settings), which allows
the JVM to use up to 8GB of RAM. My computer is not better than yours,
but I can load the refinement framework without problems.
and again got stuck the same way.

I also tried the AFP entry "Developing Security Protocols by Refinement"
again. This worked but seemed slower than on the old ubuntu version.

I am grateful for any hints,


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