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



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.
> 






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