Re: [isabelle] Jinja-Threads build problem



Finally, I broke down the problem to a strange behaviour of
Proof-General:

Take the following minimal example:
  theory A
  imports Main  
  begin
    ML_val {*
      tracing "Looping ...";
      fun f a = f a;
      f 1
      *}
  end

  theory B imports A
  begin

  end

Then use PG to load theory B. It will happily do so, ignoring that the
ML_val command is still running. Actually, the ML_val command is
started, and still running when PG displays the theory as processed.

However, when loading the theory A with PG, it gets stuck at the ML_val
command as expected.

What has happened here? Is this a problem of PG, or of some
Isabelle-stuff used elsewhere (As PG does not do loading of required
theories itself, I suspect the problem lies somewhere in Isabelle)

This raises another question about the semantics of ML_val:
  Is a theory correct, where some ML-val command diverges?

--
  Peter

p.s.
  The diverging ML_val command was introduced by my changes, that
accidently produced a code equation of the form "f a b = f a b"





On Do, 2013-10-17 at 13:25 +0200, Peter Lammich wrote:
> email message attachment (Jinja-Threads build problem), "Forwarded
> message - Jinja-Threads build problem"
> > -------- Forwarded Message --------
> > From: Peter Lammich <lammich at in.tum.de>
> > To: Isabelle Group (TUM) <isabelle-group at in.tum.de>
> > Cc: Andreas Lochbihler <andreas.lochbihler at kit.edu>
> > Subject: Jinja-Threads build problem
> > Date: Thu, 17 Oct 2013 12:30:35 +0200
> > 
> > Refering to Isabelle2013-1-RC2
> > 
> > Hi all.
> > 
> > I have done some modifications to the Collection framework, and adapted
> > JinjaThreads.
> > 
> > In Proof-General, I can load JinjaThreads.thy within half an hour or so.
> > Jedit seems to get stuck, it already runs for 2 hours when I write this
> > mail, without any visible progress.
> > 
> > However, when I try 
> >   isabelle build -j 10 -v -D JinjaThreads
> > 
> > it writes that it loads all theories, and then gets stuck. The last
> > output is:
> > 
> > [...]
> > JinjaThreads: theory JMM_Compiler_Type2
> > JinjaThreads: theory JMM
> > JinjaThreads: theory MM_Main
> > JinjaThreads: theory JinjaThreads
> > 
> > At this point, it gets stuck (>10h on lxbroy10, before I cancelled the
> > job)
> > 
> > 
> > What might have happened here? Does the build-tool write some log-file
> > where I can inspect what happened?
> > 
> > On the original JinjaThreads, the build tool finishes a few seconds
> > after the last line has been output.
> > 
> > As the number of theories that JinjaThreads depends on has increased due
> > to my modification: Is there some size-limit that I might have hit?
> > 
> > I have attached a zip-file, that contains the modified version of
> > JinjaThreads and all (modified) prerequisites in the folder "Lib".
> > 
> > Any hints or help is appreciated.
> > 
> > Best,
> >   Peter






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