133 \label{fig-reuse-ml-scala} |
133 \label{fig-reuse-ml-scala} |
134 \end{figure} |
134 \end{figure} |
135 |
135 |
136 Der Scala-Layer verbindet die Java Virtual Maschine (JVM) und den in Standart-ML (SML) geschriebenen Isabelle-Kern. Dabei wird ein internes Protokoll verwendet, dass den Datenaustausch zwischen jEdit und Isabelle/Isar erm\"oglicht. Dieses Protokoll ist im Moment noch (bewusst) ohne API ausgef\"uhrt. Aus diesem Grund musste eine Schnittstelle definiert werden, um den Datenaustausch des SD-Plugins (JVM) mit dem SD-Interpreter m\"oglich zu machen. Siehe dazu den Absatz "Verbindung zum Isabelle-Pure Plugin herstellen". Man kann aus diesem Umstand ableiten, dass die Isabelle-Entwickler mit diesem eingezogenen Scala-Layer und dem damit verbundenen internen Protokoll, auf eine konsistente Verwaltung der Theorie-Bibliotheken abzielen. Mit anderen Worten wird dem Anwendungsprogrammierer der direkte Zugriff auf die Isabelle/Isar-Komponente verwehrt. Der Anwender sollten hier also nicht angreifen sonder die Isabelle-Theorien entsprechend erweitern. |
136 Der Scala-Layer verbindet die Java Virtual Maschine (JVM) und den in Standart-ML (SML) geschriebenen Isabelle-Kern. Dabei wird ein internes Protokoll verwendet, dass den Datenaustausch zwischen jEdit und Isabelle/Isar erm\"oglicht. Dieses Protokoll ist im Moment noch (bewusst) ohne API ausgef\"uhrt. Aus diesem Grund musste eine Schnittstelle definiert werden, um den Datenaustausch des SD-Plugins (JVM) mit dem SD-Interpreter m\"oglich zu machen. Siehe dazu den Absatz "Verbindung zum Isabelle-Pure Plugin herstellen". Man kann aus diesem Umstand ableiten, dass die Isabelle-Entwickler mit diesem eingezogenen Scala-Layer und dem damit verbundenen internen Protokoll, auf eine konsistente Verwaltung der Theorie-Bibliotheken abzielen. Mit anderen Worten wird dem Anwendungsprogrammierer der direkte Zugriff auf die Isabelle/Isar-Komponente verwehrt. Der Anwender sollten hier also nicht angreifen sonder die Isabelle-Theorien entsprechend erweitern. |
137 |
137 |
138 \chapter{Aufbau des SD-Plugins} |
138 \chapter{Konfiguration und Implementation der Komponenten} |
139 Dieses Kapitel soll nun anhand der bereits gewonnen Erkenntnise illustrieren, wie die wichtigsten Schritte zum SD-Plugin f\"{u}r jEdit wahrscheinlich aussehen werden. |
139 Dieses Kapitel soll nun anhand der bereits gewonnen Erkenntnise illustrieren, wie die Entwicklungsumgebung vom Isabelle-Team kopiert wurde und wie wichtigsten Schritte zum SD-Plugin f\"{u}r jEdit wahrscheinlich aussehen werden. Wobei einige Schritte parallel und dadurch nat\"{u}rlich sehr gut im Team umgesetzt werden k\"{o}nnen. Eine genaue Aufstellung aller beteiligten Files k\"onnen dem Anhang D entnommen werden. |
140 Wobei einige Schritte parallel und dadurch nat\"{u}rlich sehr gut im Team umgesetzt werden k\"{o}nnen. |
140 |
141 Eine genaue Aufstellung aller beteiligten Files k\"onnen dem Anhang D entnommen werden. |
141 \section{Konfiguration des Netbeans Projektes} |
142 |
142 Um in k\"unftigen Entwicklungsvorhaben effizient kooperieren zu k\"onnen, wurde das Netbeans-Projekt genau nach den Vorgaben des Isabelle-Teams konfiguriert. |
143 \section{Erstellen des Plugin-Ger\"{u}sts} |
143 |
|
144 TODO |
|
145 |
|
146 |
|
147 \section{Implementation der jEdit Komponenten} |
|
148 |
|
149 \subsection{Erstellen des Plugin-Ger\"{u}sts} |
144 Hier gilt es, erstmal den Umfang der gew\"{u}nschten Anforderungen an das Plugin so genau wie m\"{o}glich zu identifizieren. Hat man eine sehr genaue Vorstellung, wie das GUI des Plugins aussehen wird und welche Zusatz-Features angeboten werden sollen so kann man gezielt unter den bereits bestehenden Plugins f\"{u}r jEdit nach n\"{u}tzlichen Plugins suchen, die in das SD-Plugin (m\"{o}glicherweise durch kleine Modifikationen) integriert werden k\"{o}nnen. Dies spart einerseits sehr viel Zeit und ist nebenbei genau die Art von Programmierung, die durch die offnene Plugin-Struktur von jEdit gef\"{o}rdert wird. |
150 Hier gilt es, erstmal den Umfang der gew\"{u}nschten Anforderungen an das Plugin so genau wie m\"{o}glich zu identifizieren. Hat man eine sehr genaue Vorstellung, wie das GUI des Plugins aussehen wird und welche Zusatz-Features angeboten werden sollen so kann man gezielt unter den bereits bestehenden Plugins f\"{u}r jEdit nach n\"{u}tzlichen Plugins suchen, die in das SD-Plugin (m\"{o}glicherweise durch kleine Modifikationen) integriert werden k\"{o}nnen. Dies spart einerseits sehr viel Zeit und ist nebenbei genau die Art von Programmierung, die durch die offnene Plugin-Struktur von jEdit gef\"{o}rdert wird. |
145 |
151 |
146 Hat man nun die Planung abgeschlossen und m\"{o}glicherweise n\"{u}tzliche Plugins gefunden, kann mit der Programmierung des GUIs begonnen werden. Man sollte hier beachten, dass man von Beginn an festlegt, ob mit Scala- oder Java-Swing Komponenten gearbeitet werden soll. Es ist zwar m\"{o}glich, beide Formen zu mischen, doch aus Klarheitsgr\"{u}nden sollte man sich doch f\"{u}r eine Art entscheiden. Wobei hier die Empfehlung im Moment eher noch Richtung Java-Swing geht, da man hier eigentlich f\"{u}r jede Art von Problem bzw. Aufgabe bereits HowTo's im Web finden kann. Da bei Scala-Swing nur Wrapper auf die Java-Swing-Libraries gesetzt wurden, entsteht dadurch auch keinerlei Performance-Verlust. |
152 Hat man nun die Planung abgeschlossen und m\"{o}glicherweise n\"{u}tzliche Plugins gefunden, kann mit der Programmierung des GUIs begonnen werden. Man sollte hier beachten, dass man von Beginn an festlegt, ob mit Scala- oder Java-Swing Komponenten gearbeitet werden soll. Es ist zwar m\"{o}glich, beide Formen zu mischen, doch aus Klarheitsgr\"{u}nden sollte man sich doch f\"{u}r eine Art entscheiden. Wobei hier die Empfehlung im Moment eher noch Richtung Java-Swing geht, da man hier eigentlich f\"{u}r jede Art von Problem bzw. Aufgabe bereits HowTo's im Web finden kann. Da bei Scala-Swing nur Wrapper auf die Java-Swing-Libraries gesetzt wurden, entsteht dadurch auch keinerlei Performance-Verlust. |
147 |
153 |
148 Es existiert bereits ein beispielhaftes Plugin am \sisac-Repository. Da der grunds\"{a}tzliche Aufbau eines jEdit-Plugins soweit umgesetzt wurde und bereits lauff\"{a}hig ist, sollte man dieses wohl als Ausgangspunkt verwenden. Die direkte Verwendung eines Isabelle-Klons ist wohl zu Beginn nicht zu empfehlen bzw. sollte meiner Meinung nach die Integration von Isac in Isabelle bzw. die Verwachsung der beiden Plugins das Fernziel sein und dadurch w\"{u}rde der Klon-Vorgang wohl eher Probleme schaffen als sie zu l\"{o}sen. |
154 Es existiert bereits ein beispielhaftes Plugin am \sisac-Repository. Da der grunds\"{a}tzliche Aufbau eines jEdit-Plugins soweit umgesetzt wurde und bereits lauff\"{a}hig ist, sollte man dieses wohl als Ausgangspunkt verwenden. Die direkte Verwendung eines Isabelle-Klons ist wohl zu Beginn nicht zu empfehlen bzw. sollte meiner Meinung nach die Integration von Isac in Isabelle bzw. die Verwachsung der beiden Plugins das Fernziel sein und dadurch w\"{u}rde der Klon-Vorgang wohl eher Probleme schaffen als sie zu l\"{o}sen. |
149 |
155 |
150 \section{Erzeugung des Plugins} |
156 \subsection{Erzeugung des Plugins} |
151 Hat man die Planung des Plugin-Ger\"{u}sts abgeschlossen und die eigentliche Implementationsphase begonnen, kann dieses Plugin getestet bzw. erzeugt und via jEdit ausgef\"{u}hrt werden. Dazu muss zuerst das jar-File erzeugt und danach in den jEdit-Pluginsordner verschoben werden. Die Erzeugung kann nat\"{u}rlich direkt mittels NetBeans durchgef\"{u}hrt werden. Doch es ist auch m\"{o}glich dies via Kommandline durchzuf\"{u}hren. Folgende Schritte illustrieren wie die Erzeugung und der Kopiervorgang des Plugins durchgef\"{u}hrt werden k\"{o}nnen(Ausschnitt aus dem Skript isac\_jedit): |
157 Hat man die Planung des Plugin-Ger\"{u}sts abgeschlossen und die eigentliche Implementationsphase begonnen, kann dieses Plugin getestet bzw. erzeugt und via jEdit ausgef\"{u}hrt werden. Dazu muss zuerst das jar-File erzeugt und danach in den jEdit-Pluginsordner verschoben werden. Die Erzeugung kann nat\"{u}rlich direkt mittels NetBeans durchgef\"{u}hrt werden. Doch es ist auch m\"{o}glich dies via Kommandline durchzuf\"{u}hren. Folgende Schritte illustrieren wie die Erzeugung und der Kopiervorgang des Plugins durchgef\"{u}hrt werden k\"{o}nnen(Ausschnitt aus dem Skript isac\_jedit): |
152 \begin{enumerate} |
158 \begin{enumerate} |
153 \item Das Plugin kann mittels Kommandline folgenderma{\ss}en erstellt werden: \\ \textit{cd ISABELLE\_HOME/src/Tools/isac/jEdit} $\rightarrow$ \textit{ant jar} |
159 \item Das Plugin kann mittels Kommandline folgenderma{\ss}en erstellt werden: \\ \textit{cd ISABELLE\_HOME/src/Tools/isac/jEdit} $\rightarrow$ \textit{ant jar} |
154 \item Nun kann das das neue Plugin ganz einfach kopiert werden \textit{cp contrib/jEdit/build/ // jars/Isac.jar ../../../../contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/} |
160 \item Nun kann das das neue Plugin ganz einfach kopiert werden \textit{cp contrib/jEdit/build/ // jars/Isac.jar ../../../../contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/} |
155 \item jEdit ausf\"{u}hren und testen |
161 \item jEdit ausf\"{u}hren und testen |
156 \end{enumerate} |
162 \end{enumerate} |
157 |
163 |
158 \section{Verbindung zum Isabelle-Pure Plugin herstellen} |
164 \subsection{Verbindung zum Isabelle-Pure Plugin herstellen} |
159 Der n\"{a}chste Schritt sieht nun die Versorgung des GUIs mit Daten vor. Da das jEdit-Plugin selbst nicht rechnen/interpretieren kann, m\"{u}ssen Daten an den Isabelle-Kern, also das Isabelle-Pure-Plugin weitergegeben werden. Dort k\"{o}nnen die Daten verwertet und aufbereitet zur\"{u}ck an das Frontend gereicht werden. |
165 Der n\"{a}chste Schritt sieht nun die Versorgung des GUIs mit Daten vor. Da das jEdit-Plugin selbst nicht rechnen/interpretieren kann, m\"{u}ssen Daten an den Isabelle-Kern, also das Isabelle-Pure-Plugin weitergegeben werden. Dort k\"{o}nnen die Daten verwertet und aufbereitet zur\"{u}ck an das Frontend gereicht werden. |
160 |
166 |
161 \begin{figure} |
167 \begin{figure} |
162 \begin{center} |
168 \begin{center} |
163 \includegraphics[width=180mm]{../fig-jedit-plugins-SD} |
169 \includegraphics[width=180mm]{../fig-jedit-plugins-SD} |
188 Die obigen Schritte sind n\"{o}tig, um das vorl\"{a}ufige Plugin SD umzusetzen. Nat\"{u}rlich beginnt danach die spannende Arbeit erst so richtig. Ist erst mal ein funktionierender SD-Parser vorhanden, kann dieser immer weiter verbessert und verfeinert werden, bis man auch damit beginnen kann, ihn f\"{u}r das \sisac-Projekt zu nutzen. |
194 Die obigen Schritte sind n\"{o}tig, um das vorl\"{a}ufige Plugin SD umzusetzen. Nat\"{u}rlich beginnt danach die spannende Arbeit erst so richtig. Ist erst mal ein funktionierender SD-Parser vorhanden, kann dieser immer weiter verbessert und verfeinert werden, bis man auch damit beginnen kann, ihn f\"{u}r das \sisac-Projekt zu nutzen. |
189 |
195 |
190 Daneben kann an der Weiterentwicklung des GUIs gearbeitet werden und die ersten Schritte zur Ann\"{a}herung an das Isabelle-Plugin k\"{o}nnen hier erfolgen. |
196 Daneben kann an der Weiterentwicklung des GUIs gearbeitet werden und die ersten Schritte zur Ann\"{a}herung an das Isabelle-Plugin k\"{o}nnen hier erfolgen. |
191 |
197 |
192 \chapter{Zusammenfassung und R\"{u}ckblick} |
198 \chapter{Zusammenfassung und R\"{u}ckblick} |
|
199 Zusammenfassend wird nun ein \"Uberblick gegeben, welche Milestones erledigt wurden und welche nicht; Details dazu finden sich in Anhang A. %TODO |
|
200 Abschlie{\ss}end gebe ich einen R\"uckblick auf meine pers\"onlichen Erfahrungen aus dieser Bakkalaureats-Arbeit. |
|
201 |
|
202 \section{Zusammenfassung} |
|
203 Folgende Milestones wurden erfolgreich abgeschlossen: |
|
204 \begin{enumerate} |
|
205 \item Relevante Isabelle Komponenten dokumentiert |
|
206 |
|
207 \item Installation der Standard-Komponenten: |
|
208 \begin{itemize} |
|
209 \item Mercurial Versioncontrol |
|
210 \item NetBeans IDE |
|
211 \item Standard Isabelle Bundle |
|
212 \end{itemize} |
|
213 |
|
214 \item Entwicklungsumgebung vom Isabelle-Team kopieren |
|
215 \begin{itemize} |
|
216 \item Isabelle-Sources vom Repository M\"unchen (Java, Scala, ML) |
|
217 \item jEdit als NetBeans Projekt definiert |
|
218 \end{itemize} |
|
219 |
|
220 \item Relevante Komponenten implementieren |
|
221 \begin{itemize} |
|
222 \item jEdit Plugin f\"ur SD |
|
223 \item Verbindung des Plugins zu Isabelle |
|
224 \item zugeh\"origen Parser: nur ein Test in SML |
|
225 \end{itemize} |
|
226 \end{enumerate} |
|
227 |
|
228 \noindent Aus Zeitgr\"unden war {\em nicht} m\"oglich, ein komplettes SD-Plugin zu implementieren; dazu w\"are auch ein Interpreter f\"ur SD auf der ML-Seite n\"otig gewesen. |
|
229 |
|
230 \paragraph{Voraussetzungen f\"ur k\"unftige Entwicklung} geschaffen: |
|
231 \begin{enumerate} |
|
232 \item f\"ur die Implementation von ``structured derivations'' in Isabelle \dots |
|
233 \item \dots als Vorarbeit f\"ur jEdit als k\"unftiges \isac-Frontend |
|
234 \item f\"ur Mitarbeit an k\"unftiger Integration von Isabelle in Entwicklungswerkzeuge (Testcase-Generation etc). |
|
235 \end{enumerate} |
|
236 |
|
237 \section{R\"uckblick} |
193 Isabelle ist ein sehr gro\ss es Softwarepacket mit mehreren Millionen LOC. Daher gestaltete sich die Einarbeitungsphase sehr schwierig und kostet sehr viel Zeit. Erschwerend kam hinzu, dass ich von Beginn an mit mehreren, f\"{u}r mich noch ganz neue, Technologien arbeiten musste. Diese Herausforderungen schon zu Beginn machten die Arbeit an \sisac{ }von Beginn an spannend. Hier ist mir vorallem die gemeinsam mit meinem Betreuer Herrn Walther Neuper durchgef\"{u}hrte Installationsarbeit von Isabelle in Erinnerung geblieben. Nie zuvor hatte ich f\"{u}r eine Installation von Software so lange gebraucht - eine ganz neue, wichtige Erfahrung. |
238 Isabelle ist ein sehr gro\ss es Softwarepacket mit mehreren Millionen LOC. Daher gestaltete sich die Einarbeitungsphase sehr schwierig und kostet sehr viel Zeit. Erschwerend kam hinzu, dass ich von Beginn an mit mehreren, f\"{u}r mich noch ganz neue, Technologien arbeiten musste. Diese Herausforderungen schon zu Beginn machten die Arbeit an \sisac{ }von Beginn an spannend. Hier ist mir vorallem die gemeinsam mit meinem Betreuer Herrn Walther Neuper durchgef\"{u}hrte Installationsarbeit von Isabelle in Erinnerung geblieben. Nie zuvor hatte ich f\"{u}r eine Installation von Software so lange gebraucht - eine ganz neue, wichtige Erfahrung. |
194 |
239 |
195 Einer der bedeutensten Milesteine war r\"{u}ckblickend wohl, die Verzeichnisstruktur von Isabelle grunds\"atzlich verstanden zu haben. Bei einem Softwarepacket von dieser Gr\"{o}{\ss}e war es wichtig zu wissen, wo man Files suchen/modifizieren/einf\"{u}gen muss, um den gew\"{u}nschten Effekt erreichen zu können. |
240 Einer der bedeutensten Milesteine war r\"{u}ckblickend wohl, die Verzeichnisstruktur von Isabelle grunds\"atzlich verstanden zu haben. Bei einem Softwarepacket von dieser Gr\"{o}{\ss}e war es wichtig zu wissen, wo man Files suchen/modifizieren/einf\"{u}gen muss, um den gew\"{u}nschten Effekt erreichen zu können. |
196 |
241 |
197 Der n\"achste wichtige Schritt war das bereits teilweise bestehende NetBeansprojekt lauff\"ahig zu machen und mir damit zum ersten mal selbst das jEdit-Isabelle-Plugin erzeugen zu k\"onnen. Dies war ein sehr bedeutsamer Schritt, da ich hier zum einen NetBeans und dessen Konfiguration besser kennenlernen konnte und zum anderen sehr viel \"{u}ber die Pluginstruktur eines jEdit-Plugins lernen konnte. Zu Beginn machte mir hier der Mix aus Scala-, Java-, XML- und diversen Config-Files Probleme. |
242 Der n\"achste wichtige Schritt war das bereits teilweise bestehende NetBeansprojekt lauff\"ahig zu machen und mir damit zum ersten mal selbst das jEdit-Isabelle-Plugin erzeugen zu k\"onnen. Dies war ein sehr bedeutsamer Schritt, da ich hier zum einen NetBeans und dessen Konfiguration besser kennenlernen konnte und zum anderen sehr viel \"{u}ber die Pluginstruktur eines jEdit-Plugins lernen konnte. Zu Beginn machte mir hier der Mix aus Scala-, Java-, XML- und diversen Config-Files Probleme. |
198 |
243 |
199 Bis jetzt hatte ich eigentlich noch nicht wirklich mit der Programmierung des Plugins begonnen doch es waren schon zig Arbeitsstunden rein f\"{u}r Einarbeitungs- und Vorbereitungsaufgaben verstrichen - wieder eine neue Erfahrung f\"{u}r mich. Nach einigen Test- bzw. Beispielprogrammen um die Sprache Scala etwas kennenzulernen, begann die wohl spannenste Phase im Projektverlauf. Das in Java geschriebene Beispielplugin "Quick-Notepad" wurde in Scala \"{u}bersetzt und etwas abge\"andert. |
244 Bis jetzt hatte ich eigentlich noch nicht wirklich mit der Programmierung des Plugins begonnen doch es waren schon zig Arbeitsstunden rein f\"{u}r Einarbeitungs- und Vorbereitungsaufgaben verstrichen - wieder eine neue Erfahrung f\"{u}r mich. Nach einigen Test- bzw. Beispielprogrammen um die Sprache Scala etwas kennenzulernen, begann die wohl spannenste Phase im Projektverlauf. Das in Java geschriebene Beispielplugin "Quick-Notepad" wurde in Scala \"{u}bersetzt und etwas abge\"andert. |
200 |
245 |
201 Der letzte wirklich bedeutende Schritt war Herstellung der Verbindung zwischen Isabelle-Pure und \sisac. Dieser Punkt ist sehr wichtig, da ohne diese Schnittstelle die Planung des SD-Parser nicht m\"oglich gewesen w\"are. Der letzte Schritt, also die Implementation des SD-Parsers wurde aufgeschoben, da es derzeit seitens des Isabelle-Teams ebenfalls Bestrebungen gibt, einen neuen Scala-Parser zu designen und wir von diesen Erkenntnissen mit Sicherheit profitieren k\"onnen. |
246 Der letzte wirklich bedeutende Schritt war Herstellung der Verbindung zwischen Isabelle-Pure und \sisac. Dieser Punkt ist sehr wichtig, da ohne diese Schnittstelle die Planung des SD-Parser nicht m\"oglich gewesen w\"are. Der letzte Schritt, also die Implementation des SD-Parsers wurde aufgeschoben, da es derzeit seitens des Isabelle-Teams ebenfalls Bestrebungen gibt, einen neuen Scala-Parser zu designen und wir von diesen Erkenntnissen mit Sicherheit in der Zunkft profitieren k\"onnen. |
202 |
247 |
203 Abschlie{\ss}end m\"ochte ich mich bei meinem Betreuer Herrn Walther Neuper sehr herzlich f\"{u}r die gute Betreuung und die spannenden Entwicklungsstuden bedanken. Es war eine sehr lehrreiche und interessante Projektarbeit! |
248 %Abschlie{\ss}end m\"ochte ich mich bei meinem Betreuer Herrn Walther Neuper sehr herzlich f\"{u}r die gute Betreuung und die spannenden Entwicklungsstuden bedanken. Es war eine sehr lehrreiche und interessante Projektarbeit! |
204 |
249 |
205 %\chapter{Milestones und Arbeitsprotokolle} |
250 %\chapter{Milestones und Arbeitsprotokolle} |
206 %\section{Inhaltliche Voraussetzungen erarbeitet: beendet am 27.09.2010} |
251 %\section{Inhaltliche Voraussetzungen erarbeitet: beendet am 27.09.2010} |
207 %\begin{itemize} |
252 %\begin{itemize} |
208 %\item Kenntnis der Grundlagen und Anwendung von CTP: beendet am 03.08.2010 |
253 %\item Kenntnis der Grundlagen und Anwendung von CTP: beendet am 03.08.2010 |