Hi, so I selected "Pure" in the dropdown in the "Theories" tab, and now isabelle/HOL does not try to build the theories anymore, which is good.
Now I can debug /src/Tools/SML/factorial.sml with the debugger stopping in the factorial function everytime I make a change to the file.
If I untick the "Continuous checking" in the "Theories" tab, upon changing the factorial.sml file, the debugger no longer gets activated. How do I manually compile and run the factorial.sml file, when the "Continuous checking" box is unticked?
Thanks
On Wed, Feb 3, 2016 at 9:42 PM, Makarius <makarius at sketis.net> wrote:
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