1.1 --- a/doc-src/isac/msteger/bakk-presentation.tex Thu Jun 16 15:09:47 2011 +0200
1.2 +++ b/doc-src/isac/msteger/bakk-presentation.tex Thu Jun 16 18:51:59 2011 +0200
1.3 @@ -57,7 +57,8 @@
1.4 % You might wish to add the option [pausesections]
1.5 \end{frame}
1.6
1.7 -\section[Isabelle]{Einleitung: Der Theoremprover Isabelle}
1.8 +\section[Stutus quo]{Ausgangssituation: das k\"unftige Isabelle Front-end}
1.9 +\subsection[Isabelle]{Der Theoremprover Isabelle}
1.10 \begin{frame}
1.11 \frametitle{Der Theoremprover Isabelle}
1.12 \begin{itemize}
1.13 @@ -94,16 +95,15 @@
1.14 \end{itemize}
1.15 \end{frame}
1.16
1.17 -\section[Stutus quo]{Ausgangssituation: das k\"unftige Isabelle Front-end}
1.18 \subsection[Scala-Layer]{Die Konzeption des Scala-Layers}
1.19 \begin{frame}\frametitle{Die Konzeption des Scala-Layers}
1.20 -%\begin{figure}
1.21 -%\begin{center}
1.22 -%\includegraphics[width=75mm]{fig/archi/fig-reuse-ml-scala-SD}
1.23 -%\end{center}
1.24 -%%\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.}
1.25 -%\label{fig-reuse-ml-scala}
1.26 -%\end{figure}
1.27 +\begin{figure}
1.28 +\begin{center}
1.29 +\includegraphics[width=100mm]{fig-reuse-ml-scala-SD}
1.30 +\end{center}
1.31 +%\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.}
1.32 +\label{fig-reuse-ml-scala}
1.33 +\end{figure}
1.34 \end{frame}
1.35
1.36 \begin{frame}\frametitle{Kommunikationsprotokoll \\Scala --- SML}
1.37 @@ -260,8 +260,28 @@
1.38 \end{itemize}
1.39 \end{frame}
1.40
1.41 -\section[Projektarbeit]{Projektarbeit: Vorbereitungen f\"ur ``structured derivations''}
1.42 -\subsection[Beispiel SD]{Beispiel ``structured derivation'' (SD)}
1.43 +\section[Projektarbeit]{Projekt: Vorarbeiten f\"ur ``structured derivations'' (SD)}
1.44 +\subsection[Aufgabenstellung]{Definition der Aufgabenstellung}
1.45 +\begin{frame}\frametitle{Definition der Aufgabenstellung}
1.46 +Aufgabenstellung: \\Feasibility-Study zur Implementierung von ``structured derivations'' in Isabelle.\\
1.47 +
1.48 +\textit{``Die Implementierung soweit vorantreiben wie im gegebenen Studenausma\3 m\"oglich~!''}\\
1.49 +
1.50 +Milestones:
1.51 +\begin{enumerate}
1.52 +\item Relevante Isabelle Komponenten identifizieren und studieren
1.53 +\item Installation der Standard-Komponenten
1.54 +\item Entwicklungsumgebung vom Isabelle-Team kopieren
1.55 +\item Relevante Komponenten implementieren
1.56 + \begin{itemize}
1.57 + \item jEdit Plugin f\"ur SD
1.58 + \item zugeh\"origen Parser
1.59 + \item nicht vorgesehen: SD-Interpreter in Isar (SML)
1.60 + \end{itemize}
1.61 +\end{enumerate}
1.62 +\end{frame}
1.63 +
1.64 +%\subsection[Beispiel SD]{Beispiel ``structured derivation'' (SD)}
1.65 \begin{frame}\frametitle{Beispiel ``structured~derivation''~(SD)}
1.66 {\footnotesize
1.67 \begin{tabbing}
1.68 @@ -285,42 +305,63 @@
1.69 }
1.70 \end{frame}
1.71
1.72 -\subsection[NetBeans]{Aufsetzen des Projektes in der NetBeans IDE}
1.73 -\begin{frame}\frametitle{Grundlegender Aufbau eines jEdit-Plugin}
1.74 +\subsection[NetBeans]{Konfiguration des Projektes in der NetBeans IDE}
1.75 +\begin{frame}\frametitle{Konfiguration in NetBeans}
1.76 +Mehrere Run-Konfigurationen sind praktisch:
1.77 \begin{itemize}
1.78 -\item Ein Plugin besteht aus:
1.79 +\item Start von jEdit + Plug-ins aus NetBeans
1.80 + \begin{itemize}
1.81 + \item Exekution der fertig kompilierten jEdit.jar
1.82 + \item Exkution der eingebundenen jEdit Sources: \\zum Debuggen !
1.83 + \end{itemize}
1.84 +\item Start von jEdit aus der Konsole
1.85 +\end{itemize}
1.86 +\vspace{0.2cm} \pause
1.87 +Dementsprechend komplex sind die Konfigurations-Files:
1.88 +\begin{center}
1.89 +\begin{tabular}{l r l}
1.90 +build.xml & 102 & LOCs\\
1.91 +project.xml & 25 & LOCs\\
1.92 +project.properties & 85 & LOCs\\
1.93 +build-impl.xml & 708 & LOCs\\
1.94 + & & (teilw. automatisch generiert)\end{tabular}
1.95 +\end{center}
1.96 +\end{frame}
1.97 +
1.98 +\subsection[Implementation]{Komponenten zur Implementation von SD}
1.99 +
1.100 +\begin{frame}\frametitle{Die Konzeption des Scala-Layers}
1.101 +\begin{figure}
1.102 +\includegraphics[width=100mm]{fig-jedit-plugins-SD}
1.103 +\label{Frontend des jEdit}
1.104 +\end{figure}
1.105 +\end{frame}
1.106 +
1.107 +\begin{frame}\frametitle{jEdit-Plugin}
1.108 +\begin{itemize}
1.109 +\item Aufbau: Ein Plugin besteht aus:
1.110 \pause
1.111 \begin{itemize}
1.112 \item Source-Files: \textbf{Scala}
1.113 \pause
1.114 \item Property file
1.115 \pause
1.116 - \item XML-Files: \textit{Klebstoff} zwischen \textbf{Java} (Editor) und \textbf{Scala} (Plugin)
1.117 + \item XML-Files: \textit{``glue code''} zwischen \textbf{Java} (Editor) und \textbf{Scala} (Plugin)
1.118 \end{itemize}
1.119 -\pause
1.120 -\item Bestehendes Java-Plugin in Scala transferieren
1.121 -\pause
1.122 -\item Neue Ordnerstruktur in bestehende Isabelle-Ordner-Hierachie integrieren
1.123 +%\pause
1.124 +%\item Bestehendes Java-Plugin in Scala transferieren
1.125 +%\pause
1.126 +%\item Neue Ordnerstruktur in bestehende Isabelle-Ordner-Hierachie integrieren
1.127 \end{itemize}
1.128 \end{frame}
1.129
1.130 -\begin{frame}\frametitle{Die Konzeption des Scala-Layers}
1.131 -\begin{figure}
1.132 -\begin{center}
1.133 -\includegraphics[width=75mm]{fig/block-frontend}
1.134 -\end{center}
1.135 -%\nocaptionrule\caption{Reuse of Isabelle/Isar's Scala API.}
1.136 -\label{Frontend des jEdit}
1.137 -\end{figure}
1.138 -\end{frame}
1.139 -
1.140 \begin{frame}\frametitle{Anforderungen an das Versuchs-Plugin}
1.141 Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt:
1.142 \pause
1.143 \begin{itemize}
1.144 \item Grunds\"atzlicher Aufbau eines GUIs
1.145 \pause
1.146 - \item Kopieren von Text zwischen den einzelnen Buffern
1.147 + \item Kopieren von Text zwischen den einzelnen Buffers
1.148 \pause
1.149 \begin{itemize}
1.150 \item \alert{Somit auch Zugriff auf andere Plugins!}
1.151 @@ -336,15 +377,53 @@
1.152 \end{itemize}
1.153 \end{frame}
1.154
1.155 -\subsection[Implementation]{Komponenten zur von SD}
1.156 +
1.157 \subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)}
1.158
1.159 \section[Summary]{Zusammenfassung}
1.160 \begin{frame}\frametitle{Zusammenfassung}
1.161 - Zusammenfassung TODO
1.162 +Folgende Milestones wurden erfolgreich abgeschlossen:
1.163 +\begin{enumerate}
1.164 +\item Relevante Isabelle Komponenten dokumentiert (...Std.)
1.165 +\item Installation der Standard-Komponenten:
1.166 + \begin{itemize}
1.167 + \item Mercurial Versioncontrol
1.168 + \item NetBeans IDE
1.169 + \item Standard Isabelle Bundle
1.170 + \end{itemize}
1.171 +\item Entwicklungsumgebung vom Isabelle-Team kopieren
1.172 + \begin{itemize}
1.173 + \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML)
1.174 + \item jEdit als NetBeans Projekt definiert
1.175 + \end{itemize}
1.176 +\item Relevante Komponenten implementieren
1.177 + \begin{itemize}
1.178 + \item jEdit Plugin f\"ur SD
1.179 + \item Verbindung des Plugins zu Isabelle
1.180 + \item zugeh\"origen Parser: nur ein Test in SML
1.181 + \end{itemize}
1.182 +\end{enumerate}
1.183 +\end{frame}
1.184 +
1.185 +\begin{frame}\frametitle{Zusammenfassung}
1.186 +\pause
1.187 +\alert{$\mathbf{- - -}$}\\
1.188 +Aus Zeitgr\"unden nicht m\"oglich: ein komplettes SD-Plugin;\\
1.189 +dazu w\"are auch ein Interpreter auf der ML-Seite n\"otig.\\
1.190 +\vspace{0.3cm}
1.191 +\alert{$\mathbf{+ + +}$}\\
1.192 +Voraussetzungen f\"ur k\"unftige Entwicklung geschaffen:
1.193 +\begin{enumerate}
1.194 +\item f\"ur die Implementation von ``structured derivations'' in Isabelle \dots
1.195 +\item \dots als Vorarbeit f\"ur jEdit als k\"unftiges \isac-Frontend
1.196 +\item f\"ur Mitarbeit an k\"unftiger Integration von Isabelle in Entwicklungswerkzeuge (Testcase-Generation etc).
1.197 +\end{enumerate}
1.198 \end{frame}
1.199
1.200 \begin{frame}\frametitle{}
1.201 +\begin{center}
1.202 +\LARGE{Danke f\"ur die Aufmerksamkeit !}
1.203 +\end{center}
1.204 \end{frame}
1.205
1.206 \end{document}