Email Gateway (Aug 22 2022 at 15:47): Email Gateway (Aug 22 2022 at 15:47):From: "Siek, Jeremy" <jsiek@indiana.edu>
I’d like to use Isabelle-generated LaTeX with the new
ACM SIGPLAN latex class file, but I’ve run into a couple
problems.
http://www.sigplan.org/sites/default/files/acmart/current/acmart.cls
I changed the first line of root.tex to:
\documentclass[acmsmall,10pt]{acmart}\settopmatter{}
I first tried to generate the PDF in a document without any
theories. But got this error:
(./pdfsetup.sty)
! LaTeX Error: Option clash for package hyperref.
To see if I could get further along, I commented out
\usepackage{pdfsetup}
in my root.tex
After that I was able to generate a pdf from a document with no theories.
I then added the Scratch theory to ROOT but then ran into a second problem:
(./session.tex (./Scratch.tex)
Runaway argument?
! File ended while scanning use of \next.
<inserted text>
\par
l.1 \input{Scratch.tex}
At which point I was in over my head and stuck.
(The problem might be due to conflicts regarding the “comment”
packages used in Isabelle and in acmart.cls.)
Any help would be appreciated!
Thanks,
Jeremy
Jeremy G. Siek <jsiek@indiana.edu<mailto:jsiek@indiana.edu>>
Associate Professor
School of Informatics and Computing
Indiana University Bloomington
http://homes.soic.indiana.edu/jsiek/
Email Gateway (Aug 22 2022 at 15:47):From: Tobias Nipkow <nipkow@in.tum.de>
Hi Jeremy,
I had the same problem and it is indeed due to the comment package. This is how
I solved it:
\usepackage{isabelle,isabellesym}
\def\isadelimtheory{}\def\endisadelimtheory{}
\def\isatagtheory{}\def\endisatagtheory{}
\def\isadelimML{}\def\endisadelimML{}
\def\isatagML{}\def\endisatagML{}
\def\isafoldML{}
\def\isadelimproof{}\def\endisadelimproof{}
\def\isatagproof{}\def\endisatagproof{}
\def\isafoldproof{}
There may be more graceful ways.
Tobias
smime.p7s
Last updated: Apr 19 2024 at 16:20 UTC