Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

[Florian Haftmann]

For the record:

> Running on host lxbroy10
> isabelle: fc53fbf9fe01 tip
> afp: 835c7e115feb tip
> Running ConcurrentGC ...
> Finished ConcurrentGC (1:08:48 elapsed time, 5:15:14 cpu time, factor 4.58)
> 1:21:59 elapsed time, 5:53:13 cpu time, factor 4.30

This seems to be fine now.

Florian

Am 16.11.2015 um 17:17 schrieb Peter Gammie:
> For:
> 
> isabelle: e6784939d645
> afp: e6d87060e398
> 
> the attached patch makes ConcurrentGC go through under Isabelle/JEdit. I 
> waited ~ 4 CPU hours for the batch build before killing it. I cannot read the 
> log files that Isabelle generates now, so I do not know what proof I 
> interrupted. Sorry about that. I’ve attached the log in case it has value to 
> someone. The log from isatest also does not have enough useful context.
> 
> It seems that the simplifier got smarter about the option datatype.
> 
> cheers,
> peter
> 
> 
> 
> 
> 
>> On 15 Nov 2015, at 16:38, Florian Haftmann 
>>  wrote:
>>
>> isabelle: f1b257607981 tip
>> afp: 1a688183b05a tip
>>
>> Any idea what is going on here?
>>
>>  Florian
>>
>> -- 
>>
>> PGP available:
>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

[Florian Haftmann]

Thanks to all who have invested time and energy to work on those issues.

Nevertheless I have the impression that in the last time there have have
been lots of movements in the distribution being speculative in the
sense that no systematic testing including the AFP had taken place.

What is the reason for this?  No access to suitable computing machines?

Cheers,
Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

[Lars Hupel]

Hi Florian,

> What is the reason for this?  No access to suitable computing machines?

currently, the "new" testboard only performs "makeall" on the
distribution. As I wrote in my mail from yesterday, I'm working on it. I
expect to be able to make a recommendation on how to reinstate regular
testing within this week.

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

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

[Lawrence Paulson]

I am partly to blame. The changes involving the “real” function caused a lot of 
disruption. I needed a week to get all of Isabelle/HOL working again, and 
thought it a more practical option to tackle the AFP failures after they 
occurred. Most of them were only out of action for a day.

Larry

> On 19 Nov 2015, at 09:16, Florian Haftmann 
>  wrote:
> 
> Thanks to all who have invested time and energy to work on those issues.
> 
> Nevertheless I have the impression that in the last time there have have
> been lots of movements in the distribution being speculative in the
> sense that no systematic testing including the AFP had taken place.
> 
> What is the reason for this?  No access to suitable computing machines?
> 
> Cheers,
>   Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

[Johannes Hölzl]

Am Sonntag, den 15.11.2015, 11:43 +0100 schrieb Andreas Lochbihler:
> Vickey_Clarke_Groves looks related to the changes to "real", but I
> have not tried to fix this.

This should be fixed now in AFP e6d87060e398.

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

[isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

[Florian Haftmann]

isabelle: f1b257607981 tip
afp: 1a688183b05a tip

Any idea what is going on here?

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Running ConcurrentGC ...
Running MonoBoolTranAlgebra ...
Running Presburger-Automata ...
Running Vickrey_Clarke_Groves ...

MonoBoolTranAlgebra FAILED
(see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.5.3_x86-linux/log/MonoBoolTranAlgebra)

Output written on root.pdf (20 pages, 176819 bytes).
Transcript written on root.log.

*** Failed to apply proof method (line 465 of "/mnt/home/haftmann/data/tum/afp/master/thys/MonoBoolTranAlgebra/Mono_Bool_Tran.thy"):
*** goal (3 subgoals):
***  1. !!xa. [| ALL xa. x xa <= xa;
***  x : disjunctive.disjunctive op \ op \
***   (%f. f);
***  x \ = x xa \ x (- xa) |]
***   ==> x (- xa) <= \
***  2. !!xa. [| ALL xa. x xa <= xa;
***  x : disjunctive.disjunctive op \ op \
***   (%f. f);
***  x \ = x xa \ x (- xa) |]
***   ==> - xa \ xa <= x xa
***  3. !!xa. [| ALL xa. x xa <= xa;
***  x : disjunctive.disjunctive op \ op \
***   (%f. f) |]
***   ==> x \ = x xa \ x (- xa)
*** At command "apply" (line 465 of "/mnt/home/haftmann/data/tum/afp/master/thys/MonoBoolTranAlgebra/Mono_Bool_Tran.thy")

Vickrey_Clarke_Groves FAILED
(see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.5.3_x86-linux/log/Vickrey_Clarke_Groves)

***   real
***(setsum
***  (summedBidVector (pseudoAllocation a <| (N <*> finestpart G)) N G) aa)
***   < real
***  (setsum
***(summedBidVector (pseudoAllocation a <| (N <*> finestpart G)) N G) a)
***   x <= real (card G)
***   0 <= x
***   (x = 0) = (a = aa)
*** goal (1 subgoal):
***  1. x <= real (card G) &
*** 0 <= x &
*** (x = 0) = (a = aa) &
*** (aa ~= a -->
***  setsum
***   (summedBidVector (pseudoAllocation a <| (N <*> finestpart G)) N G) aa
***  < setsum
*** (summedBidVector (pseudoAllocation a <| (N <*> finestpart G)) N G)
*** a)
*** At command "by" (line 985 of "/mnt/home/haftmann/data/tum/afp/master/thys/Vickrey_Clarke_Groves/UniformTieBreaking.thy")
*** Timeout
Presburger-Automata FAILED
(see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.5.3_x86-linux/log/Presburger-Automata)

  assumes "rquot_DFS A n"
Found termination order: "(%p. size_list size (snd p)) <*mlex*> {}"
Found termination order:
  "(%p. size (snd p)) <*mlex*> (%p. size (fst p)) <*mlex*> {}"
### Ignoring duplicate rewrite rule:
### accepts ?tr1 ?P1 ?s1 ?as1 == ?P1 (foldl ?tr1 ?s1 ?as1)
### Legacy feature! Bad case "goal1" (line 3660 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal2" (line 3668 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal3" (line 3672 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal4" (line 3681 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal5" (line 3685 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal6" (line 3689 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal1" (line 4057 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal2" (line 4065 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### theory "Presburger_Automata"
### 21.954s elapsed time, 75.748s cpu time, 14.988s GC time
### Legacy feature! Bad case "goal3" (line 4069 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal4" (line 4078 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal5" (line 4082 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal6" (line 4086 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

[Andreas Lochbihler]

MonoBoolTranAlgebra was failing due to my change in Isabelle/90f54d9e63f2 and the removal 
of theorem fun_eq in favour of arg_cong (I have not investigated when this happened, but 
just adapted the proof scripts), see changesets 53f94abb8704 and 0377b757f016. 
Presburger-Automata had a looping call to simp which looks related to the changes with 
real. It should work now in AFP/935a90e010a2.


Vickey_Clarke_Groves looks related to the changes to "real", but I have not 
tried to fix this.

Best,
Andreas

On 15/11/15 10:38, Florian Haftmann wrote:

isabelle: f1b257607981 tip
afp: 1a688183b05a tip

Any idea what is going on here?

Florian



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


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