Re: [polyml] ML debugging within Isabelle/PIDE
On Thu, 4 Feb 2016, Artella Coding wrote: So if I return back to "Pure" mode in the Theories tab, is there any way for me to enter (via the debugger) the factorial function only at "factorial 100;"? Right now the factorial file contains the following code : = fun factorial 0 = 1 | factorial n = n * factorial (n - 1); factorial 10; factorial 100; factorial 1000; = and it seems that one has to recurse through (in the debugger) 10 calls of the factorial function (due to "factorial 10;") before one can step through invocations of the factorial function due to "factorial 100;". Is there any way to put a breakpoint at "factorial 100;" so that one only sees invocations of the factorial function due to "factorial 100;" and ignore the invocations of factorial due to the "factorial 10;" call? It is better to split the "static" part (the function definition) from the "dynamic" exploration of later expressions with the debugger. This avoids edits on the same file, and thus a reset of breakpoints, and confusion which expressions are meant to be under debugger control. For experimentation, I recommend Isabelle/ML and not official Standard ML, since it provides more possibilities that just SML_file. Given the task sketched above, I would do it like this (see the included Test.thy). Thus you get three running threads for each invocation of factorial. From the size of the stack, it is somehow possible to guess which is which evaluation. I presently don't know a way to restrict debugging individually, e.g. to interact with ML_val ‹factorial 100› only. Debugging is controlled at compile time for factorial once and for all. There is also some tension between continued editing and debugging: the latter lets the cursur jump around according to the program position; but the user might have something else in mind. Makariustheory Test imports Pure begin declare [[ML_debugger]] ML \ fun (**) factorial 0 = 1 | factorial n = n * factorial (n - 1); \ text \Open debugger panel, set breakpoint here: (**)\ text \Explore some expressions (independently via \<^theory_text>\ML_val\). This requires careful edits just before one of them, to ensure they are evaluated again (and under debugger control).\ ML_val \factorial 10\ ML_val \factorial 100\ ML_val \factorial 1000\ end ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] ML debugging within Isabelle/PIDE
So if I return back to "Pure" mode in the Theories tab, is there any way for me to enter (via the debugger) the factorial function only at "factorial 100;"? Right now the factorial file contains the following code : = fun factorial 0 = 1 | factorial n = n * factorial (n - 1); factorial 10; factorial 100; factorial 1000; = and it seems that one has to recurse through (in the debugger) 10 calls of the factorial function (due to "factorial 10;") before one can step through invocations of the factorial function due to "factorial 100;". Is there any way to put a breakpoint at "factorial 100;" so that one only sees invocations of the factorial function due to "factorial 100;" and ignore the invocations of factorial due to the "factorial 10;" call? Thanks On Thu, Feb 4, 2016 at 12:34 PM, Makarius wrote: > On Thu, 4 Feb 2016, Artella Coding wrote: > > 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. >> > > A change usually means that the relevant parts are re-compiled and > re-executed, but it is easier to think of both just as "evaluation". > Poly/ML acts more like a statically typed LISP system in this respect. > > In contrast, debugging means you interact with a running evaluation > process, without changing anything (neither the source nor the meaning of > the running program). > > > 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? >> > > The Prover IDE has no mode to do things "manually". Continuous checking > needs to be enabled to bring new sources and changes into the system. That > is relevant for evaluation of new material. > > The debugger does work without continuous checking on an already running > programm. I've checked this again in the implementation and by some > experiments. > > I don't think that non-continuous mode is very relevant for actual > debugging. It is more important when composing large ML modules, while > still thinking about the problem and not checking anything yet. > > > Makarius > > ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] ML debugging within Isabelle/PIDE
Hi, yes you are right. I closed all applications and reset the dropdown to HOL instead of pure. With everything closed the system was using 740 mb on 3 cores. Then upon building when "Hol theory Code_Evaluation" is reached, usage goes up to 3.7GB and then later goes down to 3.6GB. Then at "Hol: theory Complex_main" it goes back up to 3.7GB (by which time swap usage is 86%). Then after a long time memory usage goes down and this time the build is successful. Thanks On Thu, Feb 4, 2016 at 12:08 PM, Makarius wrote: > On Thu, 4 Feb 2016, Artella Coding wrote: > > I have 4GB allocated to my virtual machine (the laptop actually has 8GB) >> but selecting the "Pure" in the theories dropdown stops the HOL theories >> being build, which was what was consuming so much memory. Thanks >> > > Isabelle/HOL is big, but it should definitely build on 4GB in 64bit mode. > > Can you provide more VM parameters? Number of cores? Linux version? > > > Isabelle/HOL may be also seen as a benchmark for the PIDE. Using Pure as > a basis and loading $ISABELLE_HOME/src/HOL/Main.thy (with all its > requirements as proposed by the system), it loads tons of ML modules plus > surrounding theories. > > It is then possible to go to ML_file commands (e.g. via jEdit hypersearch > over all buffers), and follow the hyperlinks to the corresponding source > files. > > This requires definitely 8GB. > > Note that a shade of pink means the system is still working towards that > point of text. The Theories panel helps to keep an overview. > > > Makarius > ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] ML debugging within Isabelle/PIDE
On Thu, 4 Feb 2016, Artella Coding wrote: 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. A change usually means that the relevant parts are re-compiled and re-executed, but it is easier to think of both just as "evaluation". Poly/ML acts more like a statically typed LISP system in this respect. In contrast, debugging means you interact with a running evaluation process, without changing anything (neither the source nor the meaning of the running program). 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? The Prover IDE has no mode to do things "manually". Continuous checking needs to be enabled to bring new sources and changes into the system. That is relevant for evaluation of new material. The debugger does work without continuous checking on an already running programm. I've checked this again in the implementation and by some experiments. I don't think that non-continuous mode is very relevant for actual debugging. It is more important when composing large ML modules, while still thinking about the problem and not checking anything yet. Makarius ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] ML debugging within Isabelle/PIDE
On Thu, 4 Feb 2016, Artella Coding wrote: I have 4GB allocated to my virtual machine (the laptop actually has 8GB) but selecting the "Pure" in the theories dropdown stops the HOL theories being build, which was what was consuming so much memory. Thanks Isabelle/HOL is big, but it should definitely build on 4GB in 64bit mode. Can you provide more VM parameters? Number of cores? Linux version? Isabelle/HOL may be also seen as a benchmark for the PIDE. Using Pure as a basis and loading $ISABELLE_HOME/src/HOL/Main.thy (with all its requirements as proposed by the system), it loads tons of ML modules plus surrounding theories. It is then possible to go to ML_file commands (e.g. via jEdit hypersearch over all buffers), and follow the hyperlinks to the corresponding source files. This requires definitely 8GB. Note that a shade of pink means the system is still working towards that point of text. The Theories panel helps to keep an overview. Makarius ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] ML debugging within Isabelle/PIDE
I have 4GB allocated to my virtual machine (the laptop actually has 8GB) but selecting the "Pure" in the theories dropdown stops the HOL theories being build, which was what was consuming so much memory. Thanks On Wed, Feb 3, 2016 at 9:42 PM, Makarius 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
Re: [polyml] ML debugging within Isabelle/PIDE
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 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
Re: [polyml] ML debugging within Isabelle/PIDE
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
Re: [polyml] ML debugging within Isabelle/PIDE
On Wed, 3 Feb 2016, Artella Coding wrote: The build process which ends up consuming too much memory says : *** Isabelle build (polyml-5.6_x86_64-linux / jdk-8u72_x86_64_linux) Build started for Isabelle/HOL... Building HOL... HOL:theory ... ... *** Is there any way of configuring the maximum amount of memory this build process uses? If you only build Pure instead of HOL, the above is irrelevant. For big applications -- not just trying some ML -- you should install 32bit g++ libraries to allow Poly/ML running efficiently in the small address model. That sounds paradoxical, but is important: big Isabelle applications need small 32bit model to avoid requiring the double amount of heap space. Makarius ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] ML debugging within Isabelle/PIDE
The build process which ends up consuming too much memory says : *** Isabelle build (polyml-5.6_x86_64-linux / jdk-8u72_x86_64_linux) Build started for Isabelle/HOL... Building HOL... HOL:theory ... ... *** Is there any way of configuring the maximum amount of memory this build process uses? Thanks On Wed, Feb 3, 2016 at 9:15 AM, Artella Coding < artella.cod...@googlemail.com> 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. 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
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
[polyml] ML debugging within Isabelle/PIDE
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
