Email Gateway (Aug 19 2022 at 10:01): Email Gateway (Aug 19 2022 at 10:01):From: Joachim Breitner <breitner@kit.edu>
Hi,
while preparing some slides, I want to include some isabelle-generated
LaTeX from a small fragment. So I fired up jEdit and wrote the few lines
in Scratch.thy, saving that file to /tmp.
Now I’d like to figure out how to convert that to .tex, without creating
a full session and running "isabelle build" and then extracting the .tex
from the generated .tex files.
Is there a low-level-command that goes from .thy directly to .tex,
without a session infrastructure involving ROOT and document/root.tex?
I tried
isabelle-process -I -q -m latex HOL < Scratch.thy
which spits out LaTeX, but not the theory but rather the progress of
processing it.
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 10:06):From: Makarius <makarius@sketis.net>
On Fri, 8 Feb 2013, Joachim Breitner wrote:
I want to include some isabelle-generated LaTeX from a small fragment.
Now I’d like to figure out how to convert that to .tex, without creating
a full session and running "isabelle build" and then extracting the .tex
from the generated .tex files.
If this is feasible in Isabelle2012 or Isabelle2013 depends on how small
the fragment might be.
For example, you can print formal entities with the "latex" print mode
interactively like this:
thm (latex) exI exE
or goal states:
pr (latex)
This is a half-forgotten and quite archaic form. I can't tell on the
spot how far it still works.
Another approximation is display_drafts, which is Present.drafts in ML.
It merely does pretty printing of Isabelle symbols, without any formal
content.
Is there a low-level-command that goes from .thy directly to .tex,
without a session infrastructure involving ROOT and document/root.tex?
That is difficult with the full spectrum of document antiquotations etc.
The main entry point for that is Thy_Output.present_thy but that is not
easily invoked manually.
Proper document preparation is still intertwined with the session concept,
although there is conceptually no strong reason for it, just old habits.
In the past few years, I have occasionally made tiny steps to make it more
value oriented, operating on given sources more systematically. My
immediate motivation is to have document preparation within the Prover
IDE, to avoid the relatively clumsy batch build sessions.
Makarius
Email Gateway (Aug 19 2022 at 10:06):From: Joachim Breitner <breitner@kit.edu>
Hi,
Am Montag, den 11.02.2013, 17:33 +0100 schrieb Makarius:
For example, you can print formal entities with the "latex" print mode
interactively like this:thm (latex) exI exE
or goal states:
pr (latex)
This is a half-forgotten and quite archaic form. I can't tell on the
spot how far it still works.
It works, just today I was using "thm (latex)" quite a few times where I
really just need a theorem, and not a whole Isar command.
Is there a low-level-command that goes from .thy directly to .tex,
without a session infrastructure involving ROOT and document/root.tex?That is difficult with the full spectrum of document antiquotations etc.
The main entry point for that is Thy_Output.present_thy but that is not
easily invoked manually.Proper document preparation is still intertwined with the session concept,
although there is conceptually no strong reason for it, just old habits.In the past few years, I have occasionally made tiny steps to make it more
value oriented, operating on given sources more systematically. My
immediate motivation is to have document preparation within the Prover
IDE, to avoid the relatively clumsy batch build sessions.
Thanks, that would be great. Until then, "isabelle mkroot -d" followed
by adding Scratch to the theories and quick_and_dirty to the options is
sufficient.
Greetings,
Joachim
signature.asc
Last updated: Apr 20 2024 at 08:16 UTC