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 <makarius at sketis.net> 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