[isabelle] Proof failed in HOL? (build with -o browser_info fails)



Hi proof authors,

I wanted to generate HTML files for HOL and HOL-BNF, and both fails with this message:

    HOL FAILED
(see also /home/yannick/.isabelle/Isabelle2013-2/heaps/polyml-5.5.1_x86-linux/log/HOL)

    ### (!!x. ?f x = ?g x) ==> ?f = ?g
    ### Rule already declared as introduction (intro)
    ### (!!x y. ?A x y ==> ?B (?f x) (?g y)) ==> (?A ===> ?B) ?f ?g
    ### Ignoring conversion rule for operator Orderings.bot_class.bot
    val it = fn: theory -> theory

    val it = "Num.neg_numeral_class.neg_numeral": string

    ### Ignoring duplicate rewrite rule:
    ### nat (numeral ?k1) == numeral ?k1
    PROOF FAILED for depth 2
    PROOF FAILED for depth 2
    PROOF FAILED for depth 3
    PROOF FAILED for depth 3
    PROOF FAILED for depth 3
    PROOF FAILED for depth 3
    PROOF FAILED for depth 4
### /home/yannick/apps/isabelle/lib/Tools/browser: ligne 96: epstopdf : commande introuvable
    ### Failed to produce pdf output
    *** Failed to prepare dependency graph
    HOL-Cardinals-Base CANCELLED
    HOL-Cardinals CANCELLED
    HOL-BNF CANCELLED
    Unfinished session(s): HOL, HOL-BNF, HOL-Cardinals, HOL-Cardinals-Base


Why does it says “PROOF FAILED”? I have not altered any theory files.

If ever that matter, here is the exact command I used:

    isabelle build -o browser_info -o document=pdf -v -c HOL-BNF

Doing the same for FOL is OK.

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.