# HG changeset patch # User urbanc # Date 1340882726 0 # Node ID 66e0ec8acedcc2ba628b3a063f987f8b72ca34f8 # Parent 1b9163229f3f7005f52f01e566d05f0409069e4c added some slides for an informal talk about PIP diff -r 1b9163229f3f -r 66e0ec8acedc prio/IsaMakefile --- a/prio/IsaMakefile Thu Jun 21 15:04:48 2012 +0000 +++ b/prio/IsaMakefile Thu Jun 28 11:25:26 2012 +0000 @@ -2,7 +2,7 @@ ## targets default: itp -all: session itp +all: session itp slides1 ## global settings @@ -16,9 +16,24 @@ ## Slides +session1: Slides/ROOT1.ML \ + Slides/document/root* \ + Slides/Slides1.thy + @$(USEDIR) -D generated -f ROOT1.ML HOL Slides + +slides1: session1 + rm -f Slides/generated/*.aux # otherwise latex will fall over + cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex + cp Slides/generated/root.beamer.pdf Slides/slides.pdf + +# main files + session: ./ROOT.ML ./*.thy @$(USEDIR) -b -D generated -f ROOT.ML HOL Prio + +# itp paper + itp: Paper/*.thy Paper/*.ML @$(USEDIR) -D generated -f ROOT.ML Prio Paper rm -f Paper/generated/*.aux # otherwise latex will fall over diff -r 1b9163229f3f -r 66e0ec8acedc prio/Slides/ROOT1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/prio/Slides/ROOT1.ML Thu Jun 28 11:25:26 2012 +0000 @@ -0,0 +1,7 @@ +(*show_question_marks := false;*) + +no_document use_thy "../CpsG"; +no_document use_thy "../ExtGG"; +no_document use_thy "~~/src/HOL/Library/LaTeXsugar"; +quick_and_dirty := true; +use_thy "Slides1" \ No newline at end of file diff -r 1b9163229f3f -r 66e0ec8acedc prio/Slides/Slides1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/prio/Slides/Slides1.thy Thu Jun 28 11:25:26 2012 +0000 @@ -0,0 +1,550 @@ +(*<*) +theory Slides1 +imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar" +begin + +notation (latex output) + set ("_") and + Cons ("_::/_" [66,65] 65) + +ML {* + open Printer; + show_question_marks_default := false; + *} + +notation (latex output) + Cons ("_::_" [78,77] 73) and + vt ("valid'_state") and + runing ("running") and + birthtime ("last'_set") and + If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and + Prc ("'(_, _')") and + holding ("holds") and + waiting ("waits") and + Th ("T") and + Cs ("C") and + readys ("ready") and + depend ("RAG") and + preced ("prec") and + cpreced ("cprec") and + dependents ("dependants") and + cp ("cprec") and + holdents ("resources") and + original_priority ("priority") and + DUMMY ("\<^raw:\mbox{$\_\!\_$}>") + +(*>*) + + + +text_raw {* + \renewcommand{\slidecaption}{London, 28 June 2012} + \newcommand{\bl}[1]{#1} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame} + \frametitle{% + \begin{tabular}{@ {}c@ {}} + \\[8mm] + \Large A Provably Correct Implementation\\[-3mm] + \Large of the Priority Inheritance Protocol\\[0mm] + \end{tabular}} + + \begin{center} + \small Christian Urban\\ + \end{center} + + \begin{center} + \small joint work with Xingyuan Zhang and Chunhan Wu\medskip \\ + \small \mbox{from the PLA University of Science and Technology in Nanjing} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Isabelle Theorem Prover} + My background: + + \begin{itemize} + \item mechanical reasoning about languages with binders (Nominal)\medskip + \item Barendregt's variable convention can lead to \alert{false}\medskip + \item found a bug in a proof by Bob Harper and Frank Pfenning (CMU) on + LF (ACM TOCL, 2005) + \end{itemize} + + \begin{textblock}{6}(6.5,12.5) + \includegraphics[scale=0.28]{isabelle1.png} + \end{textblock} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Real-Time OSes} + \large + + \begin{itemize} + \item Processes have priorities\\[5mm] + \item Resources can be locked and unlocked + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Problem} + \Large + + \begin{center} + \begin{tabular}{l} + \alert{H}igh-priority process\\[4mm] + \onslide<2->{\alert{M}edium-priority process}\\[4mm] + \alert{L}ow-priority process\\[4mm] + \end{tabular} + \end{center} + + \onslide<3->{ + \begin{itemize} + \item \alert{Priority Inversion} @{text "\"} \alert{H $<$ L} + \item<4> avoid indefinite priority inversion + \end{itemize}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Mars Pathfinder Mission 1997} + \Large + + \begin{center} + \includegraphics[scale=0.26]{pathfinder.jpg} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Solution} + \Large + + \alert{Priority Inheritance Protocol (PIP):} + + \begin{center} + \begin{tabular}{l} + \alert{H}igh-priority process\\[4mm] + \textcolor{gray}{Medium-priority process}\\[4mm] + \alert{L}ow-priority process\\[21mm] + {\normalsize (temporarily raise its priority)} + \end{tabular} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{\mbox{}} + + \begin{quote} + ``Priority inheritance is neither ef$\!$ficient nor reliable. + Implementations are either incomplete (and unreliable) + or surprisingly complex and intrusive.'' + \end{quote}\medskip + + \begin{quote} + ``I observed in the kernel code (to my disgust), the Linux + PIP implementation is a nightmare: extremely heavy weight, + involving maintenance of a full wait-for graph, and requiring + updates for a range of events, including priority changes and + interruptions of wait operations.'' + \end{quote} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{A Correctness ``Proof'' in 1990} + \Large + + \begin{itemize} + \item a paper$^\star$ + in 1990 ``proved'' the correctness of an algorithm for PIP\\[5mm] + \end{itemize} + + \normalsize + \begin{quote} + \ldots{}after the thread (whose priority has been raised) completes its + critical section and releases the lock, it ``returns to its original + priority level''. + \end{quote}\bigskip + + \small + $^\star$ in IEEE Transactions on Computers + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{} + \Large + + \begin{center} + \begin{tabular}{l} + \alert{H}igh-priority process 1\\[2mm] + \alert{H}igh-priority process 2\\[8mm] + \alert{L}ow-priority process + \end{tabular} + \end{center} + + \onslide<2->{ + \begin{itemize} + \item Solution: \\Return to highest \alert{remaining} priority + \end{itemize}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Events} + \Large + + \begin{center} + \begin{tabular}{l} + Create \textcolor{gray}{thread priority}\\ + Exit \textcolor{gray}{thread}\\ + Set \textcolor{gray}{thread priority}\\ + Lock \textcolor{gray}{thread cs}\\ + Unlock \textcolor{gray}{thread cs}\\ + \end{tabular} + \end{center}\pause\medskip + + \large + A \alert{state} is a list of events (that happened so far). + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Precedences} + \large + + \begin{center} + \begin{tabular}{l} + @{thm preced_def[where thread="th"]} + \end{tabular} + \end{center} + + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{RAGs} + +\begin{center} + \newcommand{\fnt}{\fontsize{7}{8}\selectfont} + \begin{tikzpicture}[scale=1] + %%\draw[step=2mm] (-3,2) grid (1,-1); + + \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}}; + \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}}; + \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}}; + \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}}; + \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}}; + \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}}; + \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}}; + + \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (B); + \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B); + \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting} (B); + \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding} (E); + \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (E1); + \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (E); + \end{tikzpicture} + \end{center}\bigskip + + \begin{center} + \begin{minipage}{0.8\linewidth} + \raggedleft + @{thm cs_depend_def} + \end{minipage} + \end{center}\pause + + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Good Next Events} + %%\large + + \begin{center} + @{thm[mode=Rule] thread_create[where thread=th]}\bigskip + + @{thm[mode=Rule] thread_exit[where thread=th]}\bigskip + + @{thm[mode=Rule] thread_set[where thread=th]} + \end{center} + + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Good Next Events} + %%\large + + \begin{center} + @{thm[mode=Rule] thread_P[where thread=th]}\bigskip + + @{thm[mode=Rule] thread_V[where thread=th]}\bigskip + \end{center} + + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Theorem} + + \textcolor{gray}{``No indefinite priority inversion''}\bigskip + + Theorem:$^\star$ If th is the thread with the highest precedence in state s, + then in every future state @{text "s'"} in which th is still + alive\smallskip + + + \begin{itemize} + \item th is blocked by a thread @{text "th'"} that was alive in s + \item @{text "th'"} held a resource in s, and + \item @{text "th'"} is running with the precedence of th.\bigskip + \end{itemize} + + \small + $^\star$ modulo some further assumptions\bigskip\pause + + It does not matter which process gets a released lock. + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{Implementation} + + s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip + + \alert{Create th prio}, \alert{Exit th} + + \begin{itemize} + \item @{text "RAG s' = RAG s"} + \item precedences of descendants stay all the same + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{Implementation} + + s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip + + \alert{Set th prio} + + \begin{itemize} + \item @{text "RAG s' = RAG s"} + \item we have to recalculate the precedence of the direct descendants + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{Implementation} + + s $=$ current state; @{text "s'"} $=$ next state\bigskip + + \alert{Unlock th cs} where there is a thread to take over + + \begin{itemize} + \item @{text "RAG s' = RAG s - {(C cs, T th), (T th', C cs)} \ {(C cs, T th')}"} + \item we have to recalculate the precedence of the direct descendants + \end{itemize}\bigskip + + \alert{Unlock th cs} where no thread takes over + + \begin{itemize} + \item @{text "RAG s' = RAG s - {(C cs, T th)}"} + \item no recalculation of precedences + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{Implementation} + + s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip + + \alert{Lock th cs} where cs is not locked + + \begin{itemize} + \item @{text "RAG s' = RAG s \ {(C cs, T th')}"} + \item no recalculation of precedences + \end{itemize}\bigskip + + \alert{Lock th cs} where cs is locked + + \begin{itemize} + \item @{text "RAG s' = RAG s - {(T th, C cs)}"} + \item we have to recalculate the precedence of the descendants + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{PINTOS} + + \begin{itemize} + \item \ldots{}small operating system developed at Stanford for teaching; + written in C\bigskip + \end{itemize} + + \begin{center} + \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|} + \hline + {\bf Event} & {\bf PINTOS function} \\ + \hline + @{text Create} & @{text "thread_create"}\\ + @{text Exit} & @{text "thread_exit"}\\ + @{text Set} & @{text "thread_set_priority"}\\ + @{text Lock} & @{text "lock_acquire"}\\ + @{text Unlock} & @{text "lock_release"}\\ + \hline + \end{tabular} + \end{center} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Conclusion} + + \begin{itemize} + \item surprised how pleasant the experience was\medskip + + \item no real specification existed for PIP\medskip + + \item general technique (a ``hammer''):\\[2mm] + events, separation of good and bad configurations\medskip + + \item scheduler in RT-Linux\medskip + + \item multiprocessor case\medskip + + \item other ``nails'' ? (networks, \ldots) + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +(*<*) +end +(*>*) \ No newline at end of file diff -r 1b9163229f3f -r 66e0ec8acedc prio/Slides/document/beamerthemeplaincu.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/prio/Slides/document/beamerthemeplaincu.sty Thu Jun 28 11:25:26 2012 +0000 @@ -0,0 +1,126 @@ +\ProvidesPackage{beamerthemeplaincu}[2003/11/07 ver 0.93] +\NeedsTeXFormat{LaTeX2e}[1995/12/01] + +% Copyright 2003 by Till Tantau . +% +% This program can be redistributed and/or modified under the terms +% of the LaTeX Project Public License Distributed from CTAN +% archives in directory macros/latex/base/lppl.txt. + +\newcommand{\slidecaption}{} + +\mode + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% comic fonts fonts +\DeclareFontFamily{T1}{comic}{}% +\DeclareFontShape{T1}{comic}{m}{n}{<->s*[.9]comic8t}{}% +\DeclareFontShape{T1}{comic}{m}{it}{<->s*[.9]comic8t}{}% +\DeclareFontShape{T1}{comic}{m}{sc}{<->s*[.9]comic8t}{}% +\DeclareFontShape{T1}{comic}{b}{n}{<->s*[.9]comicbd8t}{}% +\DeclareFontShape{T1}{comic}{b}{it}{<->s*[.9]comicbd8t}{}% +\DeclareFontShape{T1}{comic}{m}{sl}{<->ssub * comic/m/it}{}% +\DeclareFontShape{T1}{comic}{b}{sc}{<->sub * comic/m/sc}{}% +\DeclareFontShape{T1}{comic}{b}{sl}{<->ssub * comic/b/it}{}% +\DeclareFontShape{T1}{comic}{bx}{n}{<->ssub * comic/b/n}{}% +\DeclareFontShape{T1}{comic}{bx}{it}{<->ssub * comic/b/it}{}% +\DeclareFontShape{T1}{comic}{bx}{sc}{<->sub * comic/m/sc}{}% +\DeclareFontShape{T1}{comic}{bx}{sl}{<->ssub * comic/b/it}{}% +% +\renewcommand{\rmdefault}{comic}% +\renewcommand{\sfdefault}{comic}% +\renewcommand{\mathfamilydefault}{cmr}% mathfont should be still the old one +% +\DeclareMathVersion{bold}% mathfont needs to be bold +\DeclareSymbolFont{operators}{OT1}{cmr}{b}{n}% +\SetSymbolFont{operators}{bold}{OT1}{cmr}{b}{n}% +\DeclareSymbolFont{letters}{OML}{cmm}{b}{it}% +\SetSymbolFont{letters}{bold}{OML}{cmm}{b}{it}% +\DeclareSymbolFont{symbols}{OMS}{cmsy}{b}{n}% +\SetSymbolFont{symbols}{bold}{OMS}{cmsy}{b}{n}% +\DeclareSymbolFont{largesymbols}{OMX}{cmex}{b}{n}% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % Title page +%\usetitlepagetemplate{ +% \vbox{} +% \vfill +% \begin{centering} +% \Large\structure{\textrm{\textit{{\inserttitle}}}} +% \vskip1em\par +% \normalsize\insertauthor\vskip1em\par +% {\scriptsize\insertinstitute\par}\par\vskip1em +% \insertdate\par\vskip1.5em +% \inserttitlegraphic +% \end{centering} +% \vfill +% } + + % Part page +%\usepartpagetemplate{ +% \begin{centering} +% \Large\structure{\textrm{\textit{\partname~\@Roman\c@part}}} +% \vskip1em\par +% \textrm{\textit{\insertpart}}\par +% \end{centering} +% } + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Frametitles +\setbeamerfont{frametitle}{size={\huge}} +\setbeamerfont{frametitle}{family={\usefont{T1}{ptm}{b}{n}}} +\setbeamercolor{frametitle}{fg=gray,bg=white} + +\setbeamertemplate{frametitle}{% +\vskip 2mm % distance from the top margin +\hskip -3mm % distance from left margin +\vbox{% +\begin{minipage}{1.05\textwidth}% +\centering% +\insertframetitle% +\end{minipage}}% +} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Foot +% +\setbeamertemplate{navigation symbols}{} +\usefoottemplate{% +\vbox{% + \tinyline{% + \tiny\hfill\textcolor{gray!50}{\slidecaption{} -- + p.~\insertframenumber/\inserttotalframenumber}}}% +} + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\beamertemplateballitem +\setlength\leftmargini{2mm} +\setlength\leftmarginii{0.6cm} +\setlength\leftmarginiii{1.5cm} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% blocks +%\definecolor{cream}{rgb}{1,1,.65} +\definecolor{cream}{rgb}{1,1,.8} +\setbeamerfont{block title}{size=\normalsize} +\setbeamercolor{block title}{fg=black,bg=cream} +\setbeamercolor{block body}{fg=black,bg=cream} + +\setbeamertemplate{blocks}[rounded][shadow=true] + +\setbeamercolor{boxcolor}{fg=black,bg=cream} + +\mode + + + + + + + diff -r 1b9163229f3f -r 66e0ec8acedc prio/Slides/document/mathpartir.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/prio/Slides/document/mathpartir.sty Thu Jun 28 11:25:26 2012 +0000 @@ -0,0 +1,446 @@ +% Mathpartir --- Math Paragraph for Typesetting Inference Rules +% +% Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy +% +% Author : Didier Remy +% Version : 1.2.0 +% Bug Reports : to author +% Web Site : http://pauillac.inria.fr/~remy/latex/ +% +% Mathpartir is free software; you can redistribute it and/or modify +% it under the terms of the GNU General Public License as published by +% the Free Software Foundation; either version 2, or (at your option) +% any later version. +% +% Mathpartir is distributed in the hope that it will be useful, +% but WITHOUT ANY WARRANTY; without even the implied warranty of +% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +% GNU General Public License for more details +% (http://pauillac.inria.fr/~remy/license/GPL). +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% File mathpartir.sty (LaTeX macros) +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{mathpartir} + [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules] + +%% + +%% Identification +%% Preliminary declarations + +\RequirePackage {keyval} + +%% Options +%% More declarations + +%% PART I: Typesetting maths in paragraphe mode + +%% \newdimen \mpr@tmpdim +%% Dimens are a precious ressource. Uses seems to be local. +\let \mpr@tmpdim \@tempdima + +% To ensure hevea \hva compatibility, \hva should expands to nothing +% in mathpar or in inferrule +\let \mpr@hva \empty + +%% normal paragraph parametters, should rather be taken dynamically +\def \mpr@savepar {% + \edef \MathparNormalpar + {\noexpand \lineskiplimit \the\lineskiplimit + \noexpand \lineskip \the\lineskip}% + } + +\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em} +\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em} +\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em} +\let \MathparLineskip \mpr@lineskip +\def \mpr@paroptions {\MathparLineskip} +\let \mpr@prebindings \relax + +\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em + +\def \mpr@goodbreakand + {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip} +\def \mpr@and {\hskip \mpr@andskip} +\def \mpr@andcr {\penalty 50\mpr@and} +\def \mpr@cr {\penalty -10000\mpr@and} +\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10} + +\def \mpr@bindings {% + \let \and \mpr@andcr + \let \par \mpr@andcr + \let \\\mpr@cr + \let \eqno \mpr@eqno + \let \hva \mpr@hva + } +\let \MathparBindings \mpr@bindings + +% \@ifundefined {ignorespacesafterend} +% {\def \ignorespacesafterend {\aftergroup \ignorespaces} + +\newenvironment{mathpar}[1][] + {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering + \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else + \noindent $\displaystyle\fi + \MathparBindings} + {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend} + +\newenvironment{mathparpagebreakable}[1][] + {\begingroup + \par + \mpr@savepar \parskip 0em \hsize \linewidth \centering + \mpr@prebindings \mpr@paroptions #1% + \vskip \abovedisplayskip \vskip -\lineskip% + \ifmmode \else $\displaystyle\fi + \MathparBindings + } + {\unskip + \ifmmode $\fi \par\endgroup + \vskip \belowdisplayskip + \noindent + \ignorespacesafterend} + +% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum +% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi} + +%%% HOV BOXES + +\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip + \vbox \bgroup \tabskip 0em \let \\ \cr + \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup + \egroup} + +\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize + \box0\else \mathvbox {#1}\fi} + + +%% Part II -- operations on lists + +\newtoks \mpr@lista +\newtoks \mpr@listb + +\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter +{#2}\edef #2{\the \mpr@lista \the \mpr@listb}} + +\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter +{#2}\edef #2{\the \mpr@listb\the\mpr@lista}} + +\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb +\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}} + +\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2} +\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}} + +\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2} +\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}} + +\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}% + \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the + \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty + \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop + \mpr@flatten \mpr@all \mpr@to \mpr@one + \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof + \mpr@all \mpr@stripend + \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi + \ifx 1\mpr@isempty + \repeat +} + +\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty + \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp} + +%% Part III -- Type inference rules + +\newif \if@premisse +\newbox \mpr@hlist +\newbox \mpr@vlist +\newif \ifmpr@center \mpr@centertrue +\def \mpr@htovlist {% + \setbox \mpr@hlist + \hbox {\strut + \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi + \unhbox \mpr@hlist}% + \setbox \mpr@vlist + \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist + \else \unvbox \mpr@vlist \box \mpr@hlist + \fi}% +} +% OLD version +% \def \mpr@htovlist {% +% \setbox \mpr@hlist +% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}% +% \setbox \mpr@vlist +% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist +% \else \unvbox \mpr@vlist \box \mpr@hlist +% \fi}% +% } + +\def \mpr@item #1{$\displaystyle #1$} +\def \mpr@sep{2em} +\def \mpr@blank { } +\def \mpr@hovbox #1#2{\hbox + \bgroup + \ifx #1T\@premissetrue + \else \ifx #1B\@premissefalse + \else + \PackageError{mathpartir} + {Premisse orientation should either be T or B} + {Fatal error in Package}% + \fi \fi + \def \@test {#2}\ifx \@test \mpr@blank\else + \setbox \mpr@hlist \hbox {}% + \setbox \mpr@vlist \vbox {}% + \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi + \let \@hvlist \empty \let \@rev \empty + \mpr@tmpdim 0em + \expandafter \mpr@makelist #2\mpr@to \mpr@flat + \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi + \def \\##1{% + \def \@test {##1}\ifx \@test \empty + \mpr@htovlist + \mpr@tmpdim 0em %%% last bug fix not extensively checked + \else + \setbox0 \hbox{\mpr@item {##1}}\relax + \advance \mpr@tmpdim by \wd0 + %\mpr@tmpdim 1.02\mpr@tmpdim + \ifnum \mpr@tmpdim < \hsize + \ifnum \wd\mpr@hlist > 0 + \if@premisse + \setbox \mpr@hlist + \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}% + \else + \setbox \mpr@hlist + \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}% + \fi + \else + \setbox \mpr@hlist \hbox {\unhbox0}% + \fi + \else + \ifnum \wd \mpr@hlist > 0 + \mpr@htovlist + \mpr@tmpdim \wd0 + \fi + \setbox \mpr@hlist \hbox {\unhbox0}% + \fi + \advance \mpr@tmpdim by \mpr@sep + \fi + }% + \@rev + \mpr@htovlist + \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist + \fi + \egroup +} + +%%% INFERENCE RULES + +\@ifundefined{@@over}{% + \let\@@over\over % fallback if amsmath is not loaded + \let\@@overwithdelims\overwithdelims + \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims + \let\@@above\above \let\@@abovewithdelims\abovewithdelims + }{} + +%% The default + +\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em + $\displaystyle {#1\mpr@over #2}$}} +\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em + $\displaystyle {#1\@@atop #2}$}} + +\let \mpr@fraction \mpr@@fraction + +%% A generic solution to arrow + +\def \mpr@make@fraction #1#2#3#4#5{\hbox {% + \def \mpr@tail{#1}% + \def \mpr@body{#2}% + \def \mpr@head{#3}% + \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}% + \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}% + \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}% + \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax + \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax + \setbox0=\hbox {$\box1 \@@atop \box2$}% + \dimen0=\wd0\box0 + \box0 \hskip -\dimen0\relax + \hbox to \dimen0 {$% + \mathrel{\mpr@tail}\joinrel + \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}% + $}}} + +%% Old stuff should be removed in next version +\def \mpr@@nothing #1#2 + {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$} +\def \mpr@@reduce #1#2{\hbox + {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}} +\def \mpr@@rewrite #1#2#3{\hbox + {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}} +\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}} + +\def \mpr@empty {} +\def \mpr@inferrule + {\bgroup + \ifnum \linewidth<\hsize \hsize \linewidth\fi + \mpr@rulelineskip + \let \and \qquad + \let \hva \mpr@hva + \let \@rulename \mpr@empty + \let \@rule@options \mpr@empty + \let \mpr@over \@@over + \mpr@inferrule@} +\newcommand {\mpr@inferrule@}[3][] + {\everymath={\displaystyle}% + \def \@test {#2}\ifx \empty \@test + \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}% + \else + \def \@test {#3}\ifx \empty \@test + \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}% + \else + \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}% + \fi \fi + \def \@test {#1}\ifx \@test\empty \box0 + \else \vbox +%%% Suggestion de Francois pour les etiquettes longues +%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi + {\hbox {\RefTirName {#1}}\box0}\fi + \egroup} + +\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}} + +% They are two forms +% \inferrule [label]{[premisses}{conclusions} +% or +% \inferrule* [options]{[premisses}{conclusions} +% +% Premisses and conclusions are lists of elements separated by \\ +% Each \\ produces a break, attempting horizontal breaks if possible, +% and vertical breaks if needed. +% +% An empty element obtained by \\\\ produces a vertical break in all cases. +% +% The former rule is aligned on the fraction bar. +% The optional label appears on top of the rule +% The second form to be used in a derivation tree is aligned on the last +% line of its conclusion +% +% The second form can be parameterized, using the key=val interface. The +% folloiwng keys are recognized: +% +% width set the width of the rule to val +% narrower set the width of the rule to val\hsize +% before execute val at the beginning/left +% lab put a label [Val] on top of the rule +% lskip add negative skip on the right +% left put a left label [Val] +% Left put a left label [Val], ignoring its width +% right put a right label [Val] +% Right put a right label [Val], ignoring its width +% leftskip skip negative space on the left-hand side +% rightskip skip negative space on the right-hand side +% vdots lift the rule by val and fill vertical space with dots +% after execute val at the end/right +% +% Note that most options must come in this order to avoid strange +% typesetting (in particular leftskip must preceed left and Left and +% rightskip must follow Right or right; vdots must come last +% or be only followed by rightskip. +% + +%% Keys that make sence in all kinds of rules +\def \mprset #1{\setkeys{mprset}{#1}} +\define@key {mprset}{andskip}[]{\mpr@andskip=#1} +\define@key {mprset}{lineskip}[]{\lineskip=#1} +\define@key {mprset}{flushleft}[]{\mpr@centerfalse} +\define@key {mprset}{center}[]{\mpr@centertrue} +\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} +\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction} +\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1} +\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} +\define@key {mprset}{sep}{\def\mpr@sep{#1}} + +\newbox \mpr@right +\define@key {mpr}{flushleft}[]{\mpr@centerfalse} +\define@key {mpr}{center}[]{\mpr@centertrue} +\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} +\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1} +\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} +\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax + \advance \hsize by -\wd0\box0} +\define@key {mpr}{width}{\hsize #1} +\define@key {mpr}{sep}{\def\mpr@sep{#1}} +\define@key {mpr}{before}{#1} +\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}} +\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}} +\define@key {mpr}{narrower}{\hsize #1\hsize} +\define@key {mpr}{leftskip}{\hskip -#1} +\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce} +\define@key {mpr}{rightskip} + {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}} +\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax + \advance \hsize by -\wd0\box0} +\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax + \advance \hsize by -\wd0\box0} +\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}} +\define@key {mpr}{right} + {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0 + \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} +\define@key {mpr}{RIGHT} + {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0 + \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} +\define@key {mpr}{Right} + {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}} +\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}} +\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}} + +\newcommand \mpr@inferstar@ [3][]{\setbox0 + \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax + \setbox \mpr@right \hbox{}% + $\setkeys{mpr}{#1}% + \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else + \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi + \box \mpr@right \mpr@vdots$} + \setbox1 \hbox {\strut} + \@tempdima \dp0 \advance \@tempdima by -\dp1 + \raise \@tempdima \box0} + +\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}} +\newcommand \mpr@err@skipargs[3][]{} +\def \mpr@inferstar*{\ifmmode + \let \@do \mpr@inferstar@ + \else + \let \@do \mpr@err@skipargs + \PackageError {mathpartir} + {\string\inferrule* can only be used in math mode}{}% + \fi \@do} + + +%%% Exports + +% Envirnonment mathpar + +\let \inferrule \mpr@infer + +% make a short name \infer is not already defined +\@ifundefined {infer}{\let \infer \mpr@infer}{} + +\def \TirNameStyle #1{\small \textsc{#1}} +\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}} +\let \TirName \tir@name +\let \DefTirName \TirName +\let \RefTirName \TirName + +%%% Other Exports + +% \let \listcons \mpr@cons +% \let \listsnoc \mpr@snoc +% \let \listhead \mpr@head +% \let \listmake \mpr@makelist + + + + +\endinput diff -r 1b9163229f3f -r 66e0ec8acedc prio/Slides/document/root.beamer.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/prio/Slides/document/root.beamer.tex Thu Jun 28 11:25:26 2012 +0000 @@ -0,0 +1,12 @@ +\documentclass[14pt,t]{beamer} +%%%\usepackage{pstricks} + +\input{root.tex} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% TeX-command-default: "Slides" +%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f")) +%%% End: + diff -r 1b9163229f3f -r 66e0ec8acedc prio/Slides/document/root.notes.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/prio/Slides/document/root.notes.tex Thu Jun 28 11:25:26 2012 +0000 @@ -0,0 +1,18 @@ +\documentclass[11pt]{article} +%%\usepackage{pstricks} +\usepackage{dina4} +\usepackage{beamerarticle} +\usepackage{times} +\usepackage{hyperref} +\usepackage{pgf} +\usepackage{amssymb} +\setjobnamebeamerversion{root.beamer} +\input{root.tex} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% TeX-command-default: "Slides" +%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f")) +%%% End: + diff -r 1b9163229f3f -r 66e0ec8acedc prio/Slides/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/prio/Slides/document/root.tex Thu Jun 28 11:25:26 2012 +0000 @@ -0,0 +1,147 @@ +\usepackage{beamerthemeplaincu} +%%\usepackage{ulem} +\usepackage[T1]{fontenc} +\usepackage{proof} +\usepackage[latin1]{inputenc} +\usepackage{isabelle} +\usepackage{isabellesym} +\usepackage{mathpartir} +\usepackage[absolute, overlay]{textpos} +\usepackage{proof} +\usepackage{ifthen} +\usepackage{animate} +\usepackage{tikz} +\usepackage{pgf} +\usetikzlibrary{arrows} +\usetikzlibrary{automata} +\usetikzlibrary{shapes} +\usetikzlibrary{shadows} +\usetikzlibrary{calc} + +% Isabelle configuration +%%\urlstyle{rm} +\isabellestyle{rm} +\renewcommand{\isastyle}{\rm}% +\renewcommand{\isastyleminor}{\rm}% +\renewcommand{\isastylescript}{\footnotesize\rm\slshape}% +\renewcommand{\isatagproof}{} +\renewcommand{\endisatagproof}{} +\renewcommand{\isamarkupcmt}[1]{#1} + +% Isabelle characters +\renewcommand{\isacharunderscore}{\_} +\renewcommand{\isacharbar}{\isamath{\mid}} +\renewcommand{\isasymiota}{} +\renewcommand{\isacharbraceleft}{\{} +\renewcommand{\isacharbraceright}{\}} +\renewcommand{\isacharless}{$\langle$} +\renewcommand{\isachargreater}{$\rangle$} +\renewcommand{\isasymsharp}{\isamath{\#}} +\renewcommand{\isasymdots}{\isamath{...}} +\renewcommand{\isasymbullet}{\act} + +% mathpatir +\mprset{sep=1em} + +% general math stuff +\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions +\newcommand{\dnn}{\stackrel{\mbox{\Large def}}{=}} +\renewcommand{\isasymequiv}{$\dn$} +\renewcommand{\emptyset}{\varnothing}% nice round empty set +\renewcommand{\Gamma}{\varGamma} +\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}} +\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}} +\newcommand{\smath}[1]{\textcolor{blue}{\ensuremath{#1}}} +\newcommand{\fresh}{\mathrel{\#}} +\newcommand{\act}{{\raisebox{-0.5mm}{\Large$\boldsymbol{\cdot}$}}}% swapping action +\newcommand{\swap}[2]{(#1\,#2)}% swapping operation + +% beamer stuff +\renewcommand{\slidecaption}{Salvador, 26.~August 2008} + + +% colours for Isar Code (in article mode everything is black and white) +\mode{ +\definecolor{isacol:brown}{rgb}{.823,.411,.117} +\definecolor{isacol:lightblue}{rgb}{.274,.509,.705} +\definecolor{isacol:green}{rgb}{0,.51,0.14} +\definecolor{isacol:red}{rgb}{.803,0,0} +\definecolor{isacol:blue}{rgb}{0,0,.803} +\definecolor{isacol:darkred}{rgb}{.545,0,0} +\definecolor{isacol:black}{rgb}{0,0,0}} +\mode
{ +\definecolor{isacol:brown}{rgb}{0,0,0} +\definecolor{isacol:lightblue}{rgb}{0,0,0} +\definecolor{isacol:green}{rgb}{0,0,0} +\definecolor{isacol:red}{rgb}{0,0,0} +\definecolor{isacol:blue}{rgb}{0,0,0} +\definecolor{isacol:darkred}{rgb}{0,0,0} +\definecolor{isacol:black}{rgb}{0,0,0} +} + + +\newcommand{\strong}[1]{{\bfseries {#1}}} +\newcommand{\bluecmd}[1]{{\color{isacol:lightblue}{\strong{#1}}}} +\newcommand{\browncmd}[1]{{\color{isacol:brown}{\strong{#1}}}} +\newcommand{\redcmd}[1]{{\color{isacol:red}{\strong{#1}}}} + +\renewcommand{\isakeyword}[1]{% +\ifthenelse{\equal{#1}{show}}{\browncmd{#1}}{% +\ifthenelse{\equal{#1}{case}}{\browncmd{#1}}{% +\ifthenelse{\equal{#1}{assume}}{\browncmd{#1}}{% +\ifthenelse{\equal{#1}{obtain}}{\browncmd{#1}}{% +\ifthenelse{\equal{#1}{fix}}{\browncmd{#1}}{% +\ifthenelse{\equal{#1}{oops}}{\redcmd{#1}}{% +\ifthenelse{\equal{#1}{thm}}{\redcmd{#1}}{% +{\bluecmd{#1}}}}}}}}}}% + +% inner syntax colour +\chardef\isachardoublequoteopen=`\"% +\chardef\isachardoublequoteclose=`\"% +\chardef\isacharbackquoteopen=`\`% +\chardef\isacharbackquoteclose=`\`% +\newenvironment{innersingle}% +{\isacharbackquoteopen\color{isacol:green}}% +{\color{isacol:black}\isacharbackquoteclose} +\newenvironment{innerdouble}% +{\isachardoublequoteopen\color{isacol:green}}% +{\color{isacol:black}\isachardoublequoteclose} + +%% misc +\newcommand{\gb}[1]{\textcolor{isacol:green}{#1}} +\newcommand{\rb}[1]{\textcolor{red}{#1}} + +%% animations +\newcounter{growcnt} +\newcommand{\grow}[2] +{\begin{tikzpicture}[baseline=(n.base)]% + \node[scale=(0.1 *#1 + 0.001),inner sep=0pt] (n) {#2}; + \end{tikzpicture}% +} + +%% isatabbing +%\renewcommand{\isamarkupcmt}[1]% +%{\ifthenelse{\equal{TABSET}{#1}}{\=}% +% {\ifthenelse{\equal{TAB}{#1}}{\>}% +% {\ifthenelse{\equal{NEWLINE}{#1}}{\\}% +% {\ifthenelse{\equal{DOTS}{#1}}{\ldots}{\isastylecmt--- {#1}}}% +% }% +% }% +%}% + + +\newenvironment{isatabbing}% +{\renewcommand{\isanewline}{\\}\begin{tabbing}}% +{\end{tabbing}} + +\begin{document} +\input{session} +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% TeX-command-default: "Slides" +%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f")) +%%% End: + diff -r 1b9163229f3f -r 66e0ec8acedc prio/Slides/slides.pdf Binary file prio/Slides/slides.pdf has changed diff -r 1b9163229f3f -r 66e0ec8acedc prio/document/beamerthemeplaincu.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/prio/document/beamerthemeplaincu.sty Thu Jun 28 11:25:26 2012 +0000 @@ -0,0 +1,126 @@ +\ProvidesPackage{beamerthemeplaincu}[2003/11/07 ver 0.93] +\NeedsTeXFormat{LaTeX2e}[1995/12/01] + +% Copyright 2003 by Till Tantau . +% +% This program can be redistributed and/or modified under the terms +% of the LaTeX Project Public License Distributed from CTAN +% archives in directory macros/latex/base/lppl.txt. + +\newcommand{\slidecaption}{} + +\mode + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% comic fonts fonts +\DeclareFontFamily{T1}{comic}{}% +\DeclareFontShape{T1}{comic}{m}{n}{<->s*[.9]comic8t}{}% +\DeclareFontShape{T1}{comic}{m}{it}{<->s*[.9]comic8t}{}% +\DeclareFontShape{T1}{comic}{m}{sc}{<->s*[.9]comic8t}{}% +\DeclareFontShape{T1}{comic}{b}{n}{<->s*[.9]comicbd8t}{}% +\DeclareFontShape{T1}{comic}{b}{it}{<->s*[.9]comicbd8t}{}% +\DeclareFontShape{T1}{comic}{m}{sl}{<->ssub * comic/m/it}{}% +\DeclareFontShape{T1}{comic}{b}{sc}{<->sub * comic/m/sc}{}% +\DeclareFontShape{T1}{comic}{b}{sl}{<->ssub * comic/b/it}{}% +\DeclareFontShape{T1}{comic}{bx}{n}{<->ssub * comic/b/n}{}% +\DeclareFontShape{T1}{comic}{bx}{it}{<->ssub * comic/b/it}{}% +\DeclareFontShape{T1}{comic}{bx}{sc}{<->sub * comic/m/sc}{}% +\DeclareFontShape{T1}{comic}{bx}{sl}{<->ssub * comic/b/it}{}% +% +\renewcommand{\rmdefault}{comic}% +\renewcommand{\sfdefault}{comic}% +\renewcommand{\mathfamilydefault}{cmr}% mathfont should be still the old one +% +\DeclareMathVersion{bold}% mathfont needs to be bold +\DeclareSymbolFont{operators}{OT1}{cmr}{b}{n}% +\SetSymbolFont{operators}{bold}{OT1}{cmr}{b}{n}% +\DeclareSymbolFont{letters}{OML}{cmm}{b}{it}% +\SetSymbolFont{letters}{bold}{OML}{cmm}{b}{it}% +\DeclareSymbolFont{symbols}{OMS}{cmsy}{b}{n}% +\SetSymbolFont{symbols}{bold}{OMS}{cmsy}{b}{n}% +\DeclareSymbolFont{largesymbols}{OMX}{cmex}{b}{n}% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % Title page +%\usetitlepagetemplate{ +% \vbox{} +% \vfill +% \begin{centering} +% \Large\structure{\textrm{\textit{{\inserttitle}}}} +% \vskip1em\par +% \normalsize\insertauthor\vskip1em\par +% {\scriptsize\insertinstitute\par}\par\vskip1em +% \insertdate\par\vskip1.5em +% \inserttitlegraphic +% \end{centering} +% \vfill +% } + + % Part page +%\usepartpagetemplate{ +% \begin{centering} +% \Large\structure{\textrm{\textit{\partname~\@Roman\c@part}}} +% \vskip1em\par +% \textrm{\textit{\insertpart}}\par +% \end{centering} +% } + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Frametitles +\setbeamerfont{frametitle}{size={\huge}} +\setbeamerfont{frametitle}{family={\usefont{T1}{ptm}{b}{n}}} +\setbeamercolor{frametitle}{fg=gray,bg=white} + +\setbeamertemplate{frametitle}{% +\vskip 2mm % distance from the top margin +\hskip -3mm % distance from left margin +\vbox{% +\begin{minipage}{1.05\textwidth}% +\centering% +\insertframetitle% +\end{minipage}}% +} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Foot +% +\setbeamertemplate{navigation symbols}{} +\usefoottemplate{% +\vbox{% + \tinyline{% + \tiny\hfill\textcolor{gray!50}{\slidecaption{} -- + p.~\insertframenumber/\inserttotalframenumber}}}% +} + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\beamertemplateballitem +\setlength\leftmargini{2mm} +\setlength\leftmarginii{0.6cm} +\setlength\leftmarginiii{1.5cm} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% blocks +%\definecolor{cream}{rgb}{1,1,.65} +\definecolor{cream}{rgb}{1,1,.8} +\setbeamerfont{block title}{size=\normalsize} +\setbeamercolor{block title}{fg=black,bg=cream} +\setbeamercolor{block body}{fg=black,bg=cream} + +\setbeamertemplate{blocks}[rounded][shadow=true] + +\setbeamercolor{boxcolor}{fg=black,bg=cream} + +\mode + + + + + + + diff -r 1b9163229f3f -r 66e0ec8acedc prio/paper.pdf Binary file prio/paper.pdf has changed