Problem with \endisadelimproof in typesetting · General

Stream: General

Topic: Problem with \endisadelimproof in typesetting

Gergely Buday (Dec 05 2023 at 15:28):

I use Isabelle Snippets to generate snippets of Isabelle into LaTeX.

When I use the packages

\usepackage{output/document/isabelle}
\usepackage{output/document/isabellesym}

I get the error

! Undefined control sequence.
\snippet--lemma:mylemma ...proof
                                                  \ \ \endisadelimproof \isa...

so it seems that \endisadelimproof is not defined. When I add

\usepackage{output/document/isabelletags}

I get this error message:

! Missing } inserted.
<inserted text>
                }
l.192 \Snippet{lemma:mylemma}

which is spurious as I do not see an unpaired left curly brace { in the LaTeX file at line 192.

Do you have an advice how to look deeper into this?

Gergely Buday (Dec 06 2023 at 14:19):

Digging deep into LaTeX Hell, I have found the following generated snippets causing the trouble:

\SNIP{lemma:copairing-unique-4}{%
%\isadelimproof
\ \ %
%\endisadelimproof
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ copairing{\isacharunderscore}{\kern0pt}def\ \ \ \ \ \isanewline%
}%

and

\SNIP{lemma:coproduct-commute-right-1}{%
%\isadelimproof
\ \ %
%\endisadelimproof
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ copairing{\isacharunderscore}{\kern0pt}def\ in{\isacharunderscore}{\kern0pt}{\isadigit{1}}{\isacharunderscore}{\kern0pt}Aplus{\isadigit{1}}{\isacharunderscore}{\kern0pt}def\ comp{\isacharunderscore}{\kern0pt}def\ \isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
\isadelimproof%
}%
}

and

\SNIP{lemma:coproduct-commute-left-1}{

\isadelimproof
\ \ %
\endisadelimproof
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ copairing{\isacharunderscore}{\kern0pt}def\ comp{\isacharunderscore}{\kern0pt}def\ in{\isacharunderscore}{\kern0pt}A{\isacharunderscore}{\kern0pt}Aplus{\isadigit{1}}{\isacharunderscore}{\kern0pt}def\ \isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
\isadelimproof%
}%
}

where \SNIP is

\newcommand{\SNIP}[2]{\expandafter\newcommand\csname snippet--#1\endcsname{#2}}

and \Snippet is

\newcommand{\Snippet}[1]{{%
  \newcount\i
  \i=0
  \loop
    \GetSnip{#1-\the\i}%
    \advance \i 1
  \ifcsname snippet--#1-\the\i\endcsname
  \repeat
}}

Do you have an idea what could go wrong?

Gergely Buday (Dec 06 2023 at 14:26):

I didn't learn what was going wrong but the project page had a solution:

In some cases

The following code can be necessary to make the snippets work with some document classes.

\def\isadelimtheory{}\def\endisadelimtheory{}
\def\isatagtheory{}\def\endisatagtheory{}
\def\isadelimML{}\def\endisadelimML{}
\def\isadelimdocument{}\def\endisadelimdocument{}
\def\isatagML{}\def\endisatagML{}
\def\isatagdocument{}\def\endisatagdocument{}
\def\isafoldML{}
\def\isadelimproof{}\def\endisadelimproof{}
\def\isatagproof{}\def\endisatagproof{}
\def\isafoldproof{}

Gergely Buday (Dec 06 2023 at 14:39):

As I see this deletes the definitions of various Isabelle LaTeX macros

Last updated: Feb 28 2025 at 08:24 UTC