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 OS

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
 command:

 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
http://isabelle.in.tum.de/website-Isabelle2019-RC3 -- 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.

Thanks.

--
Adnan



	Makarius


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