[isabelle-dev] isabelle build for generating TeX Snippets

Christian Sternagel c-sterna at jaist.ac.jp
Tue Nov 6 06:04:14 CET 2012


(I send this message to the development list since isabelle build is not 
yet part of any official release.)

Dear all,

How could we translate the instructions from

   https://isabelle.in.tum.de/community/Generate_TeX_Snippets

for use with "isabelle build"?

More specifically, I currently have the ROOT file

session "Snippets" = "HOL" +
   options [
     document = "pdf",
     document_output = "generated",
     document_variants = "snippets",
     show_question_marks = "false"]
   theories
     Snippets
   files
     "document/build"
     "document/root.tex"
     "document/isabelle.sty"
     "document/isabellesym.sty"

and the document/build file:

#!/bin/bash

set -e

FORMAT="$1"
VARIANT="$2"

"$ISABELLE_TOOL" latex -o "$FORMAT"
sed -n '/DefineSnippet/,/EndSnippet/p' Snippets.tex > ../snippets.tex

together with a theory file Snippets.thy that contains the actual 
snippets. What is a bit annoying about this setup, is that I actually 
have to build a file snippets.pdf (hence also the otherwise irrelevant 
files document/root.tex, document/isabelle.sty, and 
document/isabellesym.sty) just to obtain the file 
generated/snippets.tex. Any suggestions how to do this directly (without 
falling back to an IsaMakefile)?

cheers

chris


More information about the isabelle-dev mailing list