Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Refinement Framework exceeds resources ?

Email Gateway (Aug 22 2022 at 16:10):

From: Makarius <makarius@sketis.net>
Do you have the Ubuntu package lib32stdc++6 installed? Otherwise Poly/ML
uses x86_64 mode and requires much more heap space.

Makarius

Email Gateway (Aug 22 2022 at 16:11):

From: Walther Neuper <wneuper@ist.tugraz.at>
It is installed now, thank you.

Further evaluation has to wait until I have solved my imports problem.

Walther

Email Gateway (Aug 22 2022 at 16:20):

From: Walther Neuper <wneuper@ist.tugraz.at>
Supposed my computer (attached Screenshot-mycomputer.png) would be
sufficient for Isabelle.

But loading "The Imperative Refinement Framework" gets stuck with a last
movement of the red progress bar in "Multiset", see attached
Screenshot-aft-refine.png.

Am I out of resources ?

Walther
Screenshot-mycomputer.png
Screenshot-afp-refine.png

Email Gateway (Aug 22 2022 at 16:20):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Walther,

Your computer configuration looks OK to me. 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.

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>

Hope this helps,
Andreas

Email Gateway (Aug 22 2022 at 16:20):

From: Walther Neuper <wneuper@ist.tugraz.at>
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,

Walther
Screenshot-afp-refine.png

Email Gateway (Aug 22 2022 at 16:20):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.

Andreas

Last updated: Apr 16 2024 at 12:28 UTC