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 <makar...@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 > >
_______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
