Impossible de générer LaTeX à partir d'Isabelle/HOL sous Windows7

Question

J'ai passé trop d'heures à essayer de générer un document .pdf à partir de ma théorie Isabelle Increments.thy. La commande de compilation Isabelle est bloquée et il s'agit apparemment d'une installation sous Windows. Assez frustrant, les amis ont fait cela sur leurs machines Linux et ils ne rencontrent aucun problème. Mais je ne peux pas trouver la bonne documentation pour le faire fonctionner sur mon ordinateur portable Windows 7. Est-ce que quelqu'un a la recette?

J'ai une installation LaTeX complète sur mon ordinateur portable, fonctionnant comme un jeu d'enfant. J'ai installé CYGWIN, mais cela a donné des problèmes avec les droits d'accès aux fichiers, que je n'ai pas pu résoudre (ni à partir de Windows, ni à partir de cygwin-end). J'ai essayé différents manuels, sans trop de chance.

Answer 1

Avec l'aide de l'université d'Innsbruck, j'ai pu enfin générer un pdf à partir d'une théorie d'Isabelle sur mon ordinateur portable Windows-7. J'aimerais partager le résultat pour la communauté dans son ensemble. Voici ce que j'ai fait pour le faire fonctionner:

1. Dans Microsoft Explorer, je suis allé dans le répertoire qui contient les exécutables Isabelle. Ce répertoire s'appelle Isabelle2016-1. Je l'ai trouvé en cherchant Isabelle2016-1 dans le système de fichiers. C'est au C:\Users\sjo\AppData\Roaming\local\bin\Isabelle2016-1. J'ai vérifié qu'il contient le fichier Cygwin-Terminal.bat.

2. J'ai appelé le fichier Cygwin-Terminal.bat en double-cliquant dessus. Cela ouvre un interpréteur de ligne de commande (CLI), qui est l'interpréteur GNU Bash.

3. Dans cette CLI, je naviguaient dans le répertoire qui contient mon code source Isabelle, Increments.sty, en lançant la commande:

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

   je la commande ls -al pour vérifier que ce répertoire contient mon code source Isabelle fichier Increments.thy.

4. I généré un fichier pdf D:\git\Publications\2017AFPproofs\output\document\root.pdf en appelant Isabelle:

   $ isabelle build -v -D . 
   

   J'ai vérifié le résultat dans Microsoft Explorer et affiche avec mes pdf-viewer.

Cela a fonctionné.