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-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.
sorry, for this problem. I first locally tried to replace the linorder class-constraint by some compare class-constraint, since the new derive-generator produces class-constraints of the form mytype :: (compare,...,compare)compare. However, for lack of time I did not manage to fully adapt your entry from linorder to compare before ITP submission. To this end, I manually adapted in 88dc498667ff the generation of linear orders in LTL_to_GBA_impl. Since also other entries prefer the mytype :: (linorder, ..., linorder)linorder constraint, I adding support for it in derive in 470b9d92f174 and then integrate it in LTL_to_GBA_impl in 8afc741ecb48, so that the adaptation of LTL_to_GBA_impl in total only was a change of a single line, namely the import statement from the old to the new derive. However, the problem was that I overlooked in 88dc498667ff that it also contained a change in LTL_to_GBA which removed the linorder constraint, and which shouldn't have been checked in. Anyway, thanks for fixing the problem, René _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
