Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 22 2022 at 19:41):

From: rashid@in.tum.de
Hi all,

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

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

Actually it should end up with generating a pdf at:

.../browser_info/HOL/HOL-Analysis/manual.pdf

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

ML_PLATFORM="x86-darwin"
ML_HOME="/Applications/Isabelle2018.app/Contents/Resources/Isabelle2018/cont
rib/polyml-5.7.1-8/x86-darwin"
ML_SYSTEM="polyml-5.7.1"
ML_OPTIONS="--minheap 500"

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

I also tried cleaning all sessions without building anything using "isabelle
build -a -n -c". However, it is not working as well.

I am using MacBook Pro (macOS Mojave Version 10.14.4) and I checked it on
Isabelle 2018 and Isabelle 2019-RC2.

Any idea how to resolve this problem?

view this post on Zulip Email Gateway (Aug 22 2022 at 19:43):

From: Makarius <makarius@sketis.net>
(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.

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.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 19:44):

From: "rashid@in.tum.de" <rashid@in.tum.de>
------ Original Message ------
From: "Makarius" <makarius@sketis.net>
To: rashid@in.tum.de; cl-isabelle-users@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@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.

Last updated: Apr 19 2024 at 16:20 UTC