Re: [isabelle] Error: No rule to make target `HOL.thy`
> make. *** No rule to make target `HOL.thy`, needed by `cygdrive/e
> /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.
On 6/21/2012 3:15 PM, gottfried.barrow at gmx.com wrote:
Using Isabelle2011-1, I do this and it creates the heap and browser_info
for HOL in my ~/.isabelle/Isabelle2011-1
I do the same for Isabelle2012, and I get the error shown:
make: Entering directory `/cycgdrive/e/Isabelle2012/src/Pure'
make: Nothing to be done for `Pure`.
make: Leaving directory `/cycgdrive/e/Isabelle2012/src/Pure'
make. *** No rule to make target `HOL.thy`, needed by `cygdrive/e
I also get the same error if I try to do ./build in $ISABELLE_HOME.
However, I can build sessions with usedir like this:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and