Re: [isabelle] RC3: new installation isn't interested in building target, only dependencies?

On 02/11/2013 06:07 PM, Rafal Kolanski wrote:
I am assuming that the intended semantics for the "isabelle build"
command is to actually build the specified target.
I was told that it is not ;)

You have to explicitly give the "-b" flag for building, i.e.,

isabelle build -b HOL

If I remember correctly, by default all images are built into your ~/.isabelle/<Isabelle-version>/heaps directory.

In case there are "previous" heap images that have to be build in order to run the current target, they will be built even without the "-b" flag, i.e.,

isabelle build HOL-Word

builds everything up to HOL-Word (i.e., Pure and HOL). At first this sounds strange, but I found the build tool as is, very usable and convenient.

Also, when using jedit, it is enough to start it, e.g., by

isabelle jedit -l HOL-Word

and all necessary builds are done automatically (including HOL-Word).

(an aside: this is based on the new "isabelle build_dialog")

hope this helps


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