Email Gateway (Aug 18 2022 at 20:10): Email Gateway (Aug 18 2022 at 20:10):From: gottfried.barrow@gmx.com
Hi,
Using Isabelle2011-1, I do this and it creates the heap and browser_info
for HOL in my ~/.isabelle/Isabelle2011-1
cd /cygdrive/e/Isabelle2011-1/src/HOL
isabelle make
I do the same for Isabelle2012, and I get the error shown:
cd /cygdrive/e/Isabelle2012/src/HOL
isabelle make
make[1]: Entering directory /cycgdrive/e/Isabelle2012/src/Pure'
make[1]: Nothing to be done for Pure.
make[1]: Leaving directory /cycgdrive/e/Isabelle2012/src/Pure'
make. *** No rule to make target HOL.thy, needed by `cygdrive/e
/E_main/home/.isabelle/Isabelle2012/heaps/polyml-5.4.1_x86-cygwin
/HOL'. Stop.
I also get the same error if I try to do ./build in $ISABELLE_HOME.
However, I can build sessions with usedir like this:
cd /cygdrive/e/Isabelle2012/src/HOL/Lattice
isabelle usedir -b HOL Lattice
For both Isabelle2011-1 and Isabelle2012 I have the following set:
ISABELLE_USEDIR_OPTIONS="-i true -g true -M max -p 1 -q 2 -v true -V
outline=/proof,/ML"
Regards,
GB
Email Gateway (Aug 18 2022 at 20:14):From: Gottfried Barrow <gottfried.barrow@gmx.com>
make. *** No rule to make target
HOL.thy, needed by `cygdrive/e
/E_main/home/.isabelle/Isabelle2012/heaps/polyml-5.4.1_x86-cygwin
/HOL'. Stop.
Uh, that's because in trying to copy HOL.thy some number of days back, I
moved it, so it was missing from ~/src/HOL. I guess usedir worked
because it uses the already built heap for HOL. With the file there, it
builds and makes like it's supposed to.
--GB
Last updated: Apr 25 2024 at 08:20 UTC