[isabelle] Theory Dependencies



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





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