No doubt this is my responsibility, but this very complicated heap of code has been out of my consciousness for many years. Sorting it out would be a non-trivial project.
Larry > On 30 Dec 2014, at 15:06, Makarius <makar...@sketis.net> wrote: > > Metis proof reconstruction is already known to have occasional problems due > to polymorphism. E.g. a long-pending question is how to avoid the various > workarounds for Thm.bicompose that can be seen in Brownian motion here: > > changeset: 52225:568b2cd65d50 > user: wenzelm > date: Wed May 29 18:55:37 2013 +0200 > files: src/HOL/Tools/Metis/metis_reconstruct.ML > description: > resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of > equal Vars are *not* unified -- recover last example in > src/HOL/Metis_Examples/Clausification.thy; > > > A related or unrelated Metis breakdown happened after a slight reform to give > it a proper proof context (115965966e15), such that internal tools may refer > to configuration options from the context as expected. > > A bad consequence of that were a handful of broken Metis proofs (one in main > Isabelle, the rest in AFP). E.g. see > > changeset: 59166:4e43651235b2 > user: wenzelm > date: Sun Dec 21 15:59:19 2014 +0100 > files: src/HOL/Cardinals/Cardinal_Order_Relation.thy > description: > recovered metis proof after 115965966e15 (Odd clash of type variables!?); > > > In all these situations there were (redundant) polymorphic "uses" in the > proof state, that could somehow cause a clash with schematic type variables > inside Metis. Presumably, Metis does not observe the Isabelle proof context > with its notion of locally used names -- but this is really just a guess from > a big distance from the actual code. > > I did not change anything there, but repaired these very few proofs manually, > by omitting the unused polymorphic facts. > > > There is probably no immediate need for further action, although someone who > understands Metis proof reconstruction might want to clean up its internal > treatment of locally generated types, to eliminate this potential of surprise. > > > Makarius > > ---------------------------------------------------------------------------- > http://stop-ttip.org 1,235,909 Participants > ---------------------------------------------------------------------------- > _______________________________________________ > 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
