Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
[isabelle] Status of "eval" method
15 views
Skip to first unread message
Peter Lammich
Oct 17, 2012, 3:42:46 AM10/17/12
to isabelle-users
Hi,
a student of mine recently noticed that there is no documentation for
the "eval" method. Nevertheless, he was able to find it. What he of
course did not recognize was, that it actually seems to "prove" theorems
by cheating (they are pretty-printed with [!] afterwards).
So I propose to either add proper documentation for this method,
including a warning that it does not go through the inference kernel,
perhaps even renaming it to something like "eval_sorry", or to remove
it.
--
Peter
a student of mine recently noticed that there is no documentation for
the "eval" method. Nevertheless, he was able to find it. What he of
course did not recognize was, that it actually seems to "prove" theorems
by cheating (they are pretty-printed with [!] afterwards).
So I propose to either add proper documentation for this method,
including a warning that it does not go through the inference kernel,
perhaps even renaming it to something like "eval_sorry", or to remove
it.
--
Peter
Lukas Bulwahn
Oct 17, 2012, 4:27:05 AM10/17/12
to Peter Lammich, isabelle-users
Hi Peter,
A thorough documentation can be found in the code generation tutorial in
chapter 6.
If you care much about evaluations going through Isabelle's inference
kernel, Isabelle provides a method "code_simp", which does the same as
eval but slower ;)
Maybe you could add documentation about eval in the Isar reference (by
extending chapter 10.20) then, and summarize the proof methods of chapter 6?
Removing is not possible as the Flyspeck proof relies on this method.
In my opinion, renaming is not a reasonable option either.
Lukas
A thorough documentation can be found in the code generation tutorial in
chapter 6.
If you care much about evaluations going through Isabelle's inference
kernel, Isabelle provides a method "code_simp", which does the same as
eval but slower ;)
Maybe you could add documentation about eval in the Isar reference (by
extending chapter 10.20) then, and summarize the proof methods of chapter 6?
Removing is not possible as the Flyspeck proof relies on this method.
In my opinion, renaming is not a reasonable option either.
Lukas
Makarius
Oct 17, 2012, 5:28:12 AM10/17/12
to Lukas Bulwahn, Peter Lammich, isabelle-users
On Wed, 17 Oct 2012, Lukas Bulwahn wrote:
> Removing is not possible as the Flyspeck proof relies on this method. In
> my opinion, renaming is not a reasonable option either.
>
> Removing is not possible as the Flyspeck proof relies on this method. In
> my opinion, renaming is not a reasonable option either.
>
> On 10/17/2012 09:36 AM, Peter Lammich wrote:
>>
>> So I propose to either add proper documentation for this method,
>> including a warning that it does not go through the inference kernel,
>> perhaps even renaming it to something like "eval_sorry", or to remove
>> it.
"eval_sorry" would indeed be a rather odd name, because it is based on a
>>
>> So I propose to either add proper documentation for this method,
>> including a warning that it does not go through the inference kernel,
>> perhaps even renaming it to something like "eval_sorry", or to remove
>> it.
different oracle that is supposed to be correct relative to the
implementation of the code generator.
In contrast, the oracle behind "sorry" merely pretends that "!!X. X"
holds, so you will be really sorry if you rely on the result.
Makarius
Jasmin Blanchette
Oct 17, 2012, 7:39:22 AM10/17/12
to Makarius, Peter Lammich, isabelle-users, Lukas Bulwahn
Am 17.10.2012 um 11:20 schrieb Makarius:
> "eval_sorry" would indeed be a rather odd name, because it is based on a different oracle that is supposed to be correct relative to the implementation of the code generator.
But what about "eval_oracle"? It would minimize the risk that somebody misunderstood its nature (and would free up a useful name, "eval", for the non-oracle version if desired).
> "eval_sorry" would indeed be a rather odd name, because it is based on a different oracle that is supposed to be correct relative to the implementation of the code generator.
Jasmin
Florian Haftmann
Oct 18, 2012, 4:42:22 AM10/18/12
to cl-isabe...@lists.cam.ac.uk
documented thoroughly either (at least I guess so, otherwise I would
have migrated that documentation).
If all methods relying on oracles are supposed to reflect this in their
name, there are a couple of other candidates also, e.g. normalizsation.
Keep this in mind when discussing renames etc.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
0 new messages