Re: [isabelle-dev] A suggestion: call eval with try0

Mon, 17 Aug 2020 05:04:43 -0700

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.

Peter


-------- Original Message --------
Subject: Re: [isabelle-dev] A suggestion: call eval with try0
From: Manuel Eberl <[email protected]>
To: [email protected]
CC:


Yes, that's called code_simp.

The difference, however, is often several orders of magnitude, which
makes code_simp unfeasible in most cases.

I always wondered /why/ it is that slow and whether this is just not
optimised that well or whether it's some unavoidable bottleneck.

Manuel


On 17/08/2020 13:30, [email protected] wrote:
> Hi
> Isn't there a (slower) possibility to Eval via the simplifier?
>
> Peter
>
>
> -------- Original Message --------
> Subject: Re: [isabelle-dev] A suggestion: call eval with try0
> From: Jasmin Blanchette
> To: "Dr A. Koutsoukou-Argyraki"
> CC: Isabelle-dev list
>
>
> Dear Angeliki,
>
> > eval is not one of the many methods called by try0, and to my
> experience so far Sledgehammer doesn't suggest it either.
> > I've noticed several very simple proofs that work just "by eval"
> and yet automation won't suggest any proof.
> >
> > Do people agree that it would be practical to include eval in the
> methods tried with try0?
> >
> > and would this be feasible ?
>
> Technically, this would be very feasible. The question is more
> whether it's desirable to have "try0" and Sledgehammer suggest
> tactics that bypass the LCF-style kernel and its strong guarantees.
> These are not just "academic" worries. Just a few years ago, there
> was a debilitating bug in "eval" that made it succeed every time,
> even if your conjuecture was literally "False". (I can't find it in
> "NEWS", but I vividly remember the discussion on the mailing list.)
>
> Maybe a mention "(oracle)" next to "eval" would be enough? If it's
> clear enough that "eval" doesn't have the same status as the other
> tactics, I wouldn't mind enhancing "try0" in this way. Many users
> who rely on "try0" are novices that learn Isabelle and its tactics
> partly through "try0".
>
> Cheers,
>
> Jasmin
>
> P.S. I believe your email might interest other users of Isabelle.
> You might not reach them by writing to isabelle-dev.
>
> _______________________________________________
> isabelle-dev mailing list
> [email protected]
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>
>
> _______________________________________________
> isabelle-dev mailing list
> [email protected]
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Reply via email to