生成Isabelle HTML文檔*無需校樣*

Question

我希望爲Isabelle理論（例如HOL會話）生成HTML文檔，但不包含的校樣。

也就是說，我想產生像http://isabelle.in.tum.de/library/HOL/Nat.html 而是，例如網頁，

lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==> 
    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n" 
    apply (rule_tac x = m in spec) 
    apply (induct n) 
    prefer 2 
    apply (rule allI) 
    apply (induct_tac x, iprover+) 
    done 

我只想看到

lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==> 
    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n" 

的原因是，我使用的HTML頁面看看有哪些定理可用，但證明只是分散注意力。 （我知道在生成PDF時省略證明是可能的，但我特別感興趣的是HTML文檔。）

Answer 1

不幸的是，目前在Isabelle中沒有內置的方法來執行此操作（HTML代用於包含摘要幾年前，但不再提供）。

你可以考慮後處理生成的HTML文件，但這可能聽起來比較複雜。

你最好的賭注是當前的輪廓PDF，正如克里斯指出，使用類似

find_theorems name: "MyThy." 

一個命令來獲取理論上MyThy所有定理的列表。您可以使用術語表達式或僅使用常量名稱來擴充find_theorems命令以將搜索範圍縮小爲特定的常量。這通常比瀏覽長定理列表更有效。您可以類似地使用命令find_consts按類型，常數名稱或理論名稱查找常量，例如，得到一個理論中定義的所有常量的列表。

Answer 2

我最近遇到了coqdoc輸出，並且從這個角度可以理解這個問題，儘管Coq HTML頁面現在也顯示了它們的年齡。

在Isabelle的HTML演示文稿曾經非常重要，然後其他工具，如在線find_theorems或離線PDF文件變得更加強大和有用，現在還有Isabelle/jEdit具有近似HTML瀏覽器的顯示品質， Isabelle HTML輸出首次實現。

我不知道一個簡單的方法來得到你在現代伊莎貝爾2013年所要求的，但它不是不可能的，大多需要一些舊的東西翻新，以適應新的概念。由於使用靜態網頁進行HTML瀏覽現在有點舊，所以到目前爲止它並沒有得到最高優先級。例如，在任何情況下，Isabelle/Scala（官方Isabelle系統編程接口）都已經提供了一些公共API操作，以便從您在Isabelle/jEdit中在線看到的PIDE文檔標記中獲取XML樹。從那裏開始，對於理解業務的人來說，它對於一些HTML + CSS來說並不是很遠。不過，在Isabelle/jEdit中進行一些演示，可能會更快更有用，從而繞過大量Web瀏覽器及其怪癖。