Re: [isabelle-dev] testboard
On Wed, 19 Aug 2015, Larry Paulson wrote: I pushed a changeset to the testboard, but it isn’t showing up at http://isabelle.in.tum.de/testboard/Isabelle The last change it shows was 6 days ago. Moreover, testboard and the default branch look identical (I’m using SourceTree), so have I simultaneously pushed my changes to the main repository somehow? Maybe. The changeset 6a6f15d8fbc4 turned out broken -- I've repaired this already in e1159bd15982. Generally, we are running short of proper test machines -- isatest takes very long now. The fastest machine in reach is the one under my desk. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] testboard
I pushed a changeset to the testboard, but it isn’t showing up at http://isabelle.in.tum.de/testboard/Isabelle The last change it shows was 6 days ago. Moreover, testboard and the default branch look identical (I’m using SourceTree), so have I simultaneously pushed my changes to the main repository somehow? Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] "The following files are required to resolve theory imports"
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 fundamentally. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] "The following files are required to resolve theory imports"
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. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
