Re: [polyml] ML debugging within Isabelle/PIDE

[Artella Coding]

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. 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. 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?

Thanks



On Mon, Feb 1, 2016 at 7:07 PM, Makarius  wrote:

> Dear users of the best unknown programming language in the world.
>
> Isabelle/ML is based on Poly/ML and thus benefits from the source-level
> debugger of that implementation of Standard ML. The Prover IDE provides the
> Debugger dockable to connect to running ML threads, inspect the stack frame
> with local ML bindings, and evaluate ML expressions in a particular
> run-time context.
>
> More explanations with a screenshot on
> http://sketis.net/2016/ml-debugging-within-the-prover-ide
>
>
> Makarius
> ___
> polyml mailing list
> polyml@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
>
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] ML debugging within Isabelle/PIDE

[Makarius]

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