Kann LaTeX nicht von Isabelle/HOL unter Windows7 generieren

Question

Ich habe zu viele Stunden damit verbracht, ein .pdf-Dokument aus meiner Isabelle-Theorie Increments.thy zu erzeugen. Der Build-Befehl von Isabelle bleibt hängen und das ist anscheinend eine Installationssache unter Windows. Frustrierend genug, Freunde haben dies auf ihren Linux-Maschinen getan und sie erleben überhaupt keine Probleme. Aber ich kann nicht die richtige Dokumentation finden, um es auf meinem Windows 7-Laptop zu starten. Hat jemand das Rezept?

Ich habe eine vollständige LaTeX-Installation auf meinem Laptop, funktioniert wie ein Kinderspiel. Ich habe CYGWIN installiert, aber es gab Probleme mit Zugriffsrechten von Dateien, die ich nicht lösen konnte (weder vom Windows-Ende, noch vom Cygwin-Ende). Ich habe verschiedene Handbücher ausprobiert, ohne viel Glück.

Answer 1

Mit einiger praktischer Hilfe der Universität Innsbruck konnte ich endlich ein pdf aus einer Isabelle-Theorie auf meinem Windows-7 Laptop erstellen. Ich möchte das Ergebnis für die Gemeinschaft insgesamt teilen. Hier ist, was ich getan habe, damit es funktioniert:

1. In Microsoft Explorer ging ich zu dem Verzeichnis, das die ausführbaren Isabelle-Dateien enthält. Dieses Verzeichnis heißt Isabelle2016-1. Ich habe es gefunden, indem ich im Dateisystem nach Isabelle2016-1 gesucht habe. Es ist auf C:\Users\sjo\AppData\Roaming\local\bin\Isabelle2016-1. Ich habe überprüft, dass es die Datei Cygwin-Terminal.bat enthält.

2. Ich habe die Datei Cygwin-Terminal.bat mit einem Doppelklick aufgerufen. Dies öffnet einen Befehlszeileninterpreter (CLI), der der GNU Bash-Interpreter ist.

3. In diesem CLI, navigiert ich in das Verzeichnis, das meine Isabelle Quellcode enthält, Increments.sty, mit dem folgenden Befehl:

   $ cd /cygdrive/d/git/Publications/2017AFPproofs 
   

   ich den Befehl ls -al, um zu überprüfen, dass dieses Verzeichnis meines Isabelle Quellcode enthält Datei Increments.thy.

4. I erzeugt eine pdf-Datei D:\git\Publications\2017AFPproofs\output\document\root.pdf von Isabelle Aufruf:

   $ isabelle build -v -D . 
   

   ich das Ergebnis in Microsoft Explorer überprüft und angezeigt mit meinem pdf-Viewer.

Das hat funktioniert.