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

Reply via email to