Re: [isabelle-dev] Problem in the AFP

2015-03-23 Thread Peter Lammich 
On Sa, 2015-03-21 at 18:26 +0100, Peter Lammich wrote:
 It's the operation identification phase of Autoref,
 quite difficult to debug ... I have not yet looked at it due to
 ITP-deadline. 

I found the culprit:

changeset:   5269:88dc498667ff
user:Rene Thiemann rene.thiem...@uibk.ac.at
date:Fri Mar 13 15:42:00 2015 +0100
summary: adapting entries to new Deriving mechanism

in LTL_to_GBA-theory, this removes a linorder-constraint on
create_name_igba, which causes the breakdown, because later,
autoref is only given rules to refine create_name_igba for 
'a::linorder, but the respective lemmas do not repeat the
linorder-constraint. 

I fixed it by adding the linorder-constraint to the refinement, leaving
the abstract version general.

- definition create_name_igba :: 'a::linorder ltln \Rightarrow _ 
+ definition create_name_igba :: 'a ltln \Rightarrow _ where 


See now: changeset 56d43ce6541f

http://sourceforge.net/p/afp/code/ci/56d43ce6541f4602d390d1940ce69d211bd8724c/

--
  Peter

 
 I will have look at it next week on Monday or Tuesday. Does anyone know
 the changeset that introduced the failure, or is there an easy way to
 find out?
 
 --
   Peter
 
 
 On Sa, 2015-03-21 at 18:08 +0100, Florian Haftmann wrote:
   isabelle: e6f0c361ac73 tip
   afp: 2a0dc69c001b tip
  
   Building LTL_to_GBA ...
   
   LTL_to_GBA FAILED
   (see also 
   /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/LTL_to_GBA)
   
 = ('a, 'c) node_scheme set = ('a, 'c) node_scheme set
   Phase id_op
   Failed to identify: create_name_gba
   Failed to identify: ti_Lcnv
   0.048s elapsed time, 0.288s cpu time, 0.000s GC time
   ### theory LTL_to_GBA_impl
   ### 61.088s elapsed time, 341.092s cpu time, 22.988s GC time
   *** Failed to apply proof method (line 1156 of 
   /mnt/home/haftmann/data/afp/master/thys/LTL_to_GBA/LTL_to_GBA_impl.thy):
   *** goal (1 subgoal):
   ***  1. (?c,
   ***  %\phi.
   *** create_name_gba \phi =
   *** (%A. gba_to_idx A =
   ***  (%A'. stat_set_data_nres (card (frg_V A)) (card (frg_V0 
   A'))
   *** (igbg_num_acc A') =
   ***(%_. RETURN A'
   *** : \langleId\rangleltln_rel \rightarrow
   ***   \langleigbav_impl_rel_ext unit_rel nat_rel
   *** (\langleId\ranglefun_set_rel)\ranglenres_rel
   *** At command apply (line 1156 of 
   /mnt/home/haftmann/data/afp/master/thys/LTL_to_GBA/LTL_to_GBA_impl.thy)
   CAVA_buildchain1 CANCELLED
   CAVA_buildchain3 CANCELLED
   CAVA_LTL_Modelchecker CANCELLED
   Unfinished session(s): CAVA_LTL_Modelchecker, CAVA_buildchain1, 
   CAVA_buildchain3, LTL_to_GBA
   0:20:58 elapsed time, 0:59:35 cpu time, factor 2.84
  
  ___
  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


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

Re: [isabelle-dev] Problem in the AFP

2015-03-21 Thread Peter Lammich 
It's the operation identification phase of Autoref,
quite difficult to debug ... I have not yet looked at it due to
ITP-deadline. 

I will have look at it next week on Monday or Tuesday. Does anyone know
the changeset that introduced the failure, or is there an easy way to
find out?

--
  Peter


On Sa, 2015-03-21 at 18:08 +0100, Florian Haftmann wrote:
  isabelle: e6f0c361ac73 tip
  afp: 2a0dc69c001b tip
 
  Building LTL_to_GBA ...
  
  LTL_to_GBA FAILED
  (see also 
  /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/LTL_to_GBA)
  
= ('a, 'c) node_scheme set = ('a, 'c) node_scheme set
  Phase id_op
  Failed to identify: create_name_gba
  Failed to identify: ti_Lcnv
  0.048s elapsed time, 0.288s cpu time, 0.000s GC time
  ### theory LTL_to_GBA_impl
  ### 61.088s elapsed time, 341.092s cpu time, 22.988s GC time
  *** Failed to apply proof method (line 1156 of 
  /mnt/home/haftmann/data/afp/master/thys/LTL_to_GBA/LTL_to_GBA_impl.thy):
  *** goal (1 subgoal):
  ***  1. (?c,
  ***  %\phi.
  *** create_name_gba \phi =
  *** (%A. gba_to_idx A =
  ***  (%A'. stat_set_data_nres (card (frg_V A)) (card (frg_V0 
  A'))
  *** (igbg_num_acc A') =
  ***(%_. RETURN A'
  *** : \langleId\rangleltln_rel \rightarrow
  ***   \langleigbav_impl_rel_ext unit_rel nat_rel
  *** (\langleId\ranglefun_set_rel)\ranglenres_rel
  *** At command apply (line 1156 of 
  /mnt/home/haftmann/data/afp/master/thys/LTL_to_GBA/LTL_to_GBA_impl.thy)
  CAVA_buildchain1 CANCELLED
  CAVA_buildchain3 CANCELLED
  CAVA_LTL_Modelchecker CANCELLED
  Unfinished session(s): CAVA_LTL_Modelchecker, CAVA_buildchain1, 
  CAVA_buildchain3, LTL_to_GBA
  0:20:58 elapsed time, 0:59:35 cpu time, factor 2.84
 
 ___
 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] Problem in the AFP

2015-03-21 Thread Lawrence Paulson 
I've recently pushed some changes affecting the factorial function and 
simplification of real expressions. 

Larry Paulson

 On 21 Mar 2015, at 17:26, Peter Lammich lamm...@in.tum.de wrote:
 
 It's the operation identification phase of Autoref,
 quite difficult to debug ... I have not yet looked at it due to
 ITP-deadline. 
 
 I will have look at it next week on Monday or Tuesday. Does anyone know
 the changeset that introduced the failure, or is there an easy way to
 find out?
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Problem in the AFP

2014-10-23 Thread Florian Haftmann 
Isabelle 06dfbfa4b3ea
AFP 33c18a9138e9

*** Unknown old-style datatype Regular_Exp.rexp
*** At command derive (line 18 of
/mnt/home/haftmann/data/afp/devel/thys/Containers/Compatibility_Containers_Regular_Sets.thy)

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] Problem in the AFP

2014-10-23 Thread Dmitriy Traytel 
Yes, that's my bad. Thanks! I was about to check Mira for complaints. 
See now AFP/ 1dd93cc85dfb.


Dmitriy

On 23.10.2014 14:25, Florian Haftmann wrote:

Isabelle 06dfbfa4b3ea
AFP 33c18a9138e9

*** Unknown old-style datatype Regular_Exp.rexp
*** At command derive (line 18 of
/mnt/home/haftmann/data/afp/devel/thys/Containers/Compatibility_Containers_Regular_Sets.thy)

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