Email Gateway (Aug 22 2022 at 13:09): Email Gateway (Aug 22 2022 at 13:09):From: Lars Hupel <hupel@in.tum.de>
This problem is still open, but cropped up in a different context.
I'd like to have Jenkins produce proof documents. Currently, building
the AFP is factored into "non-slow" and "slow" sessions.
Jenkins can archive build artifacts automatically and serve them under
a stable URL. It will also retain old artifacts indefinitely. This may
potentially be used in the AFP and on the Isabelle home page to link to
snapshot documents. (Including documentation sessions.)
However, due to the split into multiple jobs in Jenkins, this is
potentially difficult to deal with, because it's unclear where a
specific session document lives.
Hence my desire to pull out document processing into a separate job. Of
course I don't want to recheck the whole AFP every time. My idea was to
run everything using "skip_proofs".
Gerwin pointed out to me yesterday that isatest does it too for some
sessions.
Because of the problems with the "thm" command in conjunction with
"skip_proofs" I can't implement this, short of stripping all occurences
of the "thm" command from the AFP. For reference:
<https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-July/msg00239.html>.
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:09):From: Makarius <makarius@sketis.net>
On Thu, 14 Apr 2016, Lars Hupel wrote:
This problem is still open, but cropped up in a different context.
Because of the problems with the "thm" command in conjunction with
"skip_proofs" I can't implement this, short of stripping all occurences
of the "thm" command from the AFP. For reference:
<https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-July/msg00239.html>.
The open problem is the existence of the undefined/undocumented
skip_proofs option. It is just an adhoc way to omit certain important
things. It does change the meaning of theory content and proof documents.
It is a way to produce surprises.
I'd like to have Jenkins produce proof documents. Currently, building
the AFP is factored into "non-slow" and "slow" sessions.Jenkins can archive build artifacts automatically and serve them under
a stable URL. It will also retain old artifacts indefinitely. This may
potentially be used in the AFP and on the Isabelle home page to link to
snapshot documents. (Including documentation sessions.)However, due to the split into multiple jobs in Jenkins, this is
potentially difficult to deal with, because it's unclear where a
specific session document lives.Hence my desire to pull out document processing into a separate job.
I don't quite understand the whole situation. If you want proof documents
for a particular version, you need to produce them with its regular build
process. This takes a bit more time due to extra latex runs, but should
not be a big deal.
In the next big renovation of Isabelle document preparation, the relevant
information for documents might be stored persistently in the log file and
used for separate generation of HTML browser_info or LaTeX documents in an
authentic manner.
Makarius
Email Gateway (Aug 22 2022 at 13:10):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
To clarify that discussion from yesterday (we got interrupted, I think): isatest currently runs some specific sessions with skip_proofs. The purpose of these is not to generate documents, and it is indeed unclear to me if skip_proofs would not lead to a number of surprises, in particular for thm antiquotations, schematic lemmas and other fun things that can occur in documents.
That means, I don’t think it’ll work as a reliable method for getting documents quickly, at least not in general.
The purpose of skip_proofs is only to speed up interactive sessions for very large proofs, in the full knowledge that this sacrifices soundness for that session and that it may lead to unexpected results.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 26 2024 at 12:28 UTC