The email claims that this build includes my patch. The log says:
> Running ConcurrentGC ... > ConcurrentGC: theory Model > ConcurrentGC: theory Tactics > ConcurrentGC: theory Proofs_basis > ConcurrentGC: theory TSO > ConcurrentGC: theory Handshakes > ConcurrentGC: theory MarkObject > ConcurrentGC: theory StrongTricolour > ConcurrentGC: theory Proofs > ConcurrentGC: theory Concrete_heap > ConcurrentGC: theory Concrete > *** Timeout > ConcurrentGC FAILED > (see also > /home/isatest/afp/isabelle-afp-poly/heaps/polyml-5.5.3_x86_64-darwin/log/ConcurrentGC) > > *** sys_mem_lock s = sys_mem_lock s'; > *** ALL a. > *** filter is_mw_Mark (sys_mem_write_buffers a s) = > *** filter is_mw_Mark (sys_mem_write_buffers a s'); > *** ALL p. WL p s = WL p s'; sys_heap s' x = Some a; ~ sys_fM s; > *** ~ sys_fM s'; obj_at (%obj. ~ obj_mark obj) xa s' |] > *** ==> obj_at (%obj. ~ obj_mark obj) xa s > *** 9. !!s s'. > *** [| ALL a. W (s a) = W (s' a); > *** ALL a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); > *** sys_fM s = sys_fM s'; > *** ALL b. > *** map_option obj_mark (sys_heap s b) = > *** map_option obj_mark (sys_heap s' b); > *** sys_mem_lock s = sys_mem_lock s'; > *** ALL a. > *** filter is_mw_Mark (sys_mem_write_buffers a s) = > *** filter is_mw_Mark (sys_mem_write_buffers a s') |] > *** ==> ALL p. WL p s = WL p s' > *** At command “done" (line 390 of > "/mnt/nfsbroy/home/isatest/afp/devel/thys/ConcurrentGC/MarkObject.thy") There is no “done” on line 390 of that file in the hg repo. This is the proof I repaired. So, err, what’s the connection between what’s in the email and what’s on the build box? > Begin forwarded message: > > From: isat...@macbroy2.informatik.tu-muenchen.de (Isabelle ) > Subject: test failed (Archive of Formal Proofs) > Date: 17 November 2015 22:13:20 GMT+7 > To: undisclosed-recipients:; > > Session [ConcurrentGC] in the automated afp test failed. > > AFP version: development -- hg id e6d87060e398 > Isabelle version: devel -- hg id 7ba83fbac0ae > Test ended on: macbroy2, Tue Nov 17 16:13:20 CET 2015. > > To reproduce the error, check out the development version of the > archive from sourceforge and run "isabelle make" on your session. > > This is an automatically generated email. To switch off these > notifications, edit thys/ConcurrentGC/config and hg commit and push the > changes. > > Have a nice day, > isatest -- http://peteg.org/ _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
