Re: [isabelle] Theory Dependencies

On Wed, 13 Apr 2011, Christian Sternagel wrote:

As you see, there are no real dependencies in the target (except the ML file). So whenever I call 'isabelle make' it is only built when it does not already exist (which means that I have to manually remove it whenever I have to rebuild). It would be more convenient if all the necessary dependencies could be integrated into the IsaMakefile automatically.

This redundant approximation of dependencies in make files is indeed very cumbersome (and fragile). We are moving towards Isabelle builds without make for many years, and last winter I have made again some progress to work towards that. (Surprisingly many strange details had accumulated in the existing collection of IsaMakefiles, including AFP.)

The main obstacles have already been removed shortly after Isabelle2011, so direct Isabelle dependency management can become a reality pretty soon.

Hence my question, is there an established way of finding the (transitive) theory dependencies of a given thy/ML-file? If not, what are the relevant Isabelle/ML-functions?

There is still no official way.


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