Email Gateway (Aug 19 2022 at 10:28): Email Gateway (Aug 19 2022 at 10:28):From: Joachim Breitner <breitner@kit.edu>
Hi,
I like the new, declarative session specification system, thanks!
I’m currently writing a ROOT file for a set of exercise sheets that uses
the tags feature to generate both a variant without solutions and a
variant with solutions from the same file. Currently, the file looks
like this:
session Uebung1 = HOL +
options [document=pdf, document_variants="document=+template,-templateoops,/solution:solution=-template,-templateoops,+solution"]
theories "Deduction"
files "document/root.tex"
session Uebung2 = HOL +
options [document=pdf, document_variants="document=+template,-templateoops,-onlysolution,/solution:solution=-template,-templateoops,+onlysolution,+solution"]
theories "Simplification"
files "document/root.tex"
Can I somehow set these options for all sessions in the file, or define
a “base session” that does not add any theory and just sets options?
I know I can create a wrapper script that passes the options to
"isabelle build", but I’d prefer if the sessions were self-contained,
e.g. "isabelle build -D ." works without first having to look for the
“correct” invocation.
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 10:30):From: Makarius <makarius@sketis.net>
I tried to make sessions as declarative and self-contained as feasible, so
there is no way for common options, apart from global
ISABELLE_BUILD_OPTIONS or similar. But document_variants should indeed be
associated with the document session in question.
What you can do is to delegate interpretation of document variants to the
document job. You merely specify names in ROOT and re-adjust the latex
environments for tags later. You can do completely different things, of
course. In Isabelle2013 document variants are more flexibile than before.
Included is an example for Isabelle2013-RC1/RC2/RC3. ROOT merely
specifies document_variants="foo:bar" and root_foo.tex, root_bar.tex
determine what happens.
Just after making the Isabelle2013-RC3 snapshot, I realized that "isabelle
document" needs a tiny repair as in the included "ch" changeset.
Makarius
Variants.tar.gz
ch
Email Gateway (Aug 19 2022 at 10:30):From: Joachim Breitner <breitner@kit.edu>
Dear Makarius,
Am Donnerstag, den 07.02.2013, 14:03 +0100 schrieb Makarius:
Can I somehow set these options for all sessions in the file, or define
a “base session” that does not add any theory and just sets options?I tried to make sessions as declarative and self-contained as feasible, so
there is no way for common options, apart from global
ISABELLE_BUILD_OPTIONS or similar. But document_variants should indeed be
associated with the document session in question.What you can do is to delegate interpretation of document variants to the
document job. You merely specify names in ROOT and re-adjust the latex
environments for tags later. You can do completely different things, of
course. In Isabelle2013 document variants are more flexibile than before.
Thanks for the tip. I already had root.tex and root_solution.tex (for
differing page headers), but did not thing about configuring the tag
setting there. Now the declarations duplicated for each problem sheet
are down to
options [document=pdf, document_variants="document:solution"]
files "document/root.tex" "document/root_solution.tex" "document/root_common.tex"
which at least does no longer expose the tag list.
Just after making the Isabelle2013-RC3 snapshot, I realized that "isabelle
document" needs a tiny repair as in the included "ch" changeset.
JFTR: It works as advertised on 2013-RC2, without the patch.
Greetings,
Joachim
signature.asc
Last updated: Apr 25 2024 at 16:19 UTC