Re: [isabelle-dev] Deadlock while building HOL-Proof
On 10/05/18 00:10, Makarius wrote: > On 10/03/18 11:06, Makarius wrote: >> On 08/03/18 13:08, Makarius wrote: >>> Since David Matthews has make a lot of changes concerning fine-points of heap management in the past few months, I would like to test it with some Poly/ML repository version. But this does not build on macOS at the moment. >>> >>> I will continue with the investigations here. >> >> I have now tested it with various experimental versions of Poly/ML: the >> problem persists. >> >> Looking more closely at the ML statistics of the process (after killing >> it) reveals that the ML world is fine and active, only my future thread >> farm is somehow blocked. >> >> This indicates that the problem is in my area of responsibility. > > In the past couple of weeks I have sporadically tried to work around > this resource problem, but failed so far. > > The latest attempt is Isabelle/f6a22490cca8. As usual, it "works for me > on my usual test machines", but there is a remaining chance of problems > coming back on other configurations. > > > Overall, my guess is that the Poly/ML parallel GC vs. Isabelle/ML future > thread management somehow get into trouble, due to massive resource > requirements in parallel HOL-Proofs with a sudden spike of approx. 5 > futures that require a lot of memory. Even x86_64 does not really help. > > In a sense, it is just the normal situation "invisible concrete wall > ahead" -- we've that had occasionally in the past 10-20 years. It is a > reminder that scaling is not for free, but explicit efforts are required > for it. This thread is still open, but there are some new observations in the background, related to changeset afa7c5a239e6 at its FIXME comment. I will take at least one deep look at it again before the Isabelle2018 release, potentially also David Matthews. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Vampire
On 06/07/18 17:36, Tobias Nipkow wrote: > > On 06/07/2018 17:20, Lawrence Paulson wrote: >>> On 4 Jul 2018, at 11:11, Blanchette, J.C. wrote: >>> I’m at home today so don’t have access to that file. >>> >>> Please send it to me once you have a chance. >> >> It seems that I did finally succeed in getting the option set. My >> guess is that the Mac app doesn't necessarily save settings, depending >> on whether you exit with Isabelle > Quit Isabelle or File > Exit. And >> I’m not sure which one of these is supposed to work. > > I have stopped using Isabelle > Quit Isabelle (cmd-Q) because it does > not ask you if you want to save modified files; it doesn't save them but > creates autosave files. Quite possibly it does not save settings either. You merely need to make sure that the MacOSX plugin is enabled. For repository versions it is off by default, because the underlying platform is not known. For official Isabelle applications (e.g. release versions) the plugin is on by default. The "jedit" manual includes this general explanation: The bundled ∗‹MacOSX› plugin provides various functions that are expected from applications on that particular platform: quit from menu or dock, preferences menu, drag-and-drop of text files on the application, full-screen mode for main editor windows. It is advisable to have the ∗‹MacOSX› plugin enabled all the time on that platform. Moreover note that we have public mailing lists: isabelle-dev for repository versions and isabelle-users for releases and release candidates. I still consider these as canonical channels for open communication, where it is possible to discuss arbitrary problems, in order to get them sorted out eventually (even if this takes years), but keeping problems secret means they cannot be solved. In the past 10 years we have reached very high quality standards, and I have no inclination to let this decay for no particular reasons. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Vampire
On 06/07/2018 17:20, Lawrence Paulson wrote: On 4 Jul 2018, at 11:11, Blanchette, J.C. wrote: I’m at home today so don’t have access to that file. Please send it to me once you have a chance. It seems that I did finally succeed in getting the option set. My guess is that the Mac app doesn't necessarily save settings, depending on whether you exit with Isabelle > Quit Isabelle or File > Exit. And I’m not sure which one of these is supposed to work. I have stopped using Isabelle > Quit Isabelle (cmd-Q) because it does not ask you if you want to save modified files; it doesn't save them but creates autosave files. Quite possibly it does not save settings either. Tobias But even if I somehow misspelt “yes” five times, But maybe you wrote "true" five times? certainly not. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Vampire
> On 4 Jul 2018, at 11:11, Blanchette, J.C. wrote: > >> I’m at home today so don’t have access to that file. > > Please send it to me once you have a chance. It seems that I did finally succeed in getting the option set. My guess is that the Mac app doesn't necessarily save settings, depending on whether you exit with Isabelle > Quit Isabelle or File > Exit. And I’m not sure which one of these is supposed to work. > But even if I somehow misspelt “yes” five times, > > But maybe you wrote "true" five times? certainly not. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
