summaryrefslogtreecommitdiff
path: root/Master
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2015-02-03 23:39:18 +0000
committerKarl Berry <karl@freefriends.org>2015-02-03 23:39:18 +0000
commit5186e33c6d218e9003f3da20bedfa840c1765d27 (patch)
treefccf82dae9fd18882993ef75df511c43809c08c5 /Master
parentee0e64e16ff5d81050d780da9298fecd9eeae3b8 (diff)
ebproof (3feb15)
git-svn-id: svn://tug.org/texlive/trunk@36202 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master')
-rw-r--r--Master/texmf-dist/doc/latex/ebproof/README16
-rw-r--r--Master/texmf-dist/doc/latex/ebproof/ebproof.pdfbin0 -> 196387 bytes
-rw-r--r--Master/texmf-dist/doc/latex/ebproof/ebproof.tex493
-rw-r--r--Master/texmf-dist/tex/latex/ebproof/ebproof.sty537
-rwxr-xr-xMaster/tlpkg/bin/tlpkg-ctan-check2
-rwxr-xr-xMaster/tlpkg/bin/tlpkginfo2
-rw-r--r--Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc1
-rw-r--r--Master/tlpkg/tlpsrc/ebproof.tlpsrc0
8 files changed, 1049 insertions, 2 deletions
diff --git a/Master/texmf-dist/doc/latex/ebproof/README b/Master/texmf-dist/doc/latex/ebproof/README
new file mode 100644
index 00000000000..a64bac6f41f
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/ebproof/README
@@ -0,0 +1,16 @@
+The ebproofs package provides commands to typeset proof trees, in the style of
+sequent calculus and related systems. The commands allow for writing
+inferences with any number of premisses and alignment of successive formulas
+on an arbitrary point. Various options allow complete control over spacing,
+styles of inference rules, placement of labels, etc.
+
+The distribution includes the following files:
+
+ - ebproof.sty : the package
+ - ebproof.pdf : the documentation
+ - ebproof.tex : the LaTeX source for the documentation
+
+The package requires pgfkeys (from TikZ/PGF) for the option system.
+
+This package is written by Emmanuel Beffara <manu@beffara.org>
+It is subject to the LaTeX Project Public License.
diff --git a/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf b/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf
new file mode 100644
index 00000000000..e58d9616168
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf
Binary files differ
diff --git a/Master/texmf-dist/doc/latex/ebproof/ebproof.tex b/Master/texmf-dist/doc/latex/ebproof/ebproof.tex
new file mode 100644
index 00000000000..acb05d56759
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/ebproof/ebproof.tex
@@ -0,0 +1,493 @@
+\documentclass{article}
+
+\DeclareRobustCommand\package[1]{\texttt{#1}}
+
+\title{The \package{ebproof} package}
+\author{Emmanuel Beffara \\ \url{manu@beffara.org}}
+\date{Version 1.0 \\ February 3, 2015}
+
+\usepackage{amssymb}
+\usepackage{color}
+\usepackage{fancyvrb}
+\usepackage[a4paper]{geometry}
+\usepackage[colorlinks=true,urlcolor=blue]{hyperref}
+\usepackage{multicol}
+
+\usepackage{tikz}
+\usetikzlibrary{decorations.pathmorphing}
+
+\usepackage{ebproof}
+
+\newcommand\lit[1]{\texttt{#1}}
+\newcommand\cs[1]{\lit{\char`\\#1}}
+\newcommand\env[1]{\lit{#1}}
+\newcommand\opt[1]{\lit{#1}}
+\newcommand\meta[1]{$\langle$\textit{#1}$\rangle$}
+\newcommand\oarg[1]{\lit{[}\meta{#1}\lit{]}}
+\newcommand\marg[1]{\lit{\{}\meta{#1}\lit{\}}}
+
+\newenvironment{csdoc}[1]{%
+ \smallbreak\noindent{#1}%
+ \begin{list}{}{%
+ \topsep=1ex%
+ }%
+ \item
+}{%
+ \end{list}%
+}
+
+\newenvironment{example}[1]{%
+ \def\exampleoptions{#1}%
+ \VerbatimOut{example.tex}}{%
+ \endVerbatimOut
+ \begin{center}
+ \begin{minipage}{.4\textwidth}
+ \input{example.tex}
+ \end{minipage}%
+ \begin{minipage}{.6\textwidth}
+ \small
+ \expandafter\VerbatimInput\expandafter[\exampleoptions]{example.tex}
+ \end{minipage}%
+ \end{center}
+}
+
+\setcounter{tocdepth}{2}
+
+\begin{document}
+\maketitle
+
+\begin{multicols}{2}
+ \tableofcontents
+\end{multicols}
+
+\section{Introduction}
+
+The \env{ebproof} package provides commands to typeset proof trees, in the
+style of sequent calculus and related systems:
+
+\begin{example}{gobble=2}
+ \begin{prooftree}
+ \Hypo{ \Gamma, A &\vdash B }
+ \Infer1[abs]{ \Gamma &\vdash A\to B }
+ \Hypo{ \Gamma \vdash A }
+ \Infer2[app]{ \Gamma \vdash B }
+ \end{prooftree}
+\end{example}
+
+The structure is very much inspired by the
+\href{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}{\package{bussproofs}}
+package, in particular for the postfix notation.
+I actually wrote \package{ebproof} because there were some limitations in
+\package{bussproofs} that I did not know how to lift, and also because I did
+not like some choices in that package (and also because it was fun to write).
+
+\section{Environments}
+
+The package provides the \env{prooftree} environment, in a standard and
+starred variants.
+
+\begin{csdoc}{
+ \cs{begin}\lit{\{prooftree\}}\oarg{options}
+ \meta{statements}
+ \cs{end}\lit{\{prooftree\}}}
+ Typeset the proof tree desribed by the \meta{statements}, as described in
+ section~\ref{sec:statements}.
+ The \meta{options} provide default formatting options for the proof tree.
+ This environment can be used either in math mode or in text mode.
+ It produces a proof tree at the current position in the text flow.
+\end{csdoc}
+
+\begin{csdoc}{
+ \cs{begin}\lit{\{prooftree*\}}\oarg{options}
+ \meta{statements}
+ \cs{end}\lit{\{prooftree*\}}}
+ Typeset the proof centered on a line of its own; it is essentially
+ equivalent to wrapping the \env{prooftree} environment inside a \env{center}
+ environment.
+\end{csdoc}
+
+\noindent
+The starred version is used in situations when a single proof will be
+displayed.
+The non-starred version is useful in order to integrate the proof into some
+larger structure, like two parts of a formula:
+
+\begin{example}{gobble=2}
+ \[
+ \begin{prooftree}
+ \Hypo{ \vdash A }
+ \Hypo{ \vdash B } \Infer1{ \vdash B, C }
+ \Infer2{ \vdash A\wedge B, C }
+ \end{prooftree}
+ \quad \rightsquigarrow \quad
+ \begin{prooftree}
+ \Hypo{ \vdash A } \Hypo{ \vdash B }
+ \Infer2{ \vdash A\wedge B }
+ \Infer1{ \vdash A\wedge B, C }
+ \end{prooftree}
+ \]
+\end{example}
+
+\section{Statements}
+\label{sec:statements}
+
+Statements describes proofs in postfix notation: when typesetting a proof tree
+whose last rule has, say, two premisses, you will first write statements for
+the subtree of the first premiss, then statements for the subtree of the
+second premiss, then a statement like \cs{Infer2}\{\meta{conclusion}\} to
+build an inference with these two subtrees as premisses and the given text as
+conclusion.
+
+Hence statements operate on a stack of proof trees.
+At the beginning of a \lit{prooftree} environment, the stack is empty.
+At the end, it must contain exactly one tree, which is the one that will be
+printed.
+
+\subsection{Basic statements}
+
+The basic statements for building proofs are the following, where
+\meta{options} stands for arbitrary options as described in
+section~\ref{sec:options}.
+\begin{csdoc}{\cs{Hypo}\oarg{options}\marg{text}}
+ Push a new proof tree consisting only in one conclusion line, with no
+ premiss and no line above, in other words a tree with only a leaf
+ (\cs{Hypo} stands for \emph{hypothesis}).
+\end{csdoc}
+\begin{csdoc}{\cs{Infer}\oarg{options}\marg{arity}\oarg{label}\marg{text}}
+ Build an inference step by taking some proof trees from the top of the
+ stack, assembling them with a rule joining their conclusions and putting a
+ new conclusion below.
+ The \meta{arity} is the number of sub-proofs, it may be any number
+ including 0 (in this case there will be a line above the conclusion but no
+ sub-proof).
+ If \meta{label} is present, it is used as the label on the right of the
+ inference line; it is equivalent to using the \opt{right label} option.
+\end{csdoc}
+
+The \meta{text} in these statements is the contents of the conclusion at the
+root of the tree that the statements create.
+It is typeset in math mode by default but any kind of formatting can be used
+instead, using the \opt{template} option.
+The \meta{label} text is formatted in horizontal text mode by default.
+
+Each proof tree has a vertical axis, used for alignment of successive steps.
+The position of the axis is deduced from the text of the conclusion at the
+root of the tree: if \meta{text} contains the alignment character \verb|&|
+then the axis is set at that position, otherwise the axis is set at the center
+of the conclusion text.
+The \cs{Infer} statement makes sure that the axis of the premiss is at the
+same position as the axis of the conclusion.
+If there are several premisses, it places the axis at the center between the
+left of the leftmost conclusion and the right of the rightmost conclusion:
+
+\begin{example}{gobble=2}
+ \begin{prooftree}
+ \Hypo{ &\vdash A, B, C }
+ \Infer1{ A &\vdash B, C }
+ \Infer1{ A, B &\vdash C }
+ \Hypo{ D &\vdash E }
+ \Infer2{ A, B, D &\vdash C, E }
+ \Infer1{ A, B &\vdash C, D, E }
+ \Infer1{ A &\vdash B, C, D, E }
+ \end{prooftree}
+\end{example}
+
+\subsection{Additional statements}
+
+The following additional statements may be used to affect the format of the
+last proof tree on the stack:
+
+\begin{csdoc}{\cs{Ellipsis}\marg{label}\marg{text}}
+ Typeset vertical dots, with a label on the right, and a new conclusion.
+ No inference lines are inserted.
+ \begin{example}{gobble=4}
+ \begin{prooftree}
+ \Hypo{ \Gamma &\vdash A }
+ \Ellipsis{foo}{ \Gamma &\vdash A, B }
+ \end{prooftree}
+ \end{example}
+\end{csdoc}
+
+\begin{csdoc}{\cs{Alter}\marg{code}}
+ Modify the proof with arbitrary commands, assuming that these commands do
+ not affect the size.
+ The \meta{code} is executed in an \cs{hbox} and is followed by the insertion
+ of the actual box with the current sub-proof.
+ It is mostly useful with \cs{color} commands:
+ \begin{example}{gobble=4}
+ \begin{prooftree}
+ \Hypo{ \Gamma, A &\vdash B }
+ \Infer1[abs]{ \Gamma &\vdash A\to B }
+ \Alter{\color{red}}
+ \Hypo{ \Gamma \vdash A }
+ \Infer2[app]{ \Gamma \vdash B }
+ \end{prooftree}
+ \end{example}
+\end{csdoc}
+
+\begin{csdoc}{\cs{Delims}\marg{left}\marg{right}}
+ Put left and right delimiters around the whole sub-proof, without changing
+ the alignment (the spacing is affected by the delimiters, however).
+ The \meta{left} text must contain an opening occurrence of \cs{left} and the
+ \meta{right} text must contain a matching occurrence of \cs{right}.
+ For instance, \verb|\Delims{\left(}{\right)}| will put the
+ sub-proof between parentheses.
+ \begin{example}{gobble=4}
+ \begin{prooftree}
+ \Hypo{ A_1 \vee \cdots \vee A_n }
+ \Hypo{ [A_i] }
+ \Ellipsis{}{ B }
+ \Delims{ \left( }{ \right)_{1\leq i\leq n} }
+ \Infer2{ B }
+ \end{prooftree}
+ \end{example}
+\end{csdoc}
+
+\section{Options}
+\label{sec:options}
+
+The formatting of trees, conclusion texts and inference rules is affected by
+options, specfied using the key-value system of PGF/TikZ, provided by the
+\package{pgfkeys} package.
+All options are in the \lit{/ebproof/} path in the key tree of
+\package{pgfkeys}.
+They can be set locally for a proof tree or for a single statement using
+optional arguments in the associated commands.
+
+\begin{csdoc}{\cs{ebproofset}\marg{options}}
+ Set some options.
+ The options will apply in the current scope; using this in preamble will
+ effectively set options globally.
+ Specific options may also be specified for each proof tree and for each
+ statement in a proof tree, using optional arguments.
+\end{csdoc}
+
+\subsection{General shape}
+
+The options in this section only make sense at the global level and at the
+proof level.
+Changing the proof style inside a \lit{proof} environment has undefined
+behaviour.
+
+\begin{csdoc}{\opt{proof style=}\meta{name}}
+ Set the general shape for representing proofs.
+ The following styles are provided:
+ \begin{csdoc}{\lit{upwards}}
+ This is the default style.
+ Proof trees grow upwards, with conclusions below and premisses above.
+ \end{csdoc}
+ \begin{csdoc}{\lit{downwards}}
+ Proof trees grow downwards, with conclusions above and premisses below.
+ \begin{example}{gobble=4}
+ \begin{prooftree}[proof style=downwards]
+ \Hypo{ \Gamma, A &\vdash B }
+ \Infer1[abs]{ \Gamma &\vdash A\to B }
+ \Hypo{ \Gamma \vdash A }
+ \Infer2[app]{ \Gamma \vdash B }
+ \end{prooftree}
+ \end{example}
+ \end{csdoc}
+\end{csdoc}
+
+In the optional argument of \lit{prooftree} environments, proof styles can
+be specified directly, without prefixing the name by ``\lit{proof style=}''.
+For instance, the first line of the example above could be written
+\cs{begin}\lit{\{prooftree\}[downwards]} equivalently.
+
+\begin{csdoc}{\opt{center=}\meta{boolean}}
+ If set to \lit{true}, the tree produced by the \env{prooftree} environment
+ will be vertically centered around the text line.
+ If set to \lit{false}, the base line of the tree will be the base line of
+ the conclusion.
+ The default value is \lit{true}.
+ \begin{example}{gobble=4}
+ \begin{prooftree}[center=false]
+ \Infer0{ A \vdash A }
+ \end{prooftree}
+ \qquad
+ \begin{prooftree}[center=false]
+ \Hypo{ \Gamma, A \vdash B }
+ \Infer1{ \Gamma \vdash A \to B }
+ \end{prooftree}
+ \end{example}
+\end{csdoc}
+
+\subsection{Spacing}
+
+\begin{csdoc}{\opt{separation=}\meta{dimension}}
+ The horizontal separation between sub-proofs in an inference.
+ The default value is \lit{1.5em}.
+ \begin{example}{gobble=4}
+ \begin{prooftree}[separation=0.5em]
+ \Hypo{ A } \Hypo{ B } \Infer2{ C }
+ \Hypo{ D } \Hypo{ E } \Hypo{ F } \Infer3{ G }
+ \Hypo{ H } \Infer[separation=3em]3{ K }
+ \end{prooftree}
+ \end{example}
+\end{csdoc}
+
+\begin{csdoc}{\opt{rule margin=}\meta{dimension}}
+ The spacing above and below inference lines.
+ The default value is \lit{0.7ex}.
+ \begin{example}{gobble=4}
+ \begin{prooftree}[rule margin=2ex]
+ \Hypo{ \Gamma, A &\vdash B }
+ \Infer1[abs]{ \Gamma &\vdash A\to B }
+ \Hypo{ \Gamma \vdash A }
+ \Infer2[app]{ \Gamma \vdash B }
+ \end{prooftree}
+ \end{example}
+\end{csdoc}
+
+\subsection{Shape of inference lines}
+
+\begin{csdoc}{\opt{rule style=}\meta{name}}
+ Set the shape of inference lines.
+ The following values are provided:
+ \begin{csdoc}{\opt{simple}}
+ A simple horizontal rule is drawn.
+ This is the default style.
+ \end{csdoc}
+ \begin{csdoc}{\opt{no rule}}
+ No inference line is drawn.
+ A single space of the length of \lit{rule margin} is inserted.
+ \end{csdoc}
+ \begin{csdoc}{\opt{double}}
+ A double line is drawn.
+ \end{csdoc}
+ \begin{csdoc}{\opt{dashed}}
+ A single dashed line is drawn.
+ \end{csdoc}
+ The precise rendering is influenced by parameters specified below.
+ Arbitrary new shapes can defined using the \lit{rule code} option described
+ afterwards.
+\end{csdoc}
+
+In the optional argument of the \cs{Infer} statement, rule styles can be
+specified directly, without prefixing the style name by ``\lit{rule style=}''.
+For instance, \cs{Infer}\lit{[dashed]} is equivalent to
+\cs{Infer}\lit{[rule style=dashed]}.
+
+\begin{example}{gobble=2}
+ \begin{prooftree}
+ \Hypo{ \Gamma &\vdash A \to B }
+ \Infer[no rule]1{ \Gamma &\vdash {!A} \multimap B }
+ \Hypo{ \Delta &\vdash A }
+ \Infer[rule thickness=2pt]1{ \Delta &\vdash {!A} }
+ \Infer0{ B \vdash B }
+ \Infer[dashed]2{ \Delta, {!A}\multimap B \vdash B }
+ \Infer2{ \Gamma, \Delta &\vdash B }
+ \Infer[double]1{ \Gamma \cup \Delta &\vdash B }
+ \end{prooftree}
+\end{example}
+
+\begin{csdoc}{\opt{rule thickness=}\meta{dimension}}
+ The thickness of inference lines.
+ It is \lit{0.4pt} by default.
+\end{csdoc}
+\begin{csdoc}{\opt{rule separation=}\meta{dimension}}
+ The distance between the two lines in the \lit{double} rule style.
+ It is \lit{2pt} by default.
+\end{csdoc}
+\begin{csdoc}{\opt{rule dash length=}\meta{dimension}}
+ The length of dashes in the \lit{dashed} rule style.
+ It is \lit{0.2em} by default.
+\end{csdoc}
+\begin{csdoc}{\opt{rule dash space=}\meta{dimension}}
+ The space between dashes in the \lit{dashed} rule style.
+ It is \lit{0.3em} by default.
+\end{csdoc}
+
+\begin{csdoc}{\opt{rule code=}\meta{code}}
+ This option is used to define an arbitrary shape for rules.
+ The \meta{code} is used to render the rule, it is executed in vertical mode
+ in a \cs{vbox} whose \cs{hsize} is set to the width of the rule.
+ Margins above and below are inserted automatically (they can be removed by
+ setting \lit{rule margin} to \lit{0pt}).
+
+ \begin{example}{gobble=4}
+ \begin{prooftree}[rule code={\hbox{\tikz
+ \draw[decorate,decoration={snake,amplitude=.3ex}]
+ (0,0) -- (\hsize,0);}}]
+ \Hypo{ \Gamma &\vdash A }
+ \Infer1{ \Gamma &\vdash A, \ldots, A }
+ \Hypo{ \Delta, A, \ldots, A \vdash \Theta }
+ \Infer2{ \Gamma, \Delta \vdash \Theta }
+ \end{prooftree}
+ \end{example}
+ Note that this example requires the \package{tikz} package, with the
+ \package{decorations.pathmorphing} library for the \lit{snake} decoration.
+\end{csdoc}
+
+The option \opt{rule code} is particularly useful in a ``styles'' in the sense of
+\package{pgfkeys} as it allows to define new rule styles.
+The allowed values for \opt{rule style} are actually defined this way.
+The above example could be turned into a new rule style \lit{zigzag} with the
+following command:
+\begin{example}{gobble=2}
+ \ebproofset{
+ rule style/zigzag/.style={rule code={\hbox{\tikz
+ \draw[decorate,decoration={snake,amplitude=.3ex}]
+ (0,0) -- (\hsize,0);}}}}
+ \begin{prooftree}
+ \Hypo{ \Gamma &\vdash A }
+ \Infer1{ \Gamma &\vdash A, \ldots, A }
+ \Hypo{ \Delta, A, \ldots, A \vdash \Theta }
+ \Infer[zigzag]2{ \Gamma, \Delta \vdash \Theta }
+ \end{prooftree}
+\end{example}
+
+\subsection{Format of conclusions}
+
+\begin{csdoc}{%
+ \opt{template=}\meta{macro} \\
+ \opt{left template=}\meta{macro} \\
+ \opt{right template=}\meta{macro}}
+ Defines how conclusions are formatted.
+ The macros are arbitrary \TeX\ code, composed in horizontal mode, with the
+ macro argument \verb|#1| standing for the actual text passed to the
+ \cs{Hypo} and \cs{Infer} statements.
+ The \opt{template} value is used for conclusions with no alignment mark.
+ The \opt{left template} and \opt{right template} values are used on the left
+ and right side of the alignment mark when it is present.
+ The default value for \opt{template} is simply \verb|$#1$|, so that
+ conclusions are set in math mode.
+ The default values for \opt{left template} and \opt{right template} are
+ similar, with spacing assuming that a relation symbol is put near the
+ alignment mark, so that \verb|\Infer1{A &\vdash B}| is spaced correctly.
+
+ \begin{example}{gobble=4}
+ \begin{prooftree}[template=(\textbf{#1})]
+ \Hypo{ foo }
+ \Hypo{ bar }
+ \Infer1{ baz }
+ \Infer2{ quux }
+ \end{prooftree}
+ \end{example}
+\end{csdoc}
+
+\subsection{Format of labels}
+
+\begin{csdoc}{%
+ \opt{left label=}\meta{text} \\
+ \opt{right label=}\meta{text}}
+ The text to use as the labels of the rules, on the left and on the right
+ of the inference line.
+ Using the second optional argument in \cs{Infer} is equivalent to setting
+ the \env{right label} option with the value of that argument.
+\end{csdoc}
+\begin{csdoc}{%
+ \opt{left label template=}\meta{macro} \\
+ \opt{right label template=}\meta{macro}}
+ These macros are used to typeset the text of labels on the left and right of
+ inference lines.
+ The default values are \verb|#1| so that labels are set in plain text mode.
+\end{csdoc}
+
+\begin{csdoc}{\opt{label separation=}\meta{dimension}}
+ The spacing between an inference lines and its labels.
+ The default value is \lit{0.5em}.
+\end{csdoc}
+
+
+\end{document}
diff --git a/Master/texmf-dist/tex/latex/ebproof/ebproof.sty b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty
new file mode 100644
index 00000000000..e8018884a29
--- /dev/null
+++ b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty
@@ -0,0 +1,537 @@
+% This package contains macros for typesetting proof trees.
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{ebproof}[2015/02/03 v1.0 EB's proof trees]
+
+% The |pgfkeys| package is used for the parameters in proof construction.
+% The |ifthen| package is used for some tests.
+
+\RequirePackage{pgfkeys}
+\RequirePackage{ifthen}
+
+%%% Registers and internal parameters
+
+\newbox\ebproof@leftbox
+\newbox\ebproof@rightbox
+\newif\ifebproof@updown \ebproof@updownfalse
+\newif\ifebproof@center \ebproof@centertrue
+
+\def\ebproof@template#1{$#1$}
+\def\ebproof@lefttemplate#1{$#1\mathrel{}$}
+\def\ebproof@righttemplate#1{$\mathrel{}#1$}
+\def\ebproof@leftlabeltemplate#1{#1}
+\def\ebproof@rightlabeltemplate#1{#1}
+\def\ebproof@setleftlabel{\setbox\ebproof@leftbox=\box\voidb@x}
+\def\ebproof@setrightlabel{\setbox\ebproof@rightbox=\box\voidb@x}
+
+%%% Parameters
+
+\def\ebproofset#1{\pgfqkeys{/ebproof}{#1}}
+
+\ebproofset{
+%
+% general shape
+%
+center/.is if=ebproof@center,
+proof style/.is choice,
+proof style/upwards/.code={\ebproof@updownfalse},
+proof style/downwards/.code={\ebproof@updowntrue},
+%
+% spacing
+%
+separation/.initial=1.5em,
+rule margin/.initial=.7ex,
+%
+% shape of inference lines
+%
+rule thickness/.initial=.4pt,
+rule separation/.initial=2pt,
+rule dash length/.initial=.2em,
+rule dash space/.initial=.3em,
+rule code/.initial=,
+%
+% templates
+%
+template/.code={\def\ebproof@template##1{#1}},
+left template/.code={\def\ebproof@lefttemplate##1{#1}},
+right template/.code={\def\ebproof@righttemplate##1{#1}},
+%
+% labels
+%
+left label/.code={%
+ \def\ebproof@setleftlabel{%
+ \setbox\ebproof@leftbox=\hbox{\ebproof@leftlabeltemplate{#1}}}},
+right label/.code={%
+ \def\ebproof@setrightlabel{%
+ \setbox\ebproof@rightbox=\hbox{\ebproof@rightlabeltemplate{#1}}}},
+left label template/.code={\def\ebproof@leftlabeltemplate##1{#1}},
+right label template/.code={\def\ebproof@rightlabeltemplate##1{#1}},
+label separation/.initial=0.5em,
+}
+
+% Rule styles
+
+\pgfqkeys{/ebproof/rule style}{
+.is choice,
+.search also=/ebproof,
+simple/.style={/ebproof/rule code={%
+ \hrule height \pgfkeysvalueof{/ebproof/rule thickness}\relax
+ }},
+%
+no rule/.style={/ebproof/rule code=},
+%
+double/.style={/ebproof/rule code={%
+ \hrule height \pgfkeysvalueof{/ebproof/rule thickness}
+ \kern\pgfkeysvalueof{/ebproof/rule separation}%
+ \hrule height \pgfkeysvalueof{/ebproof/rule thickness}
+ }},
+%
+dashed/.style={/ebproof/rule code={%
+ \hbox to \hsize{%
+ \@tempdima=\pgfkeysvalueof{/ebproof/rule dash space}%
+ \divide\@tempdima2%
+ \kern-\@tempdima%
+ \cleaders\hbox{%
+ \kern\@tempdima%
+ \vrule
+ height \pgfkeysvalueof{/ebproof/rule thickness}
+ width \pgfkeysvalueof{/ebproof/rule dash length}%
+ \kern\@tempdima
+ }\hfill
+ \kern-\@tempdima
+ }%
+ }},
+%
+simple % use the 'simple' rule style by default
+}
+
+%%% Storage
+
+% Proof trees are represented as a data structure that consists of the
+% following data:
+%
+% - box : the tree itself, as a box, with the base line on that of
+% the conclusion
+% - left : the distance from the left of the box to the left of the
+% conclusion
+% - right : the distance from the right of the box to the right of the
+% conclusion
+% - axis : the distance from the left of the box to the vertical axis
+% of the conclusion
+%
+% TeX does not actually provide data structures, so we have to encode things.
+% First we provide local allocators, for temporary allocation of registers in
+% a group. Dimensions are initialized to 0pt.
+
+\def\ebproof@localdimen#1{%
+ \advance\count11\@ne% \count11 is the number of the last allocated \dimen
+ \expandafter\dimendef\csname#1\endcsname=\count11%
+ \csname#1\endcsname=0pt\relax}
+
+% For boxes, the allocator must be used as
+%
+% \ebproof@localbox{NAME}=\hbox{...}
+%
+% in order to set the value of the box.
+
+\def\ebproof@localbox#1{%
+ \advance\count14\@ne% \count14 is the number of the last allocated \box
+ \expandafter\chardef\csname#1\endcsname\count14%
+ \setbox\csname#1\endcsname}
+
+% From this we deduce an allocator for data structures. This allocator
+% receives a base name |A| and defines the registers |\A@box|, |\A@left|,
+% |\A@right| and |\A@axis|. The macro is used like |\ebproof@localbox|, by
+% providing a value for the box.
+
+\def\ebproof@alloc#1{%
+ \ebproof@localdimen{#1@left}%
+ \ebproof@localdimen{#1@right}%
+ \ebproof@localdimen{#1@axis}%
+ \ebproof@localbox{#1@box}}
+
+% Logically, such structures are stored on a stack. However, TeX does not
+% provide data structures, so we encode them using what we actually have. A
+% stack for boxes is implemented using a global hbox |\ebproof@box@stack| that
+% contains all the boxes successively, and the |\lastbox| primitive allows us
+% to pop elements from there. A macro |\ebproof@stack| is used to store the
+% dimensions textually: the empty stack is an empty macro, and a non-empty
+% stack is represented as |{left}{right}{axis}{tail}|. We maintain a counter
+% |\ebproof@level| with the number of elements on the stack, for consistency
+% checks.
+
+\newcount\ebproof@level
+\newbox\ebproof@box@stack
+\newbox\ebproof@box@temp
+
+% Clear the stack.
+
+\def\ebproof@clear{%
+ \global\ebproof@level=0%
+ \global\setbox\ebproof@box@stack=\box\voidb@x%
+ \gdef\ebproof@stack{}}
+
+% Push an allocated structure (by name) on the stack.
+
+\def\ebproof@push#1{%
+ \global\advance\ebproof@level1\relax
+ \global\setbox\ebproof@box@stack=\hbox{%
+ \unhbox\ebproof@box@stack\copy\csname#1@box\endcsname}%
+ \xdef\ebproof@stack{%
+ {\the\csname#1@left\endcsname}%
+ {\the\csname#1@right\endcsname}%
+ {\the\csname#1@axis\endcsname}%
+ {\ebproof@stack}}}
+
+% Allocate a structure and pop its value from the top of the stack.
+
+\def\ebproof@pop#1{%
+ \ifnum\ebproof@level>0\relax
+ \global\advance\ebproof@level-1\relax
+ \global\setbox\ebproof@box@stack=\hbox{%
+ \unhbox\ebproof@box@stack
+ \global\setbox\ebproof@box@temp=\lastbox}%
+ \ebproof@alloc{#1}=\box\ebproof@box@temp%
+ \begingroup\def\pop##1##2##3##4{\endgroup%
+ \csname#1@left\endcsname=##1\relax
+ \csname#1@right\endcsname=##2\relax
+ \csname#1@axis\endcsname=##3\relax
+ \gdef\ebproof@stack{##4}}%
+ \expandafter\pop\ebproof@stack
+ \else
+ \PackageError{ebproof}{%
+ Missing premiss in a proof tree}{}%
+ \ebproof@alloc{#1}=\box\voidb@x%
+ \fi}
+
+
+%%% Making boxes
+
+% Push a box with the axis in the middle.
+
+\def\ebproof@pushsimple#1{%
+ \begingroup
+ \ebproof@alloc{A}=\hbox{#1}%
+ \A@axis=.5\wd\A@box
+ \ebproof@push{A}%
+ \endgroup}
+
+% Push a box made of two halves, with the axis between the halves.
+
+\def\ebproof@pushsplit#1#2{%
+ \begingroup
+ \ebproof@alloc{A}=\hbox{#1}%
+ \A@axis=\wd\A@box
+ \setbox\A@box=\hbox{\unhbox\A@box#2}%
+ \ebproof@push{A}%
+ \endgroup}
+
+% Join horizontally the two elements at the top of the stack.
+
+\def\ebproof@joinh{%
+ \begingroup
+ \ebproof@pop{A}%
+ \ebproof@pop{B}%
+ \ebproof@alloc{C}=\hbox{%
+ \box\B@box
+ \kern\pgfkeysvalueof{/ebproof/separation}%
+ \box\A@box}%
+ \C@left=\B@left
+ \C@right=\A@right
+ \C@axis=\wd\C@box
+ \advance\C@axis\B@left
+ \advance\C@axis-\A@right
+ \divide\C@axis2\relax
+ \ebproof@push{C}%
+ \endgroup}
+
+% An $n$-ary version of the horizontal join.
+
+\def\ebproof@joinh@multi#1{%
+ \begingroup
+ \countdef\c=1
+ \c=#1\relax%
+ \ifnum\c=0
+ \ebproof@alloc{X}=\hbox{}%
+ \ebproof@push{X}%
+ \else
+ \ebproof@joinh@loop
+ \fi
+ \endgroup}
+\def\ebproof@joinh@loop{%
+ \ifnum\c>1
+ \ebproof@joinh
+ \advance\c-1
+ \expandafter\ebproof@joinh@loop
+ \fi}
+
+% Append the last element to the right of the previous one, without changing
+% its alignment.
+
+\def\ebproof@joinright{%
+ \begingroup
+ \ebproof@pop{A}%
+ \ebproof@pop{B}%
+ \ebproof@alloc{C}=\hbox{%
+ \box\B@box
+ \kern\pgfkeysvalueof{/ebproof/separation}%
+ \copy\A@box}%
+ \C@left=\B@left
+ \C@right=\B@right
+ \advance\C@right\wd\A@box
+ \advance\C@right\pgfkeysvalueof{/ebproof/separation}%
+ \ebproof@push{C}%
+ \endgroup}
+
+% Join vertically the two elements at the top of the stack, with a horizontal
+% rule of the appropriate size.
+
+\def\ebproof@joinv{%
+ \begingroup
+ \ebproof@setleftlabel
+ \ebproof@setrightlabel
+ \ebproof@pop{A}%
+ \ebproof@pop{B}%
+ %
+ \ebproof@alloc{C}=\box\voidb@x%
+ \ebproof@localdimen{A@shift}%
+ \ebproof@localdimen{B@shift}%
+ \ebproof@localdimen{R@shift}%
+ \ebproof@localdimen{R@raise}%
+ \ebproof@localdimen{R@width}%
+ \ebproof@localdimen{C@width}%
+ \ebproof@localdimen{tmp}%
+ %
+ % The placement of the boxes and the axis of the result
+ \ifdim\A@axis>\B@axis
+ \A@shift=0pt%
+ \B@shift=\A@axis
+ \advance\B@shift-\B@axis
+ \C@axis=\A@axis
+ \else
+ \A@shift=\B@axis
+ \advance\A@shift-\A@axis
+ \B@shift=0pt%
+ \C@axis=\B@axis
+ \fi
+ % The paddings of the result
+ \C@left=\A@left
+ \advance\C@left\A@shift
+ \C@right=\A@right
+ \tmp=\wd\B@box
+ \advance\tmp\B@shift
+ \advance\tmp-\wd\A@box
+ \advance\tmp-\A@shift
+ \ifdim\tmp>0pt%
+ \C@width=\wd\B@box
+ \advance\C@width\B@shift
+ \advance\C@right\tmp
+ \else
+ \C@width=\wd\A@box
+ \advance\C@width\A@shift
+ \fi
+ % The position of the rule
+ \R@shift=\A@left
+ \advance\R@shift\A@shift
+ \tmp=\B@left
+ \advance\tmp\B@shift
+ \ifdim\R@shift>\tmp
+ \R@shift=\tmp
+ \fi
+ % The width of the rule
+ \R@width=\wd\A@box
+ \advance\R@width\A@shift
+ \advance\R@width-\A@right
+ \tmp=\wd\B@box
+ \advance\tmp\B@shift
+ \advance\tmp-\B@right
+ \ifdim\tmp>\R@width
+ \R@width=\tmp
+ \fi
+ \advance\R@width-\R@shift
+ % Make the rule box
+ \ebproof@localbox{R@box}=\vbox{%
+ \hsize=\R@width
+ \hrule width \R@width height 0pt\relax
+ \kern\pgfkeysvalueof{/ebproof/rule margin}%
+ \pgfkeysgetvalue{/ebproof/rule code}{\@rulecode}%
+ \ifx\@rulecode\@empty\else
+ \@rulecode
+ \unskip% so that only one margin is inserted if no rule is drawn
+ \kern\pgfkeysvalueof{/ebproof/rule margin}%
+ \fi
+ }%
+ % Shift things if the left box is wider than |\R@shift|
+ \ifvoid\ebproof@leftbox\else
+ \tmp=\wd\ebproof@leftbox
+ \advance\tmp\pgfkeysvalueof{/ebproof/label separation}
+ \ifdim\tmp>\R@shift
+ \advance\tmp-\R@shift
+ \advance\A@shift\tmp
+ \advance\B@shift\tmp
+ \advance\C@left\tmp
+ \advance\C@axis\tmp
+ \advance\C@width\tmp
+ \R@shift=0pt\relax
+ \else
+ \advance\R@shift-\tmp
+ \fi
+ \fi
+ % Compute how the rule box must be shifted so that labels are aligned
+ \ebproof@localbox{RC@box}=\hbox{$\vcenter{\copy\R@box}$}%
+ \R@raise=\ht\R@box
+ \advance\R@raise-\ht\RC@box
+ % Make the complete rule box
+ \setbox\RC@box=\hbox{%
+ \ifvoid\ebproof@leftbox\else
+ \copy\ebproof@leftbox
+ \kern\pgfkeysvalueof{/ebproof/label separation}
+ \fi
+ \box\RC@box
+ \ifvoid\ebproof@rightbox\else
+ \kern\pgfkeysvalueof{/ebproof/label separation}
+ \copy\ebproof@rightbox
+ \fi}
+ % Adapt the dimensions on the right if the total rule width is too large
+ \tmp=\wd\RC@box
+ \advance\tmp\R@shift
+ \ifdim\tmp>\C@width
+ \advance\tmp-\C@width
+ \advance\C@right\tmp
+ \fi
+ % Cancel the labels' height and depth
+ \setbox\RC@box=\hbox{\raise\R@raise\box\RC@box}
+ \ht\RC@box=\ht\R@box
+ \dp\RC@box=\dp\R@box
+ % Make the box
+ \ifebproof@updown
+ \setbox\C@box=\vtop{%
+ \moveright\A@shift\box\A@box
+ \hrule height 0pt
+ \moveright\R@shift\box\RC@box%
+ \hrule height 0pt
+ \moveright\B@shift\box\B@box}%
+ \else
+ \setbox\C@box=\vbox{%
+ \moveright\B@shift\box\B@box
+ \hrule height 0pt
+ \moveright\R@shift\box\RC@box%
+ \hrule height 0pt
+ \moveright\A@shift\box\A@box}%
+ \fi
+ \ebproof@push{C}%
+ \endgroup}
+
+%%% Modifying boxes
+
+% Alter a proof with a command that does not affect the size. Typically useful
+% with |\color| commands.
+
+\def\ebproof@alter#1{%
+ \begingroup
+ \ebproof@pop{A}%
+ \setbox\A@box=\hbox{{#1\box\A@box}}%
+ \ebproof@push{A}%
+ \endgroup}
+
+% Insert |\left| and |\right| delimiters without changing the alignment
+
+\def\ebproof@delims#1#2{%
+ \begingroup
+ \ebproof@pop{TREE}%
+ \ebproof@localbox{@SHIFTED}=%
+ \hbox{$\vcenter{\copy\TREE@box}$}%
+ \ebproof@localbox{@LEFT}=%
+ \hbox{$#1\vrule height \ht\@SHIFTED depth \dp\@SHIFTED width 0pt\right.$}%
+ \ebproof@localbox{@RIGHT}=%
+ \hbox{$\left.\vrule height \ht\@SHIFTED depth \dp\@SHIFTED width 0pt#2$}%
+ \ebproof@localdimen{dy}
+ \dy=\dp\@SHIFTED
+ \advance\dy-\dp\TREE@box
+ \ebproof@alloc{A}=%
+ \hbox{\raise\dy\hbox{\copy\@LEFT\box\@SHIFTED\copy\@RIGHT}}%
+ \A@left=\wd\@LEFT \advance\A@left\TREE@left
+ \A@right=\wd\@RIGHT \advance\A@right\TREE@right
+ \A@axis=\wd\@LEFT \advance\A@axis\TREE@axis
+ \ebproof@push{A}%
+ \endgroup}
+
+%%% High-level commands
+
+% Push a box with default formatting, using explicit alignment if the code
+% contains a |&| character
+
+\def\ebproof@hypo@parse#1&#2&#3\ebproof@hypo@stop{
+ \ifthenelse{\equal{#3}{}}%
+ {\ebproof@pushsimple{\ebproof@template{#1}}}%
+ {\ebproof@pushsplit
+ {\ebproof@lefttemplate{#1}}%
+ {\ebproof@righttemplate{#2}}}}
+
+\newcommand\ebproof@hypo[2][]{%
+ {\ebproofset{#1}\ebproof@hypo@parse#2&&\ebproof@hypo@stop}}
+
+% Build a n-ary rule
+
+\def\ebproof@infer{%
+ \@ifnextchar[{\ebproof@infer@}{\ebproof@infer@[]}}
+\def\ebproof@infer@[#1]#2{%
+ \@ifnextchar[{\ebproof@infer@@{#1}{#2}}{\ebproof@infer@@{#1}{#2}[]}}
+\def\ebproof@infer@@#1#2[#3]#4{{%
+ \pgfqkeys{/ebproof/rule style}{.search also=/ebproof,#1}%
+ \ebproof@joinh@multi{#2}%
+ \ebproof@hypo{#4}%
+ \ifthenelse{\equal{#3}{}}{}{\ebproofset{right label={#3}}}%
+ \ebproof@joinv}}
+
+% Ellipsis with vertical dots
+
+\def\ebproof@ellipsis#1#2{{%
+ \ebproofset{rule code=}%
+ \ebproof@pushsplit{}{%
+ \setbox0=\vbox{\kern1.2ex\hbox{\ignorespaces#1}\hrule height 0pt\kern1.2ex}%
+ \vbox to\ht0{\xleaders\vbox to .8ex{\vss\hbox{.}\vss}\vfill}%
+ \rlap{ \box0}}%
+ \ebproof@joinv
+ \ebproof@hypo{#2}%
+ \ebproof@joinv}}
+
+%%% Environment interface
+
+\ebproof@clear
+
+\def\ebproof@begin{%
+ \edef\ebproof@start@level{\the\ebproof@level}%
+ \setbox1=\vbox\bgroup
+ \let\Hypo=\ebproof@hypo
+ \let\Infer=\ebproof@infer
+ \let\Ellipsis=\ebproof@ellipsis
+ \let\Alter=\ebproof@alter
+ \let\Delims=\ebproof@delims}
+\def\ebproof@end{%
+ \egroup
+ \ebproof@pop{X}%
+ \ifnum\ebproof@level=\ebproof@start@level\else
+ \PackageError{ebproof}{Malformed proof tree}{%
+ Some hypotheses were declared but not used in this tree.}%
+ \fi
+ \ifebproof@center
+ \hbox{$\vcenter{\hbox{\box\X@box}}$}%
+ \else
+ \box\X@box
+ \fi
+ \global\setbox\ebproof@box@temp=\box1}
+
+\newenvironment{prooftree}[1][]{%
+ \pgfqkeys{/ebproof/proof style}{.search also=/ebproof,#1}%
+ \leavevmode\ebproof@begin
+}{%
+ \ebproof@end}
+
+\newenvironment{prooftree*}[1][]{%
+ \center
+ \pgfqkeys{/ebproof/proof style}{.search also=/ebproof,#1}%
+ \leavevmode\ebproof@begin
+}{%
+ \ebproof@end
+ \endcenter}
diff --git a/Master/tlpkg/bin/tlpkg-ctan-check b/Master/tlpkg/bin/tlpkg-ctan-check
index 648f02b01e5..2ed3e71da42 100755
--- a/Master/tlpkg/bin/tlpkg-ctan-check
+++ b/Master/tlpkg/bin/tlpkg-ctan-check
@@ -178,7 +178,7 @@ my @TLP_working = qw(
dvdcoll dvgloss dviasm dviincl dvipdfmx-def
dvipsconfig dynblocks dyntree
ean ean13isbn easy easy-todo easyfig easylist
- ebezier ebgaramond ebgaramond-maths ebong ebook ebsthesis
+ ebezier ebgaramond ebgaramond-maths ebong ebook ebproof ebsthesis
ec ecc ecclesiastic ecltree eco economic
ecv ed edfnotes edmac edmargin ednotes eemeir eepic efbox egameps
egplot eiad eiad-ltx eijkhout einfuehrung ejpecp ekaia
diff --git a/Master/tlpkg/bin/tlpkginfo b/Master/tlpkg/bin/tlpkginfo
index 6e764c71d0a..2bde3b9d208 100755
--- a/Master/tlpkg/bin/tlpkginfo
+++ b/Master/tlpkg/bin/tlpkginfo
@@ -17,7 +17,7 @@ sub main {
# erroneous or problematic tds files (when new, tell RobinF and author)
$erroneous_tds = join ("|",
- qw(countriesofeurope dad engpron gost hacm he-she hobby imtekda
+ qw(countriesofeurope dad ebproof engpron gost hacm he-she hobby imtekda
mathdesign spanish sttools),
);
diff --git a/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc b/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc
index ac29fcbef45..730d8b34f7f 100644
--- a/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc
+++ b/Master/tlpkg/tlpsrc/collection-mathextra.tlpsrc
@@ -18,6 +18,7 @@ depend commath
depend concmath
depend concrete
depend conteq
+depend ebproof
depend eqnarray
depend extarrows
depend extpfeil
diff --git a/Master/tlpkg/tlpsrc/ebproof.tlpsrc b/Master/tlpkg/tlpsrc/ebproof.tlpsrc
new file mode 100644
index 00000000000..e69de29bb2d
--- /dev/null
+++ b/Master/tlpkg/tlpsrc/ebproof.tlpsrc