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
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