Re: [isabelle] »strict« or »sequential« mode in Isabelle/jEdit?



The points reported by Florian trouble me less than the following, of which
only the first relates to jedit, but both relate to maintenance:

- Finding the error locations can be troublesome in big theories; somtimes the
presence of an error (in red) is only visible in the theory panel.

- Adjusting the AFP frequently leads me into the follwing situation: I run
"afp_build -A"; there is an error in some entry; I fix the error; I restart
"afp_build -A"; isabelle (more precisely java) dies with some out of memory
error right away, sometimes blaming it on a corrupt log file. At this point I
need to remove all log files and rerun *everything*.

I believe both points have been discussed already but I have no idea if I can
avoid the problem with the AFP.

Tobias

On 13/04/2014 15:17, Florian Haftmann wrote:
> During fine-point tuning of a huge bunch of theories (e.g. 
> Multivariate_Analysis / Probability in Isabelle/HOL), I am often in the 
> situation to incrementally adjust the sources following the error reporting
> of Isabelle/jEdit (e.g. adding a simp rule and adjusting subsequent broken
> proofs).
> 
> In this particular situation I experience two inconveniences with 
> continuous proof checking »as it is« in Isabelle/jEdit:
> 
> * The prover tries to work hard to give early feedback on the current focus
> of the edit panel, e.g. leaving proofs unfinished in earlier theories and
> so on.  Thus the (expected) spots of problems get reported quite late, and,
> after adjusting those spots, a lot of material which follows afterwards has
> to be re-checked.
> 
> * If existing proofs degenerate into non-termination, the risk is that 
> these spots will consume a lot of resources and turn Isabelle/jEdit little
> reactive until the spots are identified and interrupted by hard edits.
> 
> What works as workaround is to set the number of threads temporarily to 1.
> Beside the comparably deep path through GUI elements for switching back and
> forth, parallelism (e.g. wrt. complete theories) is entirely lost.
> 
> I'm not sure how relevant this is (how do other people experience such 
> situations?), but maybe there is a different approach to the whole scenaio
> which so far did not come to my mind.
> 
> Cheers, Florian
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.