[isabelle] Undefined facts in skip_proofs mode (take two)
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Undefined facts in skip_proofs mode (take two)
- From: Lars Hupel <hupel at in.tum.de>
- Date: Thu, 14 Apr 2016 12:00:34 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.7.2
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
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:
This archive was generated by a fusion of
Pipermail (Mailman edition) and