On Wed, 3 Feb 2016, Artella Coding wrote:
Hi, I thought I would give this a try (I know nothing about Isabelle or
HOL). So I downloaded the executable at
http://isabelle.in.tum.de/website-Isabelle2016-RC3/ and then ran
./Isabelle2016-RC3
At first it started building loads of files but I ran out of memory so
had to stop that building.
How much memory do you have? It should work even for small machines with
only 4GB, like my old Mac Book Pro from 2009. Somehow I did not expect
anybody to try a full-scale "IDE" on a very small Netbook with less than
that. It does not make much sense to work with less than 2 cores + 4 GB.
For doing a little ML, you don't need the big and bulky HOL session,
though. You can select "Pure" in the Sessions panel and restart.
Then I noticed a src/Tools/SML/Examples.thy in the "Examples" dropdown
in the "Documentation" tab on the right. So clicking this opens the
file, but I am not sure how to compile and run this file.
Poly/ML is an incremental run-time compiler, and the IDE directly supports
that model. You edit, and the system immediately reacts on it. As in a
word processor with spell-checking, but here it is a bit more.
I looked at some online videos but they didnt really help. So how do I
compile and run the src/Tools/SML/Examples.thy file?
You need the active prover session for that, i.e. a startup build that
works.
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
