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
