Re: [isabelle] Failing afp-2015 build



> Using the dangerous word "fix" means there is a lack of information what
> is really going on.  Maybe the author of the "vcg_jackhammer" proof
> method can look again and explain the situation.

Even if the AFP entry gets changed, we have a broader problem here. Let
me explain.

As Peter already said, there is no mention of "PARALLEL_GOALS" (or
related combinators) in the official documentation. The only relevant
mention we found is the following NEWS entry:

> * Refined PARALLEL_GOALS tactical: degrades gracefully for schematic
> goal states; body tactic needs to address all subgoals uniformly.

Additionally, there are only few occurrences in the visible Isabelle
universe: The distribution uses it in "clasimp" and "simp", and there
are only two more occurrences in the AFP which are not derived from what
is used in the distribution ("AWN" and "Slicing") *. Hence, the usual
heuristics of looking for canonical examples in the sources to figure
out how it should be used fails. (Also, both "AWN" and "Slicing" build
fine in single-threaded mode.)

Looking just at the implementation, it becomes obvious that the
sequential case stems from a – what I would call – "performance
optimization"; that is, if there is only one thread, there is no point
in setting up auxiliary goal states, so the inner tactic can proceed
undisturbed.

Now, there may very well be invariants which a tactic should fulfill in
order to make both the sequential and the parallel execution
observationally equivalent. My point is that this invariant – in
contrast to many others – are not checked in this combinator, which
allows for inconsistencies to sneak into the official AFP sources. Even
if the AFP entry gets edited in such a way that the usage of the
"PARALLEL_GOALS" combinator is canonical, there might be future
non-canonical uses which are difficult to detect (needless to say, ML
tactic code – while often being necessary – is hard to understand). In
fact, the are only two ways I can think of: Time-intensive review of ML
code or running entries in both single- and multi-threaded mode.

I'm a fairly young user on the general Isabelle time scale, but as far
as I remember, additional checks have been introduced quite often to
prevent the user from doing things which might "just work" but are not
intended to happen (e.g. context discipline). In my opinion the best way
to proceed is to both edit the AFP entry, and to either remove the
optimization in the combinator or add additional robustness checks. In
the case of the "ParallelGC" session, these two measures are independent
of each other.

Cheers
Lars


* There is one more occurrence in "Isabelle_Meta_Model", but that seems
like a copy of what happens in the simplifier.




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