*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Proof failed in HOL? (build with -o browser_info fails)*From*: Peter Lammich <lammich at in.tum.de>*Date*: Tue, 17 Dec 2013 23:14:22 +0100*In-reply-to*: <op.w786wzvhule2fv@cardamome>*References*: <op.w786wzvhule2fv@cardamome>

The "PROOF FAILED for depth n" looks like some harmless tracing output of some tactic to me. The reason why your build fails seems to be >### /home/yannick/apps/isabelle/lib/Tools/browser: ligne 96: epstopdf > : commande introuvable > ### Failed to produce pdf output > *** Failed to prepare dependency graph > It does not find epstopdf on your system, and thus document generation fails. -- Peter On Di, 2013-12-17 at 21:23 +0100, Yannick Duchêne (Hibou57) wrote: > 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. >

**References**:**[isabelle] Proof failed in HOL? (build with -o browser_info fails)***From:*Yannick Duchêne (Hibou57)

- Previous by Date: [isabelle] Proof failed in HOL? (build with -o browser_info fails)
- Next by Date: [isabelle] [Fwd: F-IDE 2014]
- Previous by Thread: [isabelle] Proof failed in HOL? (build with -o browser_info fails)
- Next by Thread: [isabelle] [Fwd: F-IDE 2014]
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list