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
Re: [isabelle-dev] Vampire
Makarius wrote: > I don't remember the reason for its "tristate logic", with "unknown" as > default. The thinking is as follows. In an "unknown" state, "vampire" gets added to the list of provers by Sledgehammer, and users get a warning. In a "no" state, it doesn't. Thus, "unknown" serves a documentational purpose. If the default were "no" instead, many noncommercial users would likely fail to enable Vampire. I'm not married to the above scheme, but the years of experience with it and Z3 (until Z3 was open-sourced) suggest that it works well. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Vampire
On 04/07/18 12:11, Blanchette, J.C. wrote: > > I just copied old code I inherited from Sascha Böhm and his Vampire > noncommercial. I only vaguely remember when we introduced the original non-commercial settings variable for Z3, even with some insider joke about Microsoft: changing the value required a reboot of the Isabelle application. Later it became a system option for change at run-time, not boot-time. I don't remember the reason for its "tristate logic", with "unknown" as default. If you make it a plain bool with false as default, users can just click on a checkbox in Isabelle/jEdit Plugin options. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Vampire
On 04/07/18 12:18, Lawrence Paulson wrote: > Well, there’s this: > >> String.translate (fn c => if Char.isSpace c then "" else str c) " y e s >> "; > val it = "yes": string > > No idea what Isabelle/ML does to these primitives however. This SML'97 stuff is indeed alien to Isabelle/ML, and semantically wrong. The canonical operations always operate on Isabelle symbols, e.g. see Symbol.trim_blanks. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Vampire
Well, there’s this: > String.translate (fn c => if Char.isSpace c then "" else str c) " y e s > "; val it = "yes": string No idea what Isabelle/ML does to these primitives however. Larry > On 4 Jul 2018, at 11:11, Blanchette, J.C. wrote: > > I just copied old code I inherited from Sascha Böhm and his Vampire > noncommercial. For sure there are endlessly many ways in which we could make > Isabelle and Sledgehammer more user friendly. In Qt/C++, we had a > "stripWhiteSpace" function that would do the trick. But string manipulation > in ML is like pulling teeth. If you happen to know which function I can call, > I'll gladly change the code. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Vampire
> I’m at home today so don’t have access to that file. Please send it to me once you have a chance. > But even if I somehow misspelt “yes” five times, But maybe you wrote "true" five times? > would it revert to “unknown”? Any value other than "yes" and "no" is taken as "unknown". > Of course spaces should be ignored, esp. at the end. I just copied old code I inherited from Sascha Böhm and his Vampire noncommercial. For sure there are endlessly many ways in which we could make Isabelle and Sledgehammer more user friendly. In Qt/C++, we had a "stripWhiteSpace" function that would do the trick. But string manipulation in ML is like pulling teeth. If you happen to know which function I can call, I'll gladly change the code. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Vampire
> On 3 Jul 2018, at 13:07, Lawrence Paulson wrote: > > I keep getting the error message below. I have changed this option many times > but it never sticks. It has been happening consistently since yesterday. > > ~/isabelle/Repos/src/HOL: hg id > ec4fe1032b6e tip Could it be something as simple as a typo or a spurious space? The only recognized values are "yes" and "no" (upper- or lowercase). What happens if you change the option to "no"? What happens if you change it back to "yes"? Could you send me the contents of your file "~/.isabelle/etc/preferences"? Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Vampire
I keep getting the error message below. I have changed this option many times but it never sticks. It has been happening consistently since yesterday. ~/isabelle/Repos/src/HOL: hg id ec4fe1032b6e tip Larry "vampire": Error: The Vampire prover is not activated; to activate it, set the Isabelle system option "vampire_noncommercial" to "yes" (e.g. via the Isabelle/jEdit menu Plugin Options / Isabelle / General) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
