Re: [isabelle] AFP/VerifyThis2018 document fails in development version



On 10/05/18 09:17, Tobias Nipkow wrote:
> The above AFP entry builds fine with Isabelle2017. However, with the
> development version of the AFP (97ca62a352d8) and Isabelle (eg
> 9339687ca071), document generation fails:
> 
> *** Latex error (line 8 of
> "~/AFP/devel/thys/VerifyThis2018/lib/Synth_Definition.thy"):
> ***   Undefined control sequence.
> ***   <argument> \normalfont \rmfamily \wasylozenge
> 
> The problem seems to come from an ML block containing the string
> "⌑::?'v_T".

This is due to some confusion of theory imports that lack
session-qualified theory names (already in the Isabelle2017 version).

There is an auxiliary session "VTcomp_Lib," which looks suspiciously
like a development artifact that got accidentally published; its
theories are not intended to be typeset in LaTeX. The imports in the
main session "VerifyThis2018" are not qualified and thus taken from the
file-system (after Isabelle2017): it means the theories are loaded again
and thus subject to document output.

The included ROOT file shows how to resolve this. There is now only one
clearly defined session: it produces the correct document, and also
builds faster (because the pointless auxiliary session is gone).


Here is some timing information for this example (threads=6):

(old)
Finished VTcomp_Lib (0:00:35 elapsed time, 0:01:16 cpu time, factor 2.15)
Finished VerifyThis2018 (0:00:29 elapsed time, 0:01:51 cpu time, factor
3.76)

(new)
Finished VerifyThis2018 (0:00:40 elapsed time, 0:02:14 cpu time, factor
3.35)


We might need a more strict scheme for theory imports from other
sessions: double use of files from a different session directory should
be ruled out. (Although I can foresee special sessions that still need
that for historical reasons.)

In addition (or as alternative) we could have a tool to analyze AFP
telemetry information to detect situations of multiple uses of theories,
as well as waste of build time due to extraneous sessions. The data for
that is already stored in a database, but it needs to be digested.


	Makarius
chapter AFP

session VTcomp_Lib = Sepref_IICF +
  options [document=false]
  theories
    "lib/VTcomp"
    "lib/DF_System"
    Snippets

session VerifyThis2018 (AFP) = VTcomp_Lib +
  options [timeout = 600]
  theories
    Challenge1
    Challenge1_short
    Challenge2
    Challenge3
  document_files
    "root.tex"


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