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.

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




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