Re: [isabelle] Undefined facts in skip_proofs mode

On Thu, 31 Jul 2014, Gerwin Klein wrote:

I’m surprised that latex output works with it at all, for instance. It is even possible in some cases that the theorems you get out of skip_proofs are slightly different to the ones you would get from a normal run.

It would be nice to do skip_proofs properly. For instance, I could imagine that judicious use of futures may supersede the current skip_proofs implementation

I am trying to do such reforms for years. Eventually it should be all just one uniform concept to manage forked proofs, potentially with different priorities and different policies to insist or not insist in joining them later.

To get there, the usual layers of sediments need to be cleaned up slowly and steadily. Moreover, one needs to have a clear picture of typical applicaions, beyond accidental features inherited from the past.

That is why it is important to describe particular situations in a meaningful way. Often the reports are isomorphic to "I want to use feature X in the context of Y, but it fails".


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.