Email Gateway (Aug 19 2022 at 13:03): Email Gateway (Aug 19 2022 at 13:03):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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.
Email Gateway (Aug 19 2022 at 13:03):From: Peter Lammich <lammich@in.tum.de>
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
Last updated: Apr 25 2024 at 08:20 UTC