Re: [isabelle] Problems Generating HOL-Analysis Manual in Mac OS

------ Original Message ------
From: "Makarius" <makarius at>
To: rashid at; cl-isabelle-users at
Sent: 25-May-19 7:37:58 PM
Subject: Re: [isabelle] Problems Generating HOL-Analysis Manual in Mac OS

On 22/05/2019 16:57, rashid at wrote:

 I am trying to generate the manual for HOL-Analysis by using the following

 Isabelle build -b -v -o document=pdf HOL-Analysis

 However, it ends up with the following message and does not create any pdf.

 Session Pure/Pure
 Session HOL/HOL (main)
 Session HOL/HOL-Library (main timing)
 Session HOL/HOL-Computational_Algebra (main timing)
 Session HOL/HOL-Analysis (main timing)

 Finished at Thu May 16 13:27:18 GMT+2 2019
 0:00:03 elapsed time

(Option "-b" is not required for document preparation.)

You should make double-sure that there are no remaining build artefacts
for session HOL-Analysis in $ISABELLE_HOME_USER/heaps and especially in
$ISABELLE_HOME/heaps (e.g. as result of switching Isabelle/jEdit to
HOL-Analysis and letting it build its own logic image).

One way to do this is to try with a fresh download of -- every named
Isabelle version has its own storage for heaps.
I was having same issue, even with the fresh download of Isabelle2019-RC3.

Another way is to use "isabelle getenv ISABELLE_HOME_USER ISABELLE_HOME"
to figure out these particular directory locations and "rm -rf" their
"heaps" sub-directories manually.
However, deleting "heaps" sub-directories manually, really solved the problem and the HOL-Analysis manual has been created successfully.




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