Re: [isabelle-dev] NEWS: activation of Z3 via z3_non_commercial system option
On Mon, 13 Jan 2014, Lawrence Paulson wrote: I get an error here: ~/isabelle/Repos/src/HOL: isabelle components -a ### Missing Isabelle component: /Users/lp15/.isabelle/contrib/z3-3.2-1 Getting http://isabelle.in.tum.de/components/z3-3.2-1.tar.gz; Can't locate LWP/Simple.pm in @INC (@INC contains: /opt/local/lib/perl5/site_perl/5.12.4/darwin-thread-multi-2level /opt/local/lib/perl5/site_perl/5.12.4 /opt/local/lib/perl5/vendor_perl/5.12.4/darwin-thread-multi-2level /opt/local/lib/perl5/vendor_perl/5.12.4 /opt/local/lib/perl5/5.12.4/darwin-thread-multi-2level /opt/local/lib/perl5/5.12.4 /opt/local/lib/perl5/site_perl /opt/local/lib/perl5/vendor_perl .). BEGIN failed--compilation aborted. ~/isabelle/Repos/src/HOL: The regular /usr/bin/perl by Apple already provides the critial libwww, which is required here (as well as for remote Sledgehammer scripts). Perl from /opt/local probably comes in via MacPorts, and thus introduces the usual uncertainties of such package repositories. If you want to keep that version of perl, you need to saturate its installation. Via sudo port list, I guess that something like p5-libwww-perl should do it. Are you actually using the Isabelle.app wrapper from Isabelle2013-2? It retains the original Apple PATH, and thus uses /usr/bin/perl even with that MacPorts Perl present. That might explain, why remote sledgehammer works, but isabelle components -a with its different PATH didn't. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
On Tue, 14 Jan 2014, Thomas Sewell wrote: This is also a patch against Isabelle2013-1. Is that just a typo, or are you still using that failed release? The current one is Isabelle2013-2, and it does not introduce any incompatibilities over Isabelle2013-1, so there is no reason to keep using that. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
On Tue, 14 Jan 2014, Thomas Sewell wrote: If there is some collection of proofs that are especially bad, we can just declare [[ hypsubst_thin = true ]] Larry, you are the original author of hypsubst. Does the hypsubst_thin terminology make sense to you? It is used here both for the configuration option and its attribute, and the alternate proof method that has it already enabled. For me it does make sense, i.e. we don't need to make it explicitly legacy in the wording. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
The name makes sense: thin refers to deleting the assumption. It is ugly of course, which will be an incentive for users to update their proofs. Larry On 15 Jan 2014, at 15:05, Makarius makar...@sketis.net wrote: On Tue, 14 Jan 2014, Thomas Sewell wrote: If there is some collection of proofs that are especially bad, we can just declare [[ hypsubst_thin = true ]] Larry, you are the original author of hypsubst. Does the hypsubst_thin terminology make sense to you? It is used here both for the configuration option and its attribute, and the alternate proof method that has it already enabled. For me it does make sense, i.e. we don't need to make it explicitly legacy in the wording. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: newline in HOL char or string literals
* The symbol \newline may be used within char or string literals to represent (Char Nibble0 NibbleA), i.e. ASCII newline. This refers to Isabelle/e33c5bd729ff, which also introduces a unicode glyph for that. It is a continuation of the isabelle-users thread: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-August/004457.html by Christian Sternagel. As usual there is the difference of what one wants vs. needs vs. can have. The \newline symbol is easy to have, and it is sufficient for the applications in IsaForR, after studying the sources a bit. So that is needed here. Classic C notation \n is not easy to have, and not needed. Tab \t and CR \r were mentioned in the old thread as well. These are evil characters, but they might occur in some formal model in HOL nonetheless. I did not find any convenient unicode glyphs, though. Moreover, Isabelle symbols cannot distinguish \n vs. \r vs. \r\n, otherwise Windows files cannot be processed properly; jEdit incidently does the very same collapse of line endings. So in exotic applications of HOL where strange whitespace characters are needed, explicit (Char NibbleX NibbleY) will do the job as before. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
Whoops. It's both a typo and use of the wrong release. The patch happens to work against Isabelle2013-1 or Isabelle2013-2, since there are no relevant differences in the theory sources. I can confirm that isabelle build -a works in either 2013-1 or 2013-2. Short version of the story, I forgot the name of the newest release. Long version: The confusion was caused in part because the newest l4.verified branch is called '2013-1'. It contains Isabelle 2013-2, but the switch was accomplished so straightforwardly that we didn't end up with a new branch name. Apologies about the confusion, Thomas. On 16/01/14 02:00, Makarius wrote: On Tue, 14 Jan 2014, Thomas Sewell wrote: This is also a patch against Isabelle2013-1. Is that just a typo, or are you still using that failed release? The current one is Isabelle2013-2, and it does not introduce any incompatibilities over Isabelle2013-1, so there is no reason to keep using that. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
