如何生成html版本的Isabelle理論

我有一個Isabelle理論文件，名爲John.thy。我想將它展示給我的朋友，但我的朋友沒有Isabelle，並且原始.thy文件不太容易閱讀。我在伊莎貝爾圖書館看到了一些網頁（如這個：http://isabelle.in.tum.de/library/HOL/Finite_Set.html），它們有着漂亮的語法突出顯示，我希望我的理論看起來像這樣。如何生成html版本的Isabelle理論

那麼我該如何製作John.html？我已經看過文檔，它看起來相當可怕和困難，什麼與所有的構建文件和製作文件等。難道某種靈魂可以解釋做到這一點的最簡單方法嗎？

來源

2013-07-24 John Wickerson

也許你也可以在你的文章中將大寫字母改爲'John.thy'和'John.html'（爲了讓未來的讀者能夠看到這個約定）。然後我可以從我的答案中刪除我對它的評論。 – chris

首先回答你的問題（也見Isabelle System Manual，第3.2節 - 系統生成選項）：

要爲John.thy生成HTML，創建一個名爲ROOT文件，在同一目錄John.thy，具有以下內容

session John = "HOL" + 
    theories 
    John

然後，住在同一個目錄下，調用

isabelle build -d . -o browser_info -v John

其中

-d .指定當前目錄應該被搜索會話（其在一個ROOT文件中指定）
-o browser_info是生成HTML的基本標誌（也稱爲瀏覽器信息）和
-v（在詳細標誌）是有用的，看看在哪個目錄結果把

以上調用將類似於

Started at Thu Jul 25 09:38:20 JST 2013 [...] 
[...] 
Session Pure 
Session HOL (main) 
Session John 
Running John ... 
John: theory John 
[...] 
Browser info at /home/username/.isabelle/Isabelle2013/browser_info/HOL/John 
[...]

輸出的東西（其中[...]表示省略輸出）。所以在這裏你可以看到你需要查閱哪個目錄來獲取HTML文件。當使用

與-o browser_info你會得到一堆文件在一個目錄（而不是隻是一個單一的自包含的文件：

話雖如此，至少在以下幾個原因我個人更喜歡PDF在HTML -o document=pdf）
不是所有的伊莎貝爾符號很好地呈現在HTML（而你有過的符號生成的PDF文件時，完全控制）

注：如果您正在使用適用於Mac OS的Isabelle應用程序，您可能需要將isabelle替換爲/Applications/Isabelle2013.app/Isabelle/bin/isabelle或將/Applications/Isabelle2013.app/Isabelle/bin/添加到您的PATH。

來源

2013-07-25 00:47:33 chris

很好的答案，謝謝克里斯。我已經自由地澄清了在這個過程的每個步驟中需要在哪個目錄中，因爲這是我以前困惑的事情。我發現我需要在我的機器上安裝Isabelle的完整路徑，所以我還添加了一個關於此的說明。 –

您提到理論名稱以大寫字母開頭是慣例。會話名稱也一樣。 –

@LarsNoschinski好點。我相應地改變了我的答案。 – chris

如何生成html版本的Isabelle理論

回答

相關問題