[isabelle] Parallel proofs issue, potentially in subst method



Dear Isabelle Users and Developers,

I have recently come across an issue when trying to improve the runtimes of our regression test server. When I ran it with -q 1, the times improved drastically, which was nice. When I ran it with -q 2 though, it didn't build at all. Those of you who know me will not be surprised to find it was in a theory I wrote :)

The issue affects building an image in non-interactive mode under Isabelle 2012 and a very recent development version (2267901ae911), in both 32-bit and 64-bit builds of PolyML versions 5.4.0, 5.4.1 and 5.4.2-dev. Breakage confirmed on three different physical machines.

Settings were:
ISABELLE_USEDIR_OPTIONS="-M 2 -p 0 -q 2 -v true"
but also confirmed to break with -M max and -p 1.

Please find attached the ROOT.ML, IsaMakefile and Loading.thy which replicates the issue in a distilled form building on HOL only. Run with:
isabelle make MAPPED_SEP

The error should be on the line attempting the subst:
*** exception THM 0 raised (line 758 of "thm.ML"):
*** forall_intr: variable "bs" free in assumptions
*** [| length bs = sz; P (Suc p) sz bs; p # Z = Z |]
*** ==> p # load_list_basic sz (Suc p) = Z
***   [!!]
*** At command "apply" (line 30 of "/home/rafalk/t/isa_bug/Loading.thy")

The issue is definitely due to some shadowing/renaming of the variable bs, but what else is going on is well beyond my current grasp of comprehension.

Sincerely,

Rafal Kolanski.
USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false

$(OUT)/MAPPED_SEP: *.thy *.ML
	$(USEDIR) -f ROOT.ML -b HOL MAPPED_SEP

MAPPED_SEP: $(OUT)/MAPPED_SEP

.PHONY: clean map_sep_clean
clean: map_sep_clean

map_sep_clean:

theory Loading
imports Main

begin

ML {* quick_and_dirty := true *}

consts
  load_list_basic :: "nat \<Rightarrow> nat \<Rightarrow> nat list"

lemma load_list_basic_app [simp]:
  "load_list_basic (Suc n) p = p # load_list_basic n (p + 1)"
  sorry

lemma smbaL_load_list_basic2:
  assumes lens: "length bs = sz"
  assumes pmap: "P p sz bs"
  shows "load_list_basic sz p = Z"
using lens pmap proof (induct sz arbitrary: bs p)
  case 0 thus ?case sorry
next
  case (Suc sz)
  hence IH: "\<And>bs p. \<lbrakk>length bs = sz; P p sz bs\<rbrakk>
                      \<Longrightarrow> load_list_basic sz p = Z"
    by auto

  show ?case
    apply -
    apply simp
    apply (subst IH)
    sorry
qed

end
use_thy "Loading";



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