Re: [isabelle-dev] Future of isatest/afptest

[Peter Gammie]

On 19 Nov 2015, at 00:18, Lars Hupel  wrote:
> 
> […]

Lars, that all sounds awesome.

Reckon you could make the status of the builds somehow public?

(Right now I don’t know whether my patch to ConcurrentGC works or not, because 
I only get failure emails and don’t know when a build is run. I know, I should 
learn to stop worrying and love the silence. :-)

cheers,
peter
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Peter Gammie]

On 17 Nov 2015, at 22:50, Lars Hupel  wrote:
> 
>> The email claims that this build includes my patch.
> 
> according to the log the AFP id is e6d87060e398, which doesn't include
> your patch (82552632a098). Or are you talking about another patch?

Nope, that’s the one. Thanks! Sorry for the noise.

My hg foo is weak. :-) Just be glad I didn’t blow up the whole repo somehow.

So… I guess we find out tomorrow if that fixes^Wrepairs things.

cheers,
peter
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Peter Gammie]

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

[isabelle-dev] extra lemmas

[Peter Gammie]

Can someone add these in at the obvious places?

thanks,
peter

lemma LeastI2_wellorder_ex:
  assumes "\x::'a::wellorder. P x"
  and "\a. \ P a; \b. P b \ a \ b 
\ \ Q a"
  shows "Q (Least P)"
using assms by clarify (blast intro!: LeastI2_wellorder)

lemma fcomp_comp: "fcomp f g = comp g f" by (simp add: ext)

lemma drop_rev:
  "drop n (rev xs) = rev (take (length xs - n) xs)"
by (cases "length xs < n") (auto simp: rev_take)

lemma take_rev:
  "take n (rev xs) = rev (drop (length xs - n) xs)"
by (cases “length xs < n") (auto simp: rev_drop)

HOL/Library/Permutation:

lemma perm_finite[simp, intro!]:
  "finite {B. B <~~> A}"
proof(rule finite_subset[where B="{xs. set xs \ set A \ length 
xs \ length A}"])
  show "finite {xs. set xs \ set A \ length xs \ length A}"
apply (cases A, simp)
apply (rule card_ge_0_finite)
apply (auto simp: card_lists_length_le)
done
next
  show "{B. B <~~> A} \ {xs. set xs \ set A \ length 
xs \ length A}"
by (clarsimp simp add: perm_length perm_set_eq)
qed

lemma perm_swap:
  assumes "i < length xs"
  assumes "j < length xs"
  shows "xs[i := xs ! j, j := xs ! i] <~~> xs"
using assms by (simp add: mset_eq_perm[symmetric] mset_swap)

-- 
http://peteg.org/

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

[Peter Gammie]

Hi,

Can someone please apply the attached patch to Isabelle for me?

It does three things:
- generalises Imperative_Quicksort to work on linearly-ordered, 
heap-representable types, and not just nat
- renames Sublist to List_Sublist to avoid clashing with HOL/Library/Sublist
- mildly weakens the assumptions of lemma subarray_append in theory Subarray

The first may require existing theories to add type annotations. If this is a 
concern then perhaps the right thing to do is introduce new names for the 
polymorphic operations and preserve the existing ones, but I think that is 
overkill.

The second may also break existing theories but I do not know how to otherwise 
get around having two theories with the same name.

thanks,
peter


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

[Peter Gammie]

… and this time with the patch …

> On 15 Nov 2015, at 22:15, Peter Gammie <pete...@gmail.com> wrote:
> 
> Hi,
> 
> Can someone please apply the attached patch to Isabelle for me?
> 
> It does three things:
> - generalises Imperative_Quicksort to work on linearly-ordered, 
> heap-representable types, and not just nat
> - renames Sublist to List_Sublist to avoid clashing with HOL/Library/Sublist
> - mildly weakens the assumptions of lemma subarray_append in theory Subarray
> 
> The first may require existing theories to add type annotations. If this is a 
> concern then perhaps the right thing to do is introduce new names for the 
> polymorphic operations and preserve the existing ones, but I think that is 
> overkill.
> 
> The second may also break existing theories but I do not know how to 
> otherwise get around having two theories with the same name.
> 
> thanks,
> peter



Imperative_HOL.patch
Description: Binary data

-- 
http://peteg.org/

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle and AFP

[Peter Gammie]

Florian,

Amongst the set/pred emails this one doesn't seem to have garnered much 
response:

On 17/08/2011, at 9:18 PM, Florian Haftmann wrote:

 I repeatedly stumble over duplication among the Isabelle distribution
 and the AFP [..]

I too would be keen to see some way of moving reusable (especially small) parts 
of AFP entries into Isabelle proper. Typically I need a few minor lemmas that 
make me wonder if everyone else has proved them already...

Concretely we see this presently with the saturated naturals theory that you 
want me to clean up. (Soon, I hope. :-)

cheers
peter
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev