[isabelle-dev] test failed (Archive of Formal Proofs)

Peter Gammie peteg42 at gmail.com
Tue Nov 17 16:41:43 CET 2015


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: isatest at 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/


More information about the isabelle-dev mailing list