Email Gateway (Aug 18 2022 at 17:34): Email Gateway (Aug 18 2022 at 17:34):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi all,
A typical target in an IsaMakefile is something like:
$(ISABELLE_OUTPUT)/$(HEAP): HEAP.ML
$(ISABELLE_TOOL) usedir -b -f HEAP.ML HOL $(HEAP)
In our project the main target of this shape takes approximately 30 min
to build. Hence, I really do not want to rebuild it if not necessary. 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. 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?
A nice feature would be 'isabelle dependencies <files>', for use inside
an IsaMakefile.
cheers
chris
Email Gateway (Aug 18 2022 at 17:34):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC