[isabelle-dev] lex_prod changes

Dmitriy Traytel traytel at di.ku.dk
Fri Aug 21 12:48:42 CEST 2020


Hi Larry,

Just undoing the changes should be easy via "hg backout -r <revision>" for each of the commits in question (going backwards in time).

Cheers,
Dmitriy

On 21 Aug 2020, at 11:59, Klein, Gerwin (Data61, Kensington NSW) <Gerwin.Klein at data61.csiro.au<mailto:Gerwin.Klein at data61.csiro.au>> wrote:

I’m happy with either direction as long as we get into a consistent state. If we revert the definition, we’ll also have to revert the AFP fixes, but I’m assuming that this is going to be easier than the other direction.

Cheers,
Gerwin

On 21 Aug 2020, at 17:55, Lawrence Paulson <lp15 at cam.ac.uk<mailto:lp15 at cam.ac.uk>> wrote:

Before wasting another week, which incidentally I really can’t spare, it would be nice to know whether there are any objections to going back to the original definition?

Larry

On 21 Aug 2020, at 09:34, Lawrence Paulson <lp15 at cam.ac.uk<mailto:lp15 at cam.ac.uk>> wrote:

It’s obvious that this proposal should have been discussed more widely. And I shouldn’t have volunteered to implement it before securing firm offers of help, because it was obvious from the outset that it would be seriously laborious. With this change, a repair is never as simple as inserting some tactic or rewrite but requires at least a lemma or two. In some cases it’s a problem-solving task taking hours. So I’m sorry it’s taken me so long to reduce 60 failing entries to 20 (and I have fixes to five more in the pipeline). But I’d be happy to wash my hands of the whole thing.

_______________________________________________
isabelle-dev mailing list
isabelle-dev at in.tum.de<mailto:isabelle-dev at in.tum.de>
https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmailman46.in.tum.de%2Fmailman%2Flistinfo%2Fisabelle-dev&data=02%7C01%7Ctraytel%40di.ku.dk%7C3e7d857e667b4f14b15f08d845b8e924%7Ca3927f91cda14696af898c9f1ceffa91%7C0%7C0%7C637336008072177688&sdata=cjpY6bAE0N6qIyxAz3IkhBKVvJ1vC%2BGwi%2FjIfPZdsnU%3D&reserved=0

_______________________________________________
isabelle-dev mailing list
isabelle-dev at in.tum.de<mailto:isabelle-dev at in.tum.de>
https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmailman46.in.tum.de%2Fmailman%2Flistinfo%2Fisabelle-dev&data=02%7C01%7Ctraytel%40di.ku.dk%7C3e7d857e667b4f14b15f08d845b8e924%7Ca3927f91cda14696af898c9f1ceffa91%7C0%7C0%7C637336008072177688&sdata=cjpY6bAE0N6qIyxAz3IkhBKVvJ1vC%2BGwi%2FjIfPZdsnU%3D&reserved=0

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200821/832aabcd/attachment-0001.html>


More information about the isabelle-dev mailing list