はのWindows7

Question

私はイザベル理論 Increments.thyのうちの.pdfドキュメントを生成しようとしている、あまりにも多くの時間を費やしている

下イザベル/ HOLからのLaTeXを生成できません。 Isabelleのビルドコマンドが止まってしまい、明らかにこれはWindows上のインストールです。悔しいことに、友人たちはLinuxマシンでこれをやっており、全く問題はありません。しかし、私はそれを私のWindows 7のラップトップに行くための正しいドキュメントを見つけることができません。誰にもレシピはありますか？

私は自分のラップトップに完全なLaTeXをインストールしています。私はCYGWINをインストールしましたが、ファイルのアクセス権に問題がありました.Windows-EndでもCygwin-Endでも解決できませんでした。たくさんの運が無ければ、私は様々なマニュアルを試しました。いくつかのハンズオンインスブルックの大学の助けを借りて

Answer 1

、私はようやく私のWindows 7のラップトップ上のイザベル理論からPDFを生成することができます。コミュニティ全体の結果を共有したいと思います。ここで私はそれを動作させるためにしたものです：

1. 私は、エクスプローラで、私はIsabelle実行可能ファイルを含むディレクトリに行きました。このディレクトリはIsabelle2016-1と呼ばれます。 ファイルシステムでIsabelle2016-1を検索すると見つかりました。それはC:\Users\sjo\AppData\Roaming\local\bin\Isabelle2016-1にあります。 ファイルにCygwin-Terminal.batが含まれていることを確認しました。

2. は、私はそれをダブルクリックしてファイルCygwin-Terminal.batと呼ばれます。 これは、GNU Bashインタプリタであるコマンドラインインタプリタ（CLI）を開きます。このCLIで

3. は、私はコマンドを発行することにより、Increments.sty、私のイザベルのソースコードを含むディレクトリにナビゲート：

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

   私は、このディレクトリは、私のイザベルのソースコードが含まれていることを確認するためのコマンドls -alを使用しましたファイル。

4. 私はイザベルを呼び出すことにより、PDFファイルD:\git\Publications\2017AFPproofs\output\document\root.pdf生成：

   $ isabelle build -v -D . 
   

   を私には、Microsoft Explorerで結果を確認し、私のPDFビューアでそれを表示します。

これはうまくいきました。