[isabelle-dev] Isabelle on Cygwin
Hi, Is anyone using Isabelle on Cygwin and has build an image for a recent Isabelle changeset? Or is Isabelle regularly build under Cygwin on any of the test machines? I've installed Cygwin from scratch two days ago and downloaded Isabelle (hg id 5b889b1b465b). When building Pure, the PolyML process seems to hang at the end of building the image. The process does not use any further CPU resources and does not terminate. The Pure image seems to be build successfully, but the corresponding log file is missing. It might well be that this is a problem with my computer configuration. Could anyone please try to build this Isabelle changeset (or a closely related one) on Cygwin and report the outcome? Thanks, Sascha ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP: Session AVL-Trees broken
Sascha Boehme boeh...@in.tum.de wrote: Hi, Zitat von Ond?ej Kun?ar kun...@in.tum.de: But AVL-Trees were already broken in Isabelle's changeset 791157a4179a (ensured that rewr_conv rule t = t == u literally not just modulo beta-eta) before Jasmin's changeset 34b0464d7eef. It seems that the changeset fixing rewr_conv interacts with smt. There is a goal which is the same goal before and after the change - the term is really the same; no tricks like the pretty-printer does beta-reduction. And smt fails only after the change and it doesn't matter if the pregenerated certificates are used. Somebody who understands smt should take a look at how much the changeset with rewr_conv is harmful to smt. I do have an idea what might go wrong. I'll need to investigate it further before committing a patch. I found the explanation for the problem. It is indeed related to Tobias's change in rewr_conv. The normalization code in the smt method rewrites arithmetic constants (e.g. max) by replacing them with lambda abstractions (e.g. %a b. if a b then a else b) and not beta-reducing the resulting terms. In a later step a conversion goes through the terms and does further rewritings. Before Tobias' change, one sub-conversion (a rewr_conv) in that process returns a beta-reduced equation (reducing one of the above lambda abstractions), and hence the left-hand side does not match anymore the term given to the conversion. This causes an exception to be thrown by then_con. Nevertheless, a surrounding conversion catches that exception and tries something else resulting in a term that by accident looked as expected. Now, after Tobias' change, the inner rewr_conv returns an equation with unmodified left-hand side. The outer conversion that previously catched the exception does not kick in and the result is something different (and not what one would have expected). Summa summarum, there is something severly broken in the normalization code of the smt method, and Tobias' change of rewr_conv helped to discover this flaw. This indicates that the changed rewr_conv behaves in a way that causes fewer surprises for users and as such was an improvement to the code. I'll fix the normalization of the smt method. Cheers, Sascha ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Status of HOL/SMT
Hi, I spent a couple of hours on this issue. Some odd things are going on during normalization of goals in the smt method. I have the feeling that normalization somehow (accidentally?) worked before Tobias' change on rewr_conv, but that it should really be implemented in a different, more stable way. I'll need a bit more time. Everything should be fixed by the end of the year. Cheers, Sascha - Ursprüngliche Nachricht - Von: Jasmin Christian Blanchette Gesendet: 04.12.2012 15:07 An: Makarius Cc: isabelle-dev Mailinglist; Sascha Boehme Betreff: Re: [isabelle-dev] Status of HOL/SMT Am 04.12.2012 um 14:52 schrieb Jasmin Christian Blanchette: The real issue, at the end of the day, seems to be not so much Z3 4.0 in itself but rather the fact that our code often can't parse them. I've looked into this and saw no quick fix [*]. Oh, Tobias just reminded me that a second issue is the rewr_conv change. See Ondra's and Sascha's emails on November 9. If there's no quick resolution on that front, I would suggest simply introducing rewr_conv_old in the SMT source code and using that. Sascha, any progress on that front? Last time you wrote I do have an idea what might go wrong. I'll need to investigate it further before committing a patch. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP: Session AVL-Trees broken
Hi, Zitat von Ond?ej Kun?ar kun...@in.tum.de: But AVL-Trees were already broken in Isabelle's changeset 791157a4179a (ensured that rewr_conv rule t = t == u literally not just modulo beta-eta) before Jasmin's changeset 34b0464d7eef. It seems that the changeset fixing rewr_conv interacts with smt. There is a goal which is the same goal before and after the change - the term is really the same; no tricks like the pretty-printer does beta-reduction. And smt fails only after the change and it doesn't matter if the pregenerated certificates are used. Somebody who understands smt should take a look at how much the changeset with rewr_conv is harmful to smt. I do have an idea what might go wrong. I'll need to investigate it further before committing a patch. Cheers, Sascha ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS
The SMT solver Z3 has now by default a restricted set of directly supported features. For the full set of features (div/mod, nonlinear arithmetic, datatypes/records) with potential proof reconstruction failures, enable the configuration option z3_with_extensions. Minor INCOMPATIBILITY. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jar: command not found
Hi, When the JDK is not given in the PATH variable, the command isabelle jedit may fail with ./build-jars: line 189: jar: command not found This is at least the case for hg id 08c22e8ffe70. The problem occurs with Cygwin where the JDK is provided as a component in the Isabelle bundle and is hence typically not mentioned in the PATH. Proper prefixing of invocations of jar with the JDK's path might solve this issue. Cheers, Sascha ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] smt for word
Hi Gerwin, This is because by default the smt method tries to reconstruct the proof of Z3. For bitvectors, however, there is currently no Z3 proof reconstruction. You might want to invoke the smt method as an oracle: lemma (x :: 8 word) + x = 2 * x using [[smt_oracle]] by smt Cheers, Sascha Gerwin Klein wrote: I'm getting lemma (x :: 8 word) + x = 2 * x apply smt Solver z3: Z3 proof parser (line 2): unknown sort: bv I was trying remote Z3 from a Mac. This is on isabelle 20b3377b08d7, but I don't think anything relevant has changed since Sep 26. Am I doing something wrong? Sounds like Z3 responds with something the smt method doesn't know about. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] comparison of bindings
Hi, Given to bindings (i.e., instances of Binding.binding), how are they supposed to be compared? Here is a more concrete example. Assume there is a declaration such as: declare_foo name = ... which declares name as some new foo-entity. For later reference, the declared foo-entities are best stored in a table internally, associated with the declaration data (the omitted right-hand side above). Indexing this table with the binding produced from name is not possible, as bindings cannot be compared with each other. Using Binding.print to turn a binding into a string (and using Symtab.table) doesn't seem to be the right approach (Binding.print is probably not meant for this purpose). What should be used instead? Thanks, Sascha ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Mirabelle and load path
Alexander Krauss wrote: On 03/22/2011 10:17 PM, Makarius wrote: I also wonder about mirabelle -q, which produces strange messages in the regular makeall setup: http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Mirabelle/lib/scripts/mirabelle.pl#l134 http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Mirabelle/lib/scripts/mirabelle.pl#l139 Is this really intended, or just due to the confusing ne test? Changeset d3404f32328a silences these two lines. I'm not quite sure whether they are necessary at all, but they might come in handy when running Mirabelle with several theories. Sascha ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Application for Google Summer of Code 2011
Hi, We are in the process of applying as a mentoring organization for this year's Google Summer of Code (SoC). Some 150 open-source organizations and some thousand students take part in SoC every year -- and Google announced to accept more organizations this year. http://socghop.appspot.com/gsoc/program/home/google/gsoc2011 Participating in SoC requires to propose projects which have the potential to attract students from all over the world (students interested in Isabelle might also suggest their own projects). Each project will also need a mentor which supports the student during Soc (from mid of May until mid of August). We are looking for project ideas related to Isabelle, and will collect them on a website: http://isabelle.in.tum.de/gsoc_ideas.html Please consider sending ideas to us which are attractive and could be accomplished by interested students essentially within three months (but continuing these projects after the end of SoC is encouraged both by Google and by us). We need at least the following information for each project idea: * a title * a mentor (with contact information) * a brief description (one/two paragraphs) * a list of technologies required by the student The SoC application deadline is this Friday, 12:00 UTC. We would like to have collected most of the ideas by then, but more ideas could be added afterwards as well. Looking forward to your project ideas, Sascha Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Application for Google Summer of Code 2011
The website for the project ideas is actually (note the hyphen instead of the underscore): http://isabelle.in.tum.de/gsoc-ideas.html Thanks to Christian Sternagel for reporting this. Please don't hesitate to submit project ideas, Jasmin Sascha Sascha Boehme wrote: Hi, We are in the process of applying as a mentoring organization for this year's Google Summer of Code (SoC). Some 150 open-source organizations and some thousand students take part in SoC every year -- and Google announced to accept more organizations this year. http://socghop.appspot.com/gsoc/program/home/google/gsoc2011 Participating in SoC requires to propose projects which have the potential to attract students from all over the world (students interested in Isabelle might also suggest their own projects). Each project will also need a mentor which supports the student during Soc (from mid of May until mid of August). We are looking for project ideas related to Isabelle, and will collect them on a website: http://isabelle.in.tum.de/gsoc_ideas.html Please consider sending ideas to us which are attractive and could be accomplished by interested students essentially within three months (but continuing these projects after the end of SoC is encouraged both by Google and by us). We need at least the following information for each project idea: * a title * a mentor (with contact information) * a brief description (one/two paragraphs) * a list of technologies required by the student The SoC application deadline is this Friday, 12:00 UTC. We would like to have collected most of the ideas by then, but more ideas could be added afterwards as well. Looking forward to your project ideas, Sascha Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Google Summer of Code 2011
Hi, Until March 11, Google is looking for mentoring organization for this year's Summer of Code, a two-month period where students from all over the world improve open source software/projects. http://socghop.appspot.com/gsoc/program/home/google/gsoc2011 We might participate as project -- and at the same time spread the word of interactive theorem provers -- if we have some suggestions for student tasks (I think about jEdit-related components, especially). Please let me know and we can discuss the details in private e-mail. Cheers, Sascha ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] SMT solvers at the TUM server
Hi, To all of you who already copied the SMT solvers (CVC3, Yices, or Z3) from the TUM server: Please copy the files again, as I have just updated them in connection with changeset fda8511006f9. Sorry for the inconvenience. Sascha ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] SMT components and environment variables
Hi, With changeset 3214c39777ab, the SMT solvers have been turned into components. As a consequence, the now obsolete environment variables (in settings files) CVC3_SOLVER, YICES_SOLVER, and Z3_SOLVER should be removed. This only applies if you have used the smt method so before. Prior to their usage, SMT solvers need to be added to the components list -- more precisely, the paths to SMT solver bundles need to be added to $ISABELLE_HOME_USER/etc/components. SMT solver bundles can be found at TU Muenchen servers in the directories ~isabelle/cvc3 (without support for Darwin-based systems for now, this will be fixed within the next days) and ~isabelle/z3. Note the provided LICENSE files (e.g., Z3 is restricted for non-commercial usage only). The reward for this rather clumsy setup is a more powerful sledgehammer command. Sascha ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
SMT's timeout option is also measured in seconds, and this is the case since its beginning. I found this a natural decision, and no one has ever objected to it. Sascha Tobias Nipkow wrote: Unless I have a lapse of memory, the timeout specifications for s/h and Nitpick are also in seconds, possibly with an s appended. As a user I am glad about that, because I do not think in ms and would not like to write 3 instead of 30. Tobias Makarius schrieb: On Fri, 29 Oct 2010, Lukas Bulwahn wrote: * Quickcheck now has a configurable time limit which is set to 30 seconds by default. This can be changed by adding [timeout = n] to the quickcheck command. The time limit for auto quickcheck is still set independently, by default to 5 seconds. I am a bit puzzled about the unit of seconds here. When time is represented as plain integer in Isabelle, it is usually done in milliseconds. This is motivated by simplicity and portability. Milliseconds basically give 3 digits of fixed-point representation without venturing on floating point numbers or SML's complicated time datatype, or even more complicated languages for time spans (like the Babylonians invented a long time ago to make life more interesting). Also note that configuration options are often correlated with preferences, which need to be manageable outside the ML process (e.g. in PG/Emacs or Isabelle/Scala). So any extra complications of ML time formats would also affect other environments. The JVM normally observes our milliseconds standard as well, and jEdit properties follow the same. This makes Isabelle/ML, Isabelle/Scala, Isabelle/jEdit agree nicely without any further ado. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
How about providing a parse function time_of_string which turns strings like 30s or 15ms into proper times, and possibly adding a configuration option scheme for times (besides the existing bool, int and string schemes)? It seems that this could and should be provided be provided by the system to have a uniform interface and prevent further confusion. Sascha Tobias Nipkow wrote: As I said, I was entirely unconfused that it is in seconds, and am glad of it. HOWEVER: there is indeed a confusing difference between s/h and Nitpick on the one hand and q/c on the other hand: quickcheck[timeout=30] sledgehammer[timeout=30s] And also in their response to the wrong format: quickcheck[timeout=30s] *** Outer syntax error: end of input expected, *** but keyword [ was found sledgehammer[timeout=30] *** Parameter timeout must be assigned a positive time value (e.g., 60 s, 200 ms) or none. *** At command sledgehammer Unification is appreciated ;-) Tobias Makarius schrieb: On Fri, 29 Oct 2010, Tobias Nipkow wrote: Unless I have a lapse of memory, the timeout specifications for s/h and Nitpick are also in seconds, possibly with an s appended. As a user I am glad about that, because I do not think in ms and would not like to write 3 instead of 30. I have forgotten to say that Jasmin has his own (complicated) time formats. This is again a question how we invest our own precious time (by keeping things as simple as possible) while minimizing user confusion. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS
New proof method smt for a combination of first-order logic with equality, linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors; there is also basic support for higher-order features (esp. lambda abstractions). It is an incomplete decision procedure based on external SMT solvers using the oracle mechanism.
[isabelle-dev] Arith fails with a Type error in application
This bug has already been fixed, see http://isabelle.in.tum.de/repos/isabelle/rev/40a0760a00ea Regards, Sascha Tjark Weber wrote: On Fri, 2009-08-21 at 19:19 +0200, Dennis Walter wrote: The following proof works fine if QuickDirty is enabled, i.e. in interactive mode. But if this proof is re-run with QD turned off (e.g. in batch mode), the proof fails, because arith yields the error displayed below. lemma [| 1 = (a::int); 1 = (b::int) |] == 1 = a * b apply (subgoal_tac EX a' b'. a = 1 + a' b = 1 + b' 0 = a' 0 = b') apply (clarsimp simp add: ring_simps add_nonneg_nonneg mult_nonneg_nonneg) apply arith done *** Type error in application: Incompatible operand type With Toplevel.debug set, I get the following exception trace, which leads me to suspect that the problem is somewhere in presburger. Regards, Tjark == 8 == Exception trace for exception - ERROR Goal.prove_common(6)err(1) List.map(2) Goal.prove_common(6) Cooper.provelin(2) Cooper.linearize_conv(3)/3 Cooper.linearize_conv(3) Conv.combination_conv(3) Conv.combination_conv(3) Conv.combination_conv(3) Conv.then_conv(3) Conv.then_conv(3) Qelim.gen_qelim_conv(8)conv(2) Conv.combination_conv(3) Conv.combination_conv(3) Conv.then_conv(3) Qelim.gen_qelim_conv(8)conv(2) Conv.combination_conv(3) Conv.combination_conv(3) Conv.combination_conv(3) Conv.then_conv(3) Qelim.gen_qelim_conv(8)conv(2) Conv.combination_conv(3) Conv.then_conv(3) Conv.then_conv(3) Cooper.conv(2) Conv.combination_conv(3) Presburger.core_cooper_tac(1)(2) Tactical.CSUBGOAL(3) Tactical.CSUBGOAL(3) Tactical.CSUBGOAL(3) Seq.INTERVAL(4) Seq.map(2)(1) Seq.flat(1)(1) Seq.map(2)(1) Seq.flat(1)(1) Tactical.ORELSE(1)(1) Seq.map(2)(1) Seq.flat(1)(1) Seq.append(2)copy(1)(1) Seq.map(2)(1) Seq.map(2)(1) Seq.map(2)(1) Toplevel.proofs'(1)(1)(1) Runtime.debugging(2)(1) End of trace ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS
* New testing tool Mirabelle for automated (proof) tools. Applies several tools and tactics like sledgehammer, metis, or quickcheck, to every proof step in a theory. To be used in batch mode via isabelle mirabelle.
