79 \section{Isabelle} |
79 \section{Isabelle} |
80 Isabelle ist einer der f\"{u}hrenden CTPs und an dessen Weiterentwicklung wird st\"{a}ndig gearbeitet. Der letzte gro{\ss}e Schritt betraf den Umstieg von reinem ML auf die Mischsprache Scala. Weiters wurde der in die Jahre gekommene Proof General und der damit in Verbindung stehende Editor Emacs durch den vielseitigen Editor jEdit ersetzt. Dadurch ergeben sich auch f\"{u}r das laufende \sisac-Projekt an der TU Graz neue M\"{o}glichkeiten. Wichtig im Zusammenhang mit dieser Beschreibung ist zu erw\"{a}hnen, dass hier in weiterer Folge nur noch f\"{u}r jEdit bzw. Scala relevante Teile von Isabelle behandelt und beschrieben werden. Weiters ist wichtig zu wissen, dass f\"{u}r die bereits bestehende Struktur rund um Isablle-jEdit zwei Isabelle-Pakete zum Einsatz kommen. Auf diese Pakete soll in den n\"{a}chsten Passagen eingegangen werden. |
80 Isabelle ist einer der f\"{u}hrenden CTPs und an dessen Weiterentwicklung wird st\"{a}ndig gearbeitet. Der letzte gro{\ss}e Schritt betraf den Umstieg von reinem ML auf die Mischsprache Scala. Weiters wurde der in die Jahre gekommene Proof General und der damit in Verbindung stehende Editor Emacs durch den vielseitigen Editor jEdit ersetzt. Dadurch ergeben sich auch f\"{u}r das laufende \sisac-Projekt an der TU Graz neue M\"{o}glichkeiten. Wichtig im Zusammenhang mit dieser Beschreibung ist zu erw\"{a}hnen, dass hier in weiterer Folge nur noch f\"{u}r jEdit bzw. Scala relevante Teile von Isabelle behandelt und beschrieben werden. Weiters ist wichtig zu wissen, dass f\"{u}r die bereits bestehende Struktur rund um Isablle-jEdit zwei Isabelle-Pakete zum Einsatz kommen. Auf diese Pakete soll in den n\"{a}chsten Passagen eingegangen werden. |
81 |
81 |
82 \subsection{Isabelle-Pure} |
82 \subsection{Isabelle-Pure} |
83 In diesem Plugin ist der eigentliche CTP-Teil von Isabelle verpackt. Das bedeutet im weiteren Sinn, dass es hier keine grafische Verarbeitung der Daten gibt, sondern der Zugriff von aussen erforderich ist, um den CTP mit Daten zu versorgen und diese nach deren Verabreitung in Isabelle-Pure auszuwerten. Also ist nur hier eine Schnittstelle zum eigentlichen Proofer m\"{o}glich und deshalb ist dieses Plugin f\"{u}r das \sisac-Projekt von zentraler Bedeutung. Standardm\"{a}{\ss}ig ist bereits ein Pure.jar-Paket f\"{u}r jEdit vorhanden. Um SD umsetzten zu k\"{o}nnen, muss hier eine Schnittstelle zu Isabelle-Pure implementiert werden. Nach diesem Schritt kann das Plugin Pure.jar neu gebaut werden. |
83 In diesem Plugin ist der eigentliche CTP-Teil von Isabelle verpackt. Das bedeutet im weiteren Sinn, dass es hier keine grafische Verarbeitung der Daten gibt, sondern der Zugriff von aussen erforderich ist, um den CTP mit Daten zu versorgen und diese nach deren Verabreitung in Isabelle-Pure auszuwerten. Also ist nur hier eine Schnittstelle zum eigentlichen Proofer m\"{o}glich und deshalb ist dieses Plugin f\"{u}r das \sisac-Projekt von zentraler Bedeutung. Standardm\"{a}{\ss}ig ist bereits ein Pure.jar-Paket f\"{u}r jEdit vorhanden. Um SD umsetzten zu k\"{o}nnen, muss hier eine Schnittstelle zu Isabelle-Pure implementiert werden. Nach diesem Schritt kann das Plugin Pure.jar neu gebaut werden. |
84 Eine Auflistung der f\"ur das Isabelle-Pure-Packet ben\"otigten Scala-Source-Files kann Anhang B.2 entnommen werden. |
84 Eine Auflistung der f\"ur das Isabelle-Pure-Packet ben\"otigten Scala-Source-Filles kann Anhang B.2 entnommen werden. |
85 |
85 |
86 \subsection{Isabelle-jEdit} |
86 \subsection{Isabelle-jEdit} |
87 Dieser Teil von Isabelle repr\"{a}sentiert das Frontend in jEdit. Hier wird also die grafische Aufbereitung der von Isabelle-Pure berechneten Daten \"{u}bernommen. Dieses Plugin zeigt sehr sch\"{o}n, wie bereits bestehende Plugins weiter genutzt und erweitert werden k\"{o}nnen. |
87 Dieser Teil von Isabelle repr\"{a}sentiert das Frontend in jEdit. Hier wird also die grafische Aufbereitung der von Isabelle-Pure berechneten Daten \"{u}bernommen. Dieses Plugin zeigt sehr sch\"{o}n, wie bereits bestehende Plugins weiter genutzt und erweitert werden k\"{o}nnen. |
88 An diesem Plugin wird von Seiten der Isabelle-Entwickler sehr stark weitergearbeitet. Darum sollten hier wohl nicht zu viele, am besten nat\"{u}rlich keine \"{A}nderungen, vorgenommen werden. Der Umstand, dass sich einzelne Plugins ganz einfach in einem anderen mitverwenden lassen, macht es m\"{o}glich, dass das \sisac-Plugin sehr einfach, im Idealfall von Seiten der Isabelle-Entwickler, in das Isabelle-jEdit-Plugin integriert werden kann. |
88 An diesem Plugin wird von Seiten der Isabelle-Entwickler sehr stark weitergearbeitet. Darum sollten hier wohl nicht zu viele, am besten nat\"{u}rlich keine \"{A}nderungen, vorgenommen werden. Der Umstand, dass sich einzelne Plugins ganz einfach in einem anderen mitverwenden lassen, macht es m\"{o}glich, dass das \sisac-Plugin sehr einfach, im Idealfall von Seiten der Isabelle-Entwickler, in das Isabelle-jEdit-Plugin integriert werden kann. |
89 |
89 |
90 \subsection{Paketstruktur von Isabelle} |
90 \subsection{Paketstruktur von Isabelle} |
91 Durch die Komplexit\"{a}t des Isabelle-Entwicklungs-Aufbaus soll hier eine Auflistung aller relevanten jar-Pakete erfolgen. Alle Pakete befinden sich innerhalb der Ordnerstruktur von ISABELLE\_HOME. Darum wird ab hier immer von diesem Verzeichnis ausgegangen. |
91 pDurch die Komplexit\"{a}t des Isabelle-Entwicklungs-Aufbaus soll hier eine Auflistung aller relevanten jar-Pakete erfolgen. Alle Pakete befinden sich innerhalb der Ordnerstruktur von ISABELLE\_HOME. Darum wird ab hier immer von diesem Verzeichnis ausgegangen. |
92 Die nachfolgende Auflistung zeigt alle Pakete, die f\"{u}r SD bzw. \sisac von Bedeutung sind und und wo diese zu finden sind. |
92 Die nachfolgende Auflistung zeigt alle Pakete, die f\"{u}r SD bzw. \sisac von Bedeutung sind und und wo diese zu finden sind. |
93 |
93 |
94 |
94 |
95 \begin{itemize} |
95 \begin{itemize} |
96 \item \textit{contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, ...} Der Ordner contrib ist in der Repository-Version nicht vorhanden! Dieser kann dem Isabelle-Bundle entnommen werden. Hier befinden sich alle ben\"{o}tigten Zusatztools f\"{u}r Isabelle und darunter eben auch jEdit. In dem oben angef\"{u}hrten Ordner liegen alle Plugins bzw. dorthin werden alle Plugins kopiert, die zusammen mit jEdit gestartet werden sollen. Das oben angef\"{u}hrte Script \"{u}bernimmt genau diesen Kopiervorgang f\"{u}r Isac.jar und Pure.jar. |
96 \item \textit{contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars:} \textbf{Isabelle-jEdit.jar, Pure.jar, SideKick.jar, ...} Der Ordner contrib ist in der Repository-Version nicht vorhanden! Dieser kann dem Isabelle-Bundle entnommen werden. Hier befinden sich alle ben\"{o}tigten Zusatztools f\"{u}r Isabelle und darunter eben auch jEdit. In dem oben angef\"{u}hrten Ordner liegen alle Plugins bzw. dorthin werden alle Plugins kopiert, die zusammen mit jEdit gestartet werden sollen. Das oben angef\"{u}hrte Script \"{u}bernimmt genau diesen Kopiervorgang f\"{u}r Isac.jar und Pure.jar. |
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. |
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 |
140 |
141 \section{Konfiguration des Netbeans Projektes} |
141 \section{Konfiguration des Netbeans Projektes} |
142 Um in k\"unftigen Entwicklungsvorhaben effizient kooperieren zu k\"onnen, wurde das Netbeans-Projekt genau nach den Vorgaben des Isabelle-Teams konfiguriert. |
142 Um in k\"unftigen Entwicklungsvorhaben effizient kooperieren zu k\"onnen, wurde das Netbeans-Projekt genau nach den Vorgaben des Isabelle-Teams konfiguriert. |
143 |
143 |
144 TODO |
144 \begin{enumerate} |
|
145 \item Konfigurations-Files von Netbeans in ``Files''-View; beeinflussen sich gegenseitig |
|
146 \begin{enumerate} |
|
147 \item build.xml (aus template erzeugt, keine automatischen Ver\"anderunen) |
|
148 \item nbproject/build-impl.xml (z.T. automatische Ver\"anderunen) |
|
149 \item nbproject/project.xml (z.T. automatische Ver\"anderunen) |
|
150 \item TODO |
|
151 \end{enumerate} |
|
152 \item Sacla-plugin installieren laut http://wiki.netbeans.org/Scala69, |
|
153 \begin{enumerate} |
|
154 \item von ``Install with NetBeasn 6.9'' |
|
155 \item nach /usr/local/netbeans.../plugins/scala |
|
156 \end{enumerate} |
|
157 \item Scala-plugin installiert in NetBeans |
|
158 \begin{enumerate} |
|
159 \item Men\"u $>$ Tools $>$ Plugins $>$ Downloaded $>$ Add Plugins |
|
160 \item alle Files von /usr/local/netbeans.../plugins/scala/ |
|
161 \item Fenster zeigt alle ausgew\"alten Files |
|
162 \item $<$Install$>$ calls Wizzard $<$Next$>$ probably accept Warning |
|
163 \item Funktionstest: Men\"ue $>$ Files $>$ New Project: zeigt Scala als ``Categories'' |
|
164 \end{enumerate} |
|
165 \item Neues Projekt ``isac-jedit'' konfigurieren |
|
166 \begin{enumerate} |
|
167 \item Men\"u $>$ Open Project (weil schon aus dem Repository die notwendigen Files vorhanden sind) |
|
168 \item /src/Tools/jeditC: Reference Problems, weil jEdit folgende Plugins braucht |
|
169 \item Funktionskontrolle: ``Projects''-View zeigt das neue Projekt |
|
170 \item Die Konfigurations-Files sind v\"ollig getrennt von anderen Projekten |
|
171 \item Referenz-Probleme beheben; das zeigt auch eventuell fehlende Files |
|
172 \begin{enumerate} |
|
173 \item ``Projects''-View $>$ rightMouse $>$ Resolve Reference Problems: Fenster zeigt dieListe der fehlenden Dateien; $<$Next$>$ |
|
174 \item Files holen aus ``Tools'' $>$ Libraries: \"uber Filebrowser aus dem Isabelle\_bundle holen contrib/jEdit---/jars |
|
175 \item ``New Library'' |
|
176 \begin{enumerate} |
|
177 \item Cobra-renderer: cobra.jar |
|
178 \item Console: Console.jar |
|
179 \item ErrorList: ErrorList.jar |
|
180 \item Hyperlinks: Hyperlinks.jar |
|
181 \item Isabelle-Pure: Pure.jar |
|
182 \item Rhino-JavaScript: js.jar |
|
183 \item Scala-compiler: scala-compiler.jar |
|
184 \item SideKick: SideKick.jar |
|
185 \end{enumerate} |
|
186 \item Funktions-Kontrollen |
|
187 \begin{enumerate} |
|
188 \item das kleine gelbe Warndreieck im ``Projects''-View ist verschwunden |
|
189 \item im ``Projects''-View 2 Ordner: ``src'' und ``Libraries'' |
|
190 \end{enumerate} |
|
191 \end{enumerate} |
|
192 \item jEdit-Paket zum ``isac-jedit''-Projekt hinzuf\"ugen |
|
193 \begin{enumerate} |
|
194 \item ``Project''-View $>$ rightMouse $>$ Add Jar/Folder: Filebrowser |
|
195 \item /contrib/jedit.../jedit.jar |
|
196 \item Funktions-Kontrolle: ist in ``Projects''/Libraries/jedit.jar |
|
197 \end{enumerate} |
|
198 \item Das neue Projekt ``isac-jedit'' zum Hauptprojekt machen: ``Project''-View $>$ rightMouse $>$ Set as Main Project; Funktions-Kontrolle: der Projektname ist boldface. |
|
199 \end{enumerate} |
|
200 \item Ab nun wird die Konfiguration \"uber ``trial and error'' zu Ende gef\"uhrt |
|
201 \begin{enumerate} |
|
202 \item Men\"u $>$ Build Main |
|
203 \begin{enumerate} |
|
204 \item Wenn: Target ``Isac-impl.jar'' does not exist in the project ``isac-jedit''. It is used from target ``debug'' |
|
205 \begin{enumerate} |
|
206 \item Versuch |
|
207 \begin{itemize} |
|
208 \item build-impl.xml l\"oschen |
|
209 \item NetBeans neu starten, stellt build-impl.xml automatisch aus build.xml wieder her |
|
210 \item \dots hat in diesem Fall nicht geholfen |
|
211 \end{itemize} |
|
212 \item Versuch zur Vermutung: Projekt wurde umbenannt von ``Isac'' in ``isac-jedit'', und das machte build.xml inkonsistent |
|
213 \begin{itemize} |
|
214 \item in build.xml query-replace ``Isac'' in ``isac-jedit'' |
|
215 \item TODO? |
|
216 \item |
|
217 \end{itemize} |
|
218 \end{enumerate} |
|
219 \item Wenn: Problem: failed to create tsk or type scalac |
|
220 \begin{enumerate} |
|
221 \item Versuch: Pfad zum Scala bekanntgeben |
|
222 \begin{itemize} |
|
223 \item /usr/local/netbeans-6.9.1/etc/netbeans.conf: netbeans\_default\_options= richtigen Scala-Pfad setzen |
|
224 \item build-impl.xml l\"oschen |
|
225 \item NetBeans neu starten. |
|
226 \end{itemize} |
|
227 \end{enumerate} |
|
228 \item Wenn Fehler: ``/usr/local/isabisac/src/Tools/jEditC/\${project.jEdit}/modes does not exist'' |
|
229 \begin{enumerate} |
|
230 \item grep -r "project.jEdit" * |
|
231 \item nbproject/project.properties:project.jEdit=contrib/jEdit |
|
232 \item |
|
233 \item |
|
234 |
|
235 \begin{itemize} |
|
236 \item |
|
237 \begin{itemize} |
|
238 \item |
|
239 \item |
|
240 \item |
|
241 \end{itemize} |
|
242 \item |
|
243 \item |
|
244 \end{itemize} |
|
245 \item |
|
246 \item |
|
247 \end{enumerate} |
|
248 \item |
|
249 \item |
|
250 \end{enumerate} |
|
251 \end{enumerate} |
|
252 $<$ $>$ |
|
253 Men\"u $>$ $>$ $>$ $>$ $>$ $>$ |
|
254 ``Project''-View $>$ rightMouse $>$ $>$ $>$ $>$ $>$ |
|
255 \item |
|
256 \begin{enumerate} |
|
257 \item |
|
258 \begin{enumerate} |
|
259 \item |
|
260 \begin{itemize} |
|
261 \item |
|
262 \begin{itemize} |
|
263 \item |
|
264 \item |
|
265 \item |
|
266 \end{itemize} |
|
267 \item |
|
268 \item |
|
269 \end{itemize} |
|
270 \item |
|
271 \item |
|
272 \end{enumerate} |
|
273 \item |
|
274 \item |
|
275 \end{enumerate} |
|
276 \item |
|
277 \begin{enumerate} |
|
278 \item |
|
279 \begin{enumerate} |
|
280 \item |
|
281 \begin{itemize} |
|
282 \item |
|
283 \begin{itemize} |
|
284 \item |
|
285 \item |
|
286 \item |
|
287 \end{itemize} |
|
288 \item |
|
289 \item |
|
290 \end{itemize} |
|
291 \item |
|
292 \item |
|
293 \end{enumerate} |
|
294 \item |
|
295 \item |
|
296 \end{enumerate} |
|
297 \end{enumerate} |
145 |
298 |
146 |
299 |
147 \section{Implementation der jEdit Komponenten} |
300 \section{Implementation der jEdit Komponenten} |
148 |
301 |
149 \subsection{Erstellen des Plugin-Ger\"{u}sts} |
302 \subsection{Erstellen des Plugin-Ger\"{u}sts} |