[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