[isabelle] Isabelle document prep and ACM journals document class



Dear Isabelle users,

Does anyone on the list have experience preparing documents that use the 
'acmsmall' document class?

I'm getting a latex error when building and am hoping somebody might 
have experience in how to debug or resolve it.

Below is a minimal example, derived by doing a clean 'isabelle mkroot 
-d', with a minimal theory file and the relevant document class and 
associated style files.

In case you want to reproduce, download: 
http://www.acm.org/binaries/content/assets/publications/article-templates/acmsmall.zip 
and extract the 'acmsmall.cls' and 'acmcopyright.sty' files (listed in 
the ROOT file below).

$ cat Test.thy
theory Test
imports Main
begin

text {*
Here is a theorem: @{thm TrueI}
*}


$ ls document/
acmcopyright.sty acmsmall.cls     root.tex

$ head -7 document/root.tex
% the only modification made to the original root.tex generated by
% isabelle mkroot -d
%\documentclass[11pt,a4paper]{article}
\documentclass[prodmode,acmtops]{acmsmall}

\usepackage{isabelle,isabellesym}


$ cat ROOT
session "minex" = "HOL" +
   options [document = pdf, document_output = "output"]
   theories
     Test
   document_files
     "root.tex"
     "acmsmall.cls"
     "acmcopyright.sty"


$ /Applications/Isabelle2016.app/Isabelle/bin/isabelle build -D .
Running minex ...

minex FAILED
(see also 
/Users/tobiasm1/.isabelle/Isabelle2016/heaps/polyml-5.6_x86-darwin/log/minex)

*** (/usr/local/texlive/2016/texmf-dist/tex/latex/hyperref/nameref.sty
*** 
(/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
*** (./root.out) (./root.out)
*** (/usr/local/texlive/2016/texmf-dist/tex/latex/psnfss/ot1phv.fd) 
(./root.toc)
*** (./session.tex (./Test.tex)
*** Runaway argument?
*** ! File ended while scanning use of \next.
*** <inserted text>
***                 \par
*** l.1 \input{Test.tex}
***
*** ))
*** ! Emergency stop.
*** <*> \nonstopmode\input{root.tex}
***
*** !  ==> Fatal error occurred, no output PDF file produced!
*** Transcript written on root.log.
*** Document preparation failure in directory 'output/document'
***
*** Failed to build document "/Users/tobiasm1/tmp/minex/output/document.pdf"
Unfinished session(s): minex
0:00:08 elapsed time, 0:00:19 cpu time, factor 2.37



Any suggestions would be very helpful and much appreciated.

Thanks heaps

Toby




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.