Email Gateway (Aug 19 2022 at 14:13): Email Gateway (Aug 19 2022 at 14:13):From: Joachim Breitner <breitner@kit.edu>
Hi,
I’m surprised how often, when googling some problem I’m having, I find
me asking the question somewhen in the past. Unfortunately, there was
not always an answer, so let me try again – maybe things have changed
since then:
I have am preparing an AFP submission that should contain a session
graph. It also contains a theory (“Everything”) that includes everything
and will \input’ed in the introduction, so it is not visible as a Theory
to the user. Currently, it shows up in the session graph (which is
confusing, makes the graph layout less nice and pulls in the also not
interesting TaTeXsugar theory).
Can I prevent isabelle from including that theory in the session graph?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 14:14):From: Makarius <makarius@sketis.net>
Both the graph and HTML presentation are relatively old, and awaiting
renovation for many years. The graph tool and its wrap-up within the
document preparation is particularly ancient.
One could probably play nasty tricks with some perl scripts to force the
Isabelle document to look in a certain way, but that would play against
any reform of that if / when it actually happens.
For now I recommend to let the system do its work with minimal
intervention. E.g. what is the purpose of the Everything.thy instead of
just listing all its imports in ROOT?
Suppressing LaTeXsugar.thy could work by an auxiliary base session,
although for the purpose of AFP that is probably a bit much extra weight.
Since LaTeXsigar is part of the HOL-Library session, you could use that as
a base if you don't have any other special one already.
Makarius
Email Gateway (Aug 19 2022 at 14:14):From: Joachim Breitner <breitner@kit.edu>
Hello Makarius,
Am Montag, den 28.04.2014, 20:24 +0200 schrieb Makarius:
For now I recommend to let the system do its work with minimal
intervention. E.g. what is the purpose of the Everything.thy instead of
just listing all its imports in ROOT?
it not only imports everything, but also contains TeX code with
anti-quotations that state the main results. See
http://afp.sourceforge.net/browser_info/current/AFP/Launchbury/document.pdf where section 1.1 is the result of Isabelle processing Everything.thy.
Suppressing LaTeXsugar.thy could work by an auxiliary base session,
although for the purpose of AFP that is probably a bit much extra weight.
Since LaTeXsigar is part of the HOL-Library session, you could use that as
a base if you don't have any other special one already.
Basing my HOLCF+Nominal2 session (which is the base for my work) on
HOL-Library is a good idea to solve that, thanks!
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 14:14):From: Makarius <makarius@sketis.net>
I would say that small imperfection is OK. If/when some reform of the
graph presentation tool happens eventually, you should remind the person
who does it to provide some simple means to filter the result.
Makarius
Last updated: Apr 19 2024 at 20:15 UTC