Re: [isabelle] Failing afp-2015 build



On Thu, 12 Nov 2015, Lars Hupel wrote:

As Peter already said, there is no mention of "PARALLEL_GOALS" (or related combinators) in the official documentation.

I was actually under the impression that a small paragraph about that was already in the relevant manuals, but that is not the case. It will happen eventually. (I am committed to keep the important reference manuals up-to-date, but the massive amount of material is already a problem; many people just ignore the manuals, either passively or actively.)


Anyway, official documentation is also the ML source and the cumulative NEWS file.

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.

Doing an exhaustive hypersearch on NEWS in Isabelle2015 provides the following bits of information:

  Isabelle2009-1 (December 2009)

  * PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
  parallel tactical reasoning.


  Isabelle2011-1 (October 2011)

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


  Isabelle2015 (May 2015)

  * Tactical PARALLEL_ALLGOALS is the most common way to refer to
  PARALLEL_GOALS.


This provides a glimpse on the typical bottom-up construction of new Isabelle concepts. We start with something we know already (Par_List.map) and work our way through further system structures, e.g. tactical reasoning with goal and subgoal addressing.

You probably know that the Larry-Paulson-goal-state is great in many respects, but also more concrete than semantically intended. This means ML tactics and Isar proof methods need to be "well-behaved" in certain ways. This is quite explicitly documented in the "implementation" manual, but I still see violations routinely in Isabelle applications. The proof parallelization occasionally changes the representation of goal states, and tactic expressions seen in the wild break down.

The present situation seems to be much less spectacular, though.


For the PARALLEL_GOALS, the October 2011 NEWS snipped says "body tactic needs to address all subgoals uniformly". This means it needs to ignore the accidental number of subgoals that it sees, and operate on all subgoals that happen to be there, e.g. like simp_all.

Since it already turned out a bit impractical to take this extra condition into account in applications, and all concrete uses were using ALLGOALS, the May 2015 version formalizes that situation by a new PARALLEL_ALLGOALS combinator and makes it "the most common way" in the NEWS.


The ConcurrentIMP session was added before the Isabelle2015 release, where PARALLEL_ALLGOALS was not yet available as canonical shortcut. Thus it fell into the gap of the historical confusion of what PARALLEL_GOALS really means.

So this is just a routine case of updating existing AFP entries. What is less routine is the total run-time of that session, which makes maintenance more difficult. I have already reduced it a lot by using the newer 'subgoal' Isar command, but that is for the next Isabelle release.


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

I will standardize all occurrences, but only in afp-devel.


	Makarius




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