[isabelle-dev] "The following files are required to resolve theory imports"
makarius at sketis.net
Wed Aug 19 15:45:06 CEST 2015
On Wed, 19 Aug 2015, Larry Paulson wrote:
> I frequently look at finished theories when looking for useful theorems.
> But I’ve noticed a new and undesirable behaviour: I get the message "The
> following files are required to resolve theory imports” even though the
> theory is finished, and presumably has already been imported. Dismiss
> the message, and it re-appears at least once more.
This is part of ongoing reforms about management of ML source files -- the
option is called jedit_auto_resolve, and in d94f3afd69b6 I've just changed
the default to give more time to rethink it.
The reason why it came up right now is the new ML debugger IDE (which
requires a recent repository version of Poly/ML). Once that is stablized,
I will announce it here for public exposure and more serious testing. It
has the potential to change the way we work with Isabelle/ML development
More information about the isabelle-dev