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



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





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