[isabelle] Undefined facts in skip_proofs mode (take two)



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.