Re: [isabelle] Error: No rule to make target `HOL.thy`



> 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



On 6/21/2012 3:15 PM, gottfried.barrow at gmx.com wrote:
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











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