Re: [isabelle-dev] [isabelle] the sound of a sledgehammer
On Fri, 2013-02-15 at 13:37 +0100, Tobias Nipkow wrote: * Sledgehammer spontaneously acts asynchronously of certain open problems in the text, depending on certain parameters like time outs. Triggering s/h via sorry (or some other explicit means) is perfectly reasonable, but having the IDE invoke s/h based on time outs and guesses should be avoided: the success rate is low and it consumes a lot of resources. My gut feeling is that already today, I would prefer s/h to run automatically on every intermediate proof state if this didn't interfere with my editing. Why should the many cores in my machine sit idle? It seems perfectly reasonable to spend a few billion CPU cycles if that occasionally saves a minute or two of human time. Architecturally, some kind of incremental mode for s/h (as suggested by Jasmin) could reduce the performance overhead. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] the sound of a sledgehammer
On Sunday, February 17, 2013 at 17:06:46 (+0100), Tjark Weber wrote: On Fri, 2013-02-15 at 13:37 +0100, Tobias Nipkow wrote: * Sledgehammer spontaneously acts asynchronously of certain open problems in the text, depending on certain parameters like time outs. Triggering s/h via sorry (or some other explicit means) is perfectly reasonable, but having the IDE invoke s/h based on time outs and guesses should be avoided: the success rate is low and it consumes a lot of resources. My gut feeling is that already today, I would prefer s/h to run automatically on every intermediate proof state if this didn't interfere with my editing. Why should the many cores in my machine sit idle? Well I am all for it, as long as there is also a way to switch it on and off on demand. I sometimes work in a quite environment where my Mac Book Air should not emit noise like on an airport and be hot like a potato. In such circumstances I am quite happy if my CPUs waste a bit of idle time. ;o) Christian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] nat_code Equation
In private conversation, there has been some confusion concerning this issue (stemming from the users mailinglist originally). Let me clarify, quoting the tutorial on code generation: -- Code_Binary_Nat implements type nat using a binary rather than a linear representation, which yields a considerable speedup for computations. Pattern matching with 0 / Suc is eliminated by a preprocessor. Code_Target_Nat implements type nat by integer and thus by target-language built-in integers. Pattern matching with 0 / Suc is eliminated by a preprocessor. -- Both approaches currently share the same preprocessor which strives to eliminate all pattern matching on nat in function arguments by combining 0/Suc-twins. It naturally fails if no twin can be found but pattern matching on nat is still present. For Code_Binary_Nat, the alternative preprocessor suggested by Brian could be used instead: the binary presentation still allows pattern matching on 0 / Suc n to be replace by pattern matching on 0 / nat_of_num, but no pattern matching with successive Sucs. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Order Relations
Dear Larry, Stefan, Tobias, and Andrei (as authors of the relevant Isabelle/HOL theories), already several times I stumbled upon the definition of Relation.refl_on (and thus also Order_Relation.Refl) and was irritated. What is the reason for demanding r = A * A? And why are other properties from Order_Relation, which indicate an explicit domain by their name, defined by means of corresponding properties with implicit domain? E.g., in the following definitions definition preorder_on A r == refl_on A r ∧ trans r definition partial_order_on A r == preorder_on A r ∧ antisym r definition linear_order_on A r == partial_order_on A r ∧ total_on A r definition strict_linear_order_on A r == trans r ∧ irrefl r ∧ total_on A r definition well_order_on A r == linear_order_on A r ∧ wf(r - Id) I would expect properties like trans_on, antisym_on, irrefl_on, and wf_on with explicit domain (of course that would only make sense after dropping r = A * A from the definition of refl_on, since otherwise r will only ever relate elements of A in the above definitions). Now I saw that Andrei writes Refl_on A r requires in particular that r = A * A, and therefore whenever Refl_on A r, we have that necessarily A = Field r. This means that in a theory of orders the domain A would be redundant -- we decided not to include it explicitly for most of the tehory. in his README to the new Cardinal theories. So this (strange?) definition of reflexivity is here to stay and used by an ever growing body of theories. This occasionally causes me some headache when I start to think about how my definitions from the AFP entry Well_Quasi_Orders would fit in as standard definitions in Isabelle/HOL. ( do recall that the current definition of Relation.refl_on would not have worked for my proofs.) Any comments are appreciated. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] the sound of a sledgehammer
Am 17/02/2013 19:41, schrieb Christian Urban: On Sunday, February 17, 2013 at 17:06:46 (+0100), Tjark Weber wrote: On Fri, 2013-02-15 at 13:37 +0100, Tobias Nipkow wrote: * Sledgehammer spontaneously acts asynchronously of certain open problems in the text, depending on certain parameters like time outs. Triggering s/h via sorry (or some other explicit means) is perfectly reasonable, but having the IDE invoke s/h based on time outs and guesses should be avoided: the success rate is low and it consumes a lot of resources. My gut feeling is that already today, I would prefer s/h to run automatically on every intermediate proof state if this didn't interfere with my editing. Why should the many cores in my machine sit idle? Well I am all for it, as long as there is also a way to switch it on and off on demand. I sometimes work in a quite environment where my Mac Book Air should not emit noise like on an airport and be hot like a potato. In such circumstances I am quite happy if my CPUs waste a bit of idle time. ;o) There should be an energy saving mode switch for people on battery. It should disable all spontaneous computations. Tobias Christian ___ 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
