Email Gateway (Aug 19 2020 at 10:31): Email Gateway (Aug 19 2020 at 10:31):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear All, CC: Jasmin
(Apologies to the members of the isabelle-dev list for the duplication).
I am forwarding a post on a suggestion I recently made at the
isabelle-dev list (suggesting to
call eval by try0 which might be helpful especially for new users, as
currently proofs by eval are never found by any automation tools)
together with Jasmin's reply. Please see below.
(Florian, Manuel and Peter might want to forward their discussion about
code_simp too).
Would anyone like to share their thoughts?
Best,
Angeliki
Email Gateway (Aug 21 2020 at 21:02):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
I have a short comment related to the following statement
As someone who started learning Isabelle not too long ago by the 'Isabelle
time scale', I can tell that it would be very useful to make it more
apparent which of the methods that are available from the main distribution
"bypass the LCF-style kernel and its strong guarantees". I can imagine, a
new user can be easily misled into a belief that all methods are
equivalently safe, unless some warnings/errors are issued (for example, the
fake proof step 'sorry' requires the quick_and_dirty_mode), especially due
to the existence of (seemingly) un(der)documented methods (e.g. argo). As
much as I appreciate "Ignorantia juris non excusat", there is little reason
not to include gentle reminders about the breach of some of the guarantees
that the software provides under most of the common circumstances.
Kind Regards,
Mikhail Chekhov
Last updated: Jul 15 2022 at 23:21 UTC