Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] AFP/VerifyThis2018 document fails in developme...


view this post on Zulip Email Gateway (Aug 22 2022 at 17:15):

From: Tobias Nipkow <nipkow@in.tum.de>
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".

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 17:15):

From: Makarius <makarius@sketis.net>
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
ROOT

view this post on Zulip Email Gateway (Aug 22 2022 at 17:15):

From: Makarius <makarius@sketis.net>
This is actually the updated ROOT file.

Makarius
ROOT

view this post on Zulip Email Gateway (Aug 22 2022 at 17:15):

From: Lars Hupel <hupel@in.tum.de>

This is actually the updated ROOT file.

See AFP/b28b21cce555.

view this post on Zulip Email Gateway (Aug 22 2022 at 17:16):

From: Makarius <makarius@sketis.net>
In very rare cases there is a need for that, but in most practical
situations, it is probably just some legacy.

Maybe all AFP authors with auxiliary intermediate sessions can check, if
the situation can be improved by eliminating them.

For the next Isabelle release, there will be fancy options for "isabelle
jedit" to build an adhoc session image from the requirements of another
regular session (notably options -A and -S). As we are heading towards
the release in June/July/August 2018, I will probably simplify these
options further, based on feedback by users.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 17:16):

From: Lars Hupel <hupel@in.tum.de>

In very rare cases there is a need for that, but in most practical
situations, it is probably just some legacy.

One case that comes into mind is the distinction between the session
that can be used by downstream dependencies, and another session that
includes (maybe costly) examples, e.g. in the case of the iptables
semantics. Luckily, the metadata file, together with the regular
Isabelle session information, allows for a precise mapping between
sessions and entries.


Last updated: Mar 28 2024 at 12:29 UTC