It's the speed of compilation plus native execution vs interpretation through the kernel via the simplifier. The simplifier is already pretty optimised. No idea whether there are specific optimisations for code equations.<br><br>Peter <div class="quote" style="line-height: 1.5"><br><br>-------- Original Message --------<br>Subject: Re: [isabelle-dev] A suggestion: call eval with try0<br>From: Manuel Eberl <eberlm@in.tum.de><br>To: isabelle-dev@mailman46.in.tum.de<br>CC: <br><br><br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Yes, that's called code_simp.<br><br>The difference, however, is often several orders of magnitude, which<br>makes code_simp unfeasible in most cases.<br><br>I always wondered /why/ it is that slow and whether this is just not<br>optimised that well or whether it's some unavoidable bottleneck.<br><br>Manuel<br><br><br>On 17/08/2020 13:30, lammich@in.tum.de wrote:<br>> Hi<br>> Isn't there a (slower) possibility to Eval via the simplifier?<br>> <br>> Peter<br>> <br>> <br>> -------- Original Message --------<br>> Subject: Re: [isabelle-dev] A suggestion: call eval with try0<br>> From: Jasmin Blanchette <j.c.blanchette@vu.nl><br>> To: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk><br>> CC: Isabelle-dev list <isabelle-dev@mailbroy.informatik.tu-muenchen.de><br>> <br>> <br>>     Dear Angeliki,<br>> <br>>     > eval is not one of the many methods called by try0, and to my<br>>     experience so far Sledgehammer doesn't suggest it either.<br>>     > I've noticed several very simple proofs that work just "by eval"<br>>     and yet automation won't suggest any proof.<br>>     ><br>>     > Do people agree that it would be practical to include eval in the<br>>     methods tried with try0?<br>>     ><br>>     > and would this be feasible ?<br>> <br>>     Technically, this would be very feasible. The question is more<br>>     whether it's desirable to have "try0" and Sledgehammer suggest<br>>     tactics that bypass the LCF-style kernel and its strong guarantees.<br>>     These are not just "academic" worries. Just a few years ago, there<br>>     was a debilitating bug in "eval" that made it succeed every time,<br>>     even if your conjuecture was literally "False". (I can't find it in<br>>     "NEWS", but I vividly remember the discussion on the mailing list.)<br>> <br>>     Maybe a mention "(oracle)" next to "eval" would be enough? If it's<br>>     clear enough that "eval" doesn't have the same status as the other<br>>     tactics, I wouldn't mind enhancing "try0" in this way. Many users<br>>     who rely on "try0" are novices that learn Isabelle and its tactics<br>>     partly through "try0".<br>> <br>>     Cheers,<br>> <br>>     Jasmin<br>> <br>>     P.S. I believe your email might interest other users of Isabelle.<br>>     You might not reach them by writing to isabelle-dev.<br>> <br>>     _______________________________________________<br>>     isabelle-dev mailing list<br>>     isabelle-dev@in.tum.de<br>>     https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br>> <br>> <br>> _______________________________________________<br>> isabelle-dev mailing list<br>> isabelle-dev@in.tum.de<br>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br>> <br>_______________________________________________<br>isabelle-dev mailing list<br>isabelle-dev@in.tum.de<br>https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br></blockquote></div>