Re: [isabelle] Problems Generating HOL-Analysis Manual in Mac OS
------ Original Message ------
From: "Makarius" <makarius at sketis.net>
To: rashid at in.tum.de; cl-isabelle-users at lists.cam.ac.uk
Sent: 25-May-19 7:37:58 PM
Subject: Re: [isabelle] Problems Generating HOL-Analysis Manual in Mac
I was having same issue, even with the fresh download of
On 22/05/2019 16:57, rashid at in.tum.de 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 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
http://isabelle.in.tum.de/website-Isabelle2019-RC3 -- every named
Isabelle version has its own storage for heaps.
However, deleting "heaps" sub-directories manually, really solved the
problem and the HOL-Analysis manual has been created successfully.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and