Email Gateway (Nov 07 2022 at 14:43): Email Gateway (Nov 07 2022 at 14:43):From: "C. Diekmann" <diekmann@net.in.tum.de>
Howdy Isabelle experts,
I'm building a pdf document for human consumption with
options [document_variants="outline=-proof,-ML"]
theories [show_question_marks = false]
I don't want to show the proofs to humans, since they are technical and not
helpful for my target audience. Yet, I'd like to claim that folks can
definitely skip reading the proofs in good conscience, since Isabelle
checked them when compiling the pdf. Therefore, I'm building the document
only as an outline with outline=-proof.
When I have some leftover lemma in my theory, for example
lemma False
oops
the proof document will just contain
lemma False
as if I had proven this.
Is there a way to exclude or mark unfinished proofs in an outline proof
document?
Thanks,
Cornelius
Email Gateway (Nov 07 2022 at 14:58):From: Alex Weisberger <alex.m.weisberger@gmail.com>
isabelle build will fail if there are any errors or oops / sorry
statements. Maybe it's worth creating a script that first builds the theory
and then exports it, so the export won't happen unless build succeeds.
Other than that, I'm not aware of a flag or anything that will prevent the
outline from succeeding, though I'm not an expert there.
Email Gateway (Nov 07 2022 at 15:01):From: Peter Lammich <lammich@in.tum.de>
On 07/11/2022 15:58, Alex Weisberger wrote:
isabelle buildwill fail if there are any errors or oops / sorry
statements.
Clarification/correction: 'isabelle build' does not fail on oopsed
lemmas! It fails on errors and sorrys though, unless in quick-and-dirty
mode.
Last updated: Apr 25 2024 at 20:15 UTC