Dear Peter,
>> 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:
>
> summary: adapting entries to new Deriving mechanism
>
> in LTL_to_GBA-theory, this removes a linorder-constrai
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
date:Fri Mar 13 1
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 wrote:
>
> It's the operation identification phase of Autoref,
> quite difficult to debug ... I have not yet looked at it due to
>
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
O
> 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
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/haftman
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/ha
