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



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.