From: "Dr A. Koutsoukou-Argyraki" <firstname.lastname@example.org>
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
Would anyone like to share their thoughts?
From: Mikhail Chekhov <email@example.com>
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.
Last updated: Sep 28 2021 at 19:14 UTC