Re: [isabelle] Isabelle 2012 on Win7



Le Sat, 04 Aug 2012 18:01:59 +0200, Jens Doll <jd at cococo.de> a écrit:

Hello all,

I now have a CygWin installation with the Isabelle2012 directory copied
to it's root.
Then I called 'isabelle mkdir MyTheo' and found the directory MyTheo
(somewhere).
Afterwards I created a simple theory myth.thy in that directory and
tried to build it by calling 'isabelle make'.
I got a message of a missing Isamake file.

My two questions are:

a) Why is the makefile needed?
b) Which is the most simple makefile here?

Jens

Hi Jens, and welcome home :)

Just an hypothesis: are you sure you ran the “isabelle make” command from within the same directory as the one you use to run the “isabelle mkdir” command?

Say you invoke “isabelle mkdir MySession” from “~/foo”, then it will create a directory “~/foo/MySession”, will populate it, and will create the makefile as “~/foo/Isamake”, so you have to run “isabelle make” from inside of “~/foo”, not from inside of “~/foo/MySession”.

Can you check this prior to anything else?

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University






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