Re: [isabelle-dev] Integers in Poly/ML
On 02/11/16 13:51, Makarius wrote: > On 02/11/16 13:07, Lawrence Paulson wrote: >> David Matthews is working on a new release of Poly/ML in which the default >> type of integers is fixed-precision. A configuration option can restore the >> former set up, but that might be a mistake: I modified MetiTarski to use >> large integers only where needed and saw runtime decrease by around 30%. We >> could do the same. I imagine that we need large integers almost nowhere. Now >> consider that every bound variable is represented internally by an integer. > > I am surprised that MetiTarski shows such a relatively big speedup. > > My guess for Isabelle is between 0.1-5%, but it needs to be proven by > concrete measurements. Changing type int to be a fixed-width machine > word (and thus no int at all), will not work without significant work on > the sources. Already about 10 years ago, we switched in the opposite > direction, to make type int a proper integer even for SML/ML. That was a > great improvement for tool development, and a slowdown for SML/NJ of > 20-40% -- its IntInf implementation is very poor. To conclude this thread properly, here are the results of a quick test with ZF (spending only 20min on it). HOL probably requires much more work to make it run, with its use of rational numbers etc. Isabelle version: 2bf4fdcebd49 Poly/ML version: 55db4cc076ea8 ML_PLATFORM=x86_64-linux ML_HOME="$HOME/lib/polyml/${ML_PLATFORM}" ML_SYSTEM=polyml-5.6.1 ML_OPTIONS="-H 4000" FixedInt: isabelle build -g ZF -o threads=1 Finished Pure (0:00:19 elapsed time, 0:00:19 cpu time, factor 1.00) Finished ZF (0:00:33 elapsed time, 0:00:33 cpu time, factor 1.00) Finished ZF-AC (0:00:09 elapsed time, 0:00:09 cpu time, factor 1.00) Finished ZF-Constructible (0:00:24 elapsed time, 0:00:24 cpu time, factor 1.00) Finished ZF-Induct (0:00:11 elapsed time, 0:00:11 cpu time, factor 1.00) Finished ZF-UNITY (0:00:30 elapsed time, 0:00:30 cpu time, factor 1.00) Finished ZF-ex (0:00:12 elapsed time, 0:00:12 cpu time, factor 1.00) isabelle build -g ZF -o threads=4 Finished Pure (0:00:19 elapsed time, 0:00:19 cpu time, factor 1.00) Finished ZF (0:00:16 elapsed time, 0:00:46 cpu time, factor 2.84) Finished ZF-AC (0:00:04 elapsed time, 0:00:12 cpu time, factor 3.20) Finished ZF-Constructible (0:00:12 elapsed time, 0:00:41 cpu time, factor 3.18) Finished ZF-Induct (0:00:05 elapsed time, 0:00:15 cpu time, factor 2.90) Finished ZF-UNITY (0:00:11 elapsed time, 0:00:40 cpu time, factor 3.66) Finished ZF-ex (0:00:07 elapsed time, 0:00:17 cpu time, factor 2.44) IntInf: isabelle build -g ZF -o threads=1 Finished Pure (0:00:22 elapsed time, 0:00:22 cpu time, factor 1.00) Finished ZF (0:00:34 elapsed time, 0:00:34 cpu time, factor 1.00) Finished ZF-AC (0:00:07 elapsed time, 0:00:07 cpu time, factor 1.00) Finished ZF-Constructible (0:00:25 elapsed time, 0:00:25 cpu time, factor 1.00) Finished ZF-Induct (0:00:07 elapsed time, 0:00:07 cpu time, factor 1.00) Finished ZF-UNITY (0:00:28 elapsed time, 0:00:28 cpu time, factor 1.00) Finished ZF-ex (0:00:13 elapsed time, 0:00:13 cpu time, factor 1.00) isabelle build -g ZF -o threads=4 Finished Pure (0:00:20 elapsed time, 0:00:20 cpu time, factor 1.00) Finished ZF (0:00:18 elapsed time, 0:00:50 cpu time, factor 2.80) Finished ZF-AC (0:00:03 elapsed time, 0:00:10 cpu time, factor 3.19) Finished ZF-Constructible (0:00:10 elapsed time, 0:00:35 cpu time, factor 3.20) Finished ZF-Induct (0:00:03 elapsed time, 0:00:10 cpu time, factor 2.77) Finished ZF-UNITY (0:00:11 elapsed time, 0:00:40 cpu time, factor 3.64) Finished ZF-ex (0:00:07 elapsed time, 0:00:18 cpu time, factor 2.49) This means there is no measurable difference, just some noise in the data. So the actual speedup might be closer to 0.1% than to 5% in my initial guess. My original plan to experiment with FixedInt, when the Poly/ML repository version is again fully working, had a much higher priority before this mail thread. Now I will put it to the bottom of my TODO list. There are so many better ways to scale Isabelle, by looking at the big picture, instead of low-level tuning that degrades basic mathematical concepts. Makarius # HG changeset patch # User wenzelm # Date 1478379718 -3600 # Sat Nov 05 22:01:58 2016 +0100 # Node ID b2ca5566c978c4b238c4126051a00fa6f60f64b2 # Parent 2bf4fdcebd495516947e5e85f3b3db01d5fbe1a4 test; diff -r 2bf4fdcebd49 -r b2ca5566c978 src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Sat Nov 05 20:44:47 2016 +0100 +++ b/src/Pure/Concurrent/task_queue.ML Sat Nov 05 22:01:58 2016 +0100 @@ -150,7 +150,7 @@ let val (run, wait, wait_deps) = (case timing of NONE => timing_start | SOME var => Synchronized.value var); -fun micros time = string_of_int (Time.toNanoseconds time div 1000); +fun micros time = string_of_int (IntInf.toInt (Time.toNanoseconds time div 1000)); in [("now", Value.print_real (Time.toReal (Time.now (, ("task_name", name)
Re: [isabelle-dev] Integers in Poly/ML
On 03/11/16 14:59, Lawrence Paulson wrote: > Let’s be clear: the semantics of type int is well-defined. It denotes > the set of integers over a specific finite range of values, and if this > range is exceeded, exception Overflow is raised. If one’s requirements > fit within that range of values then there is no rational reason to > suffer a penalty in order to widen that range. Back to field 1. We need to reboot the project "Enlightment and Rationalism" from some centuries ago. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Integers in Poly/ML
Let’s be clear: the semantics of type int is well-defined. It denotes the set of integers over a specific finite range of values, and if this range is exceeded, exception Overflow is raised. If one’s requirements fit within that range of values then there is no rational reason to suffer a penalty in order to widen that range. Larry > On 3 Nov 2016, at 13:46, Makarius wrote: > > Luckily the situation is not as bad, and David Matthews continues to > consolidate the new compiler and run-time system: Isabelle is already a > bit faster than before, while still remaining true to mathematical > semantics of int. > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Integers in Poly/ML
On 03/11/16 13:47, Lawrence Paulson wrote: > Just as remark: MetiTarski took a slight performance hit in the > transition to the new compiler, happily greatly reversed by my decision > to use fixed-precision integers. That taken alone would have meant a step backwards: proper integers have become non-integers, just to follow the errors of the majority in the last decades. Luckily the situation is not as bad, and David Matthews continues to consolidate the new compiler and run-time system: Isabelle is already a bit faster than before, while still remaining true to mathematical semantics of int. More tuning and measurements will follow in the coming weeks/months ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Integers in Poly/ML
Just as remark: MetiTarski took a slight performance hit in the transition to the new compiler, happily greatly reversed by my decision to use fixed-precision integers. Of course I would like to use the IDE for Standard ML, but getting started is always more complicated than it looks. Larry > On 2 Nov 2016, at 22:22, Makarius wrote: > > I've been working with David Matthews for some weeks to see the new > compiler and related run-time system changes work with Isabelle, and > perform well. Right now the situation is that all of the Isabelle > repository compiles, and AFP almost works (I have tested it for the > first time only a few days ago). > > At the same time, we have taken some looks at performance: in the very > first round, the new approach was much slower, now it is a bit faster -- > thanks to some improvements in string comparison. More systematic > performance tests will come later. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Integers in Poly/ML
On 02/11/16 17:30, Lawrence Paulson wrote: > > I think it would be quite straightforward to try the experiment of > building Isabelle with the new compiler, but I would need some help with > our present setup I've been working with David Matthews for some weeks to see the new compiler and related run-time system changes work with Isabelle, and perform well. Right now the situation is that all of the Isabelle repository compiles, and AFP almost works (I have tested it for the first time only a few days ago). At the same time, we have taken some looks at performance: in the very first round, the new approach was much slower, now it is a bit faster -- thanks to some improvements in string comparison. More systematic performance tests will come later. Nothing of this is fundamentally new: Poly/ML has changed many times before, and Isabelle was changed to follow-up and improve the overall situation: towards more clarity, more correctness, more performance. > Is the question of 32 versus 64 bits relevant here? I suspect it isn’t. > Any integers of ours requiring more than 32 bits need to be large integers. The short int has only 31 bits and there is also a sign bit. It means there are only approx. 10E9 different values, lets say for some uniquely generated identifier or index into some data structure. As an array index that is only 1GB, afterwards overflow happens. In Java, this has led to some surprises some years ago (IIRC in array sorting algorithms). Although nobody should be surprised, when small finite values do eventually overflow. For us there would be spurious exceptions, instead of silent overflow. I need to correct an earlier statement of mine: overflow *can* be a problem, e.g. in the frequently used "try" and "can" combinators. Only interrupt exceptions are carefully separated from the mathematical meaning of Isabelle/ML, not overflows or other soft errors. > whereas I recall we keep our own copy of the compiler packaged in > a special way somewhere I was talking a tiny little bit about this at the Isabelle workshop in Nancy. There are several stages of Isabelle/ML compiler bootstrap, also the separation of a physical and a virtual version of the ML environment. That is definitely interesting to look at, but not so easy to understand. To get a feel for it, I recommend to start as a user of the IDE for Isabelle/ML or Standard ML. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Integers in Poly/ML
Okay then. Obviously proceed with caution, as always. MetiTarski also has high standards, and doesn’t have the added security of a kernel architecture. Every significant change is checked by regression testing using tools that highlight significant changes in the runtime of the full test suite. This test suite includes many statements known to be false in order to catch soundness errors. Not that I was expecting any in this case: the required changes were small and logically trivial (mainly, converting between large and small integers). I think it would be quite straightforward to try the experiment of building Isabelle with the new compiler, but I would need some help with our present setup (whereas I recall we keep our own copy of the compiler packaged in a special way somewhere). Also now is perhaps about time to accumulate changes, though I don’t expect to see many. Can we wait until the next release is out? And yes, I could do it myself. Is the question of 32 versus 64 bits relevant here? I suspect it isn’t. Any integers of ours requiring more than 32 bits need to be large integers. Larry > On 2 Nov 2016, at 15:29, Makarius wrote: > > On 02/11/16 15:58, Lawrence Paulson wrote: >> I have to say, I’m absolutely mystified by the response to my suggestion. > > Why? I did not reject the idea, but only put it into the context of > Isabelle. MetiTarski is a small research experiment, but Isabelle a huge > and complex software product, with very high standards. > > >> We have spent a lot of time discussing problems caused by the cost of >> regression testing, and now we have the possibility of reducing that by 30%. > > Where is the empirical measurement for Isabelle? Without that it is just > speculation. > > A quick test with x86_64 and int = FixedInt might actually give some > ideas about the order of potential performance improvement. Do you want > to make one? > > > In the Jenkins project, there were also proposals to move to 64bit by > default, and thus lose a lot of performance. (The general waste of > resources of Jenkins is caused by high-level policies, though, and > theses were not openly discussed so far.) > > >> As to changes in behaviour that could be caused by overflows, I checked: >> exception Overflow is explicitly caught in only two places throughout >> the sources, both in HOL decision procedures (and therefore well outside >> the kernel) while the wildcard exception is caught in three places in >> Pure. > > I routinely check these things before each release. Catch-all patterns > are more frequent than that, but they are OK. > > I don't think that such a change would cause wrong results, but just > unexpected failure, and that is already bad enough in everyday use. > > >> No exception handlers had to be added when I converted MetiTarski >> to use fixed integers. An uncaught exception doesn’t prove anything, of >> course. > > BTW, you have a lot of catch-all exception handlers in MetiTarski. The > Isabelle/ML IDE shows that -- my changeset from last summer is attached > again. > > > Makarius > > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Integers in Poly/ML
On 02/11/16 15:43, Makarius wrote: > On 02/11/16 15:30, Lawrence Paulson wrote: > > We also have conceptual reasons to stay true to the concept of an > integer that is an integer, a string that is a string etc. -- and thus > not using a machine word instead of an integer, or a "char" type that > cannot hold a textual character (not even in Unicode). Isabelle/ML is > meant to be a programming environment free from bad jokes like that. This side-track requires more explanations: recent changes by David Matthews in Poly/ML provide more direct access to machine word arithmetic, but also characters that are not the same as singleton strings (which used to be the representation over 3 decades). The problem is that type char cannot hold a text entity outside the ASCII / ISO-LATIN world from the 1980s. Even wide chars from the 1990s are not sufficient, see the nice article http://utf8everywhere.org -- it explains why Windows, Java, even Python did it all wrong (while meaning only good). This view of varianbe-width characters nicely fits into the Isabelle symbol representation, as packed strings or exploded strings. And after some standard fine-tuning of the implementation, the change of representation in the Poly/ML repository version did not affect Isabelle performance: we could keep up our model of an unbounded formal alphabet. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Integers in Poly/ML
On 02/11/2016 15:58, Lawrence Paulson wrote: I have to say, I’m absolutely mystified by the response to my suggestion. This is a nontrivial change in the semantics. The programming language community has tried to get away from the "looks ok" approach to "here is some sound reasoning why it is ok". I could indeed not construct an example where a new incorrect result arises because of a caught over/underflow exception (only new ways to construct results that could already arise before). But that isn't exactly a proof (although the proposition may well be a thm). Otherwise I agree with Makarius. Tobias MetiTarski, which during execution relies heavily on large integers, nevertheless benefits to the tune of 30% to having all other integers fixed-precision. During its execution, Isabelle makes very heavy use of small integers, in the representation of bound variables and flexible variables, which are renamed by having an offset before each and every resolution step. We have spent a lot of time discussing problems caused by the cost of regression testing, and now we have the possibility of reducing that by 30%. As to changes in behaviour that could be caused by overflows, I checked: exception Overflow is explicitly caught in only two places throughout the sources, both in HOL decision procedures (and therefore well outside the kernel) while the wildcard exception is caught in three places in Pure. No exception handlers had to be added when I converted MetiTarski to use fixed integers. An uncaught exception doesn’t prove anything, of course. Larry On 2 Nov 2016, at 14:43, Makarius mailto:makar...@sketis.net>> wrote: On 02/11/16 15:30, Lawrence Paulson wrote: I actually can’t think of many places where Isabelle would need large integers, so it would probably benefit even more than MetiTarski does. "Can't think of" merely indicates a lack of empirical tests, against the Isabelle repository and AFP. Afterwards the situation usually looks quite different, and the initial hypothesis needs to be changed. When we moved to proper int by default some years ago, there were several tool implementors approaching me, asking to be delivered from the curse of many different "int" types. We also have conceptual reasons to stay true to the concept of an integer that is an integer, a string that is a string etc. -- and thus not using a machine word instead of an integer, or a "char" type that cannot hold a textual character (not even in Unicode). Isabelle/ML is meant to be a programming environment free from bad jokes like that. Nonetheless, I do think that proper use of machine words in isolated situations can help, but they should not be called "int" and used by default. Makarius 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] Integers in Poly/ML
On 02/11/16 15:58, Lawrence Paulson wrote: > I have to say, I’m absolutely mystified by the response to my suggestion. Why? I did not reject the idea, but only put it into the context of Isabelle. MetiTarski is a small research experiment, but Isabelle a huge and complex software product, with very high standards. > We have spent a lot of time discussing problems caused by the cost of > regression testing, and now we have the possibility of reducing that by 30%. Where is the empirical measurement for Isabelle? Without that it is just speculation. A quick test with x86_64 and int = FixedInt might actually give some ideas about the order of potential performance improvement. Do you want to make one? In the Jenkins project, there were also proposals to move to 64bit by default, and thus lose a lot of performance. (The general waste of resources of Jenkins is caused by high-level policies, though, and theses were not openly discussed so far.) > As to changes in behaviour that could be caused by overflows, I checked: > exception Overflow is explicitly caught in only two places throughout > the sources, both in HOL decision procedures (and therefore well outside > the kernel) while the wildcard exception is caught in three places in > Pure. I routinely check these things before each release. Catch-all patterns are more frequent than that, but they are OK. I don't think that such a change would cause wrong results, but just unexpected failure, and that is already bad enough in everyday use. > No exception handlers had to be added when I converted MetiTarski > to use fixed integers. An uncaught exception doesn’t prove anything, of > course. BTW, you have a lot of catch-all exception handlers in MetiTarski. The Isabelle/ML IDE shows that -- my changeset from last summer is attached again. Makarius # HG changeset patch # User wenzelm # Date 1464704221 -7200 # Tue May 31 16:17:01 2016 +0200 # Node ID e517f280847f40ff7b3a104c4c0f46bca815cc54 # Parent b11e8139b880bde17d291e1d35c3a3577185a82f basic setup for Isabelle/SML IDE; diff -r b11e8139b880 -r e517f280847f src/+ld.sml --- a/src/+ld.sml Mon Mar 30 15:28:39 2015 +0100 +++ b/src/+ld.sml Tue May 31 16:17:01 2016 +0200 @@ -66,7 +66,12 @@ use"Tptp.sig"; use"Tptp.sml"; use"SMTLIB.sig"; use"SMTLIB.sml"; -use"Syntax/load.sml"; +use"Syntax/lib/base.sig"; +use"Syntax/lib/join.sml"; +use"Syntax/lib/lrtable.sml"; +use"Syntax/lib/stream.sml"; +use"Syntax/lib/parser2.sml"; +use"Syntax/load0.sml"; use"Options.sig"; use"Options.sml"; use"metis.sml"; diff -r b11e8139b880 -r e517f280847f src/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 + +++ b/src/ROOT.ML Tue May 31 16:17:01 2016 +0200 @@ -0,0 +1,75 @@ +SML_file "Portable.sig"; +SML_file "Random.sig"; SML_file "Random.sml"; +SML_file "PortablePolyml.sml"; +SML_file "Polyhash.sig"; SML_file "Polyhash.sml"; +SML_file "Useful.sig"; SML_file "Useful.sml"; +SML_file "rat.sml"; (*John Harrison's code*) +SML_file "Lazy.sig"; SML_file "Lazy.sml"; +SML_file "Map.sig"; SML_file "Map.sml"; +SML_file "Set.sig"; SML_file "Set.sml"; +SML_file "Ordered.sig"; SML_file "Ordered.sml"; +SML_file "KeyMap.sig"; SML_file "KeyMap.sml"; +SML_file "ElementSet.sig"; SML_file "ElementSet.sml"; +SML_file "Sharing.sig"; SML_file "Sharing.sml"; +SML_file "Stream.sig"; SML_file "Stream.sml"; +SML_file "Heap.sig"; SML_file "Heap.sml"; +SML_file "Print.sig"; SML_file "Print.sml"; +SML_file "Parse.sig"; SML_file "Parse.sml"; +SML_file "Name.sig"; SML_file "Name.sml"; +SML_file "NameArity.sig"; SML_file "NameArity.sml"; +SML_file "Term.sig"; SML_file "Term.sml"; +SML_file "Subst.sig"; SML_file "Subst.sml"; +SML_file "Atom.sig"; SML_file "Atom.sml"; +SML_file "Formula.sig"; SML_file "Formula.sml"; +SML_file "Literal.sig"; SML_file "Literal.sml"; +SML_file "KnuthBendixOrder.sig"; SML_file "KnuthBendixOrder.sml"; +SML_file "Poly.sig"; SML_file "Poly.sml"; +SML_file "RCF/Common.sig"; SML_file "RCF/Common.sml"; +SML_file "RCF/Algebra.sig"; SML_file "RCF/Algebra.sml"; +SML_file "RCF/Groebner.sig"; SML_file "RCF/Groebner.sml"; +SML_file "RCF/SMT.sig"; SML_file "RCF/SMT.sml"; +SML_file "RCF/IntvlsFP.sig"; SML_file "RCF/IntvlsFP.sml"; +SML_file "RCF/Resultant.sig"; SML_file "RCF/Resultant.sml"; +SML_file "RCF/Sturm.sig"; SML_file "RCF/Sturm.sml"; +SML_file "RCF/RealAlg.sig"; SML_file "RCF/RealAlg.sml"; +SML_file "RCF/MTAlgebra.sig"; SML_file "RCF/MTAlgebra.sml"; +SML_file "RCF/CADProjO.sig"; SML_file "RCF/CADProjO.sml"; +SML_file "RCF/Mathematica.sig"; SML_file "RCF/Mathematica.sml"; +SML_file "RCF/Qepcad.sig"; SML_file "RCF/Qepcad.sml"; +SML_file "RCF/Nullsatz.sig"; SML_file "RCF/Nullsatz.sml"; +SML_file "RCF/CertRCFk.sig"; SML_file "RCF/CertRCFk.sml"; +SML_file "RCF/CertRCFp.sig"; SML_file "RCF/CertRCFp.sml"; +SML_file "RCF/RCF.sig"; SML_file "RCF/RCF.sml"; +SML_file "Thm.sig"; SML_file "Thm.sml"; +SML_file "Proof.sig"; SML_file "Proof.sml"; +SML_file "Rule.sig"; SML_file "Rule.sml"; +SML_file "Normalize.sig
Re: [isabelle-dev] Integers in Poly/ML
I have to say, I’m absolutely mystified by the response to my suggestion. MetiTarski, which during execution relies heavily on large integers, nevertheless benefits to the tune of 30% to having all other integers fixed-precision. During its execution, Isabelle makes very heavy use of small integers, in the representation of bound variables and flexible variables, which are renamed by having an offset before each and every resolution step. We have spent a lot of time discussing problems caused by the cost of regression testing, and now we have the possibility of reducing that by 30%. As to changes in behaviour that could be caused by overflows, I checked: exception Overflow is explicitly caught in only two places throughout the sources, both in HOL decision procedures (and therefore well outside the kernel) while the wildcard exception is caught in three places in Pure. No exception handlers had to be added when I converted MetiTarski to use fixed integers. An uncaught exception doesn’t prove anything, of course. Larry > On 2 Nov 2016, at 14:43, Makarius wrote: > > On 02/11/16 15:30, Lawrence Paulson wrote: >> >> I actually can’t think of many places where Isabelle would need large >> integers, so it would probably benefit even more than MetiTarski does. > > "Can't think of" merely indicates a lack of empirical tests, against the > Isabelle repository and AFP. Afterwards the situation usually looks > quite different, and the initial hypothesis needs to be changed. > > When we moved to proper int by default some years ago, there were > several tool implementors approaching me, asking to be delivered from > the curse of many different "int" types. > > We also have conceptual reasons to stay true to the concept of an > integer that is an integer, a string that is a string etc. -- and thus > not using a machine word instead of an integer, or a "char" type that > cannot hold a textual character (not even in Unicode). Isabelle/ML is > meant to be a programming environment free from bad jokes like that. > > > Nonetheless, I do think that proper use of machine words in isolated > situations can help, but they should not be called "int" and used by > default. > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Integers in Poly/ML
On 02/11/16 15:37, Tobias Nipkow wrote: > > With bounded integers, we would have to worry about what happens to > over/underflow exceptions: can handlers for such exceptions in a piece > of user code lead to unsoundness in the inference system? At first it > seems that if such an exception propagates out of the kernel, no > incorrect theorems can arise (because control has left the kernel). > However, in the presence of higher-order functions (e.g. user functions > can be passed to kernel code) this is not so clear to me. This introduces two more aspects: (1) Spurious overflow exceptions: our ML code (even out there in user tools) is usually quite clean, in *not* using unspecific exception handlers, but that is no guarantee. Interestingly, the SML'97 + SML/NJ guys who introduced the short ints also propagated the "handle _ => .." style that makes a programm erratic wrt. environmental effects (interrupts) and unexpected overflows. (2) Critical modules (sometimes called kernel, although we have more than one such area). Here the exception situation is clean, because the sources have been inspected over and over again. One benefit of *not* using full int, but the speculative type "index" for term structures, would be a simpler situation in the ML implementation. We've had errors with full integers in distant past, in the glue between the ML and C world. Relying only on plain machine arithmetic with overflow handling would reduce the dependence on other modules. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Integers in Poly/ML
On 02/11/16 15:30, Lawrence Paulson wrote: > > I actually can’t think of many places where Isabelle would need large > integers, so it would probably benefit even more than MetiTarski does. "Can't think of" merely indicates a lack of empirical tests, against the Isabelle repository and AFP. Afterwards the situation usually looks quite different, and the initial hypothesis needs to be changed. When we moved to proper int by default some years ago, there were several tool implementors approaching me, asking to be delivered from the curse of many different "int" types. We also have conceptual reasons to stay true to the concept of an integer that is an integer, a string that is a string etc. -- and thus not using a machine word instead of an integer, or a "char" type that cannot hold a textual character (not even in Unicode). Isabelle/ML is meant to be a programming environment free from bad jokes like that. Nonetheless, I do think that proper use of machine words in isolated situations can help, but they should not be called "int" and used by default. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Integers in Poly/ML
I value the guarantees we get from having proper integers a lot. No worries. With bounded integers, we would have to worry about what happens to over/underflow exceptions: can handlers for such exceptions in a piece of user code lead to unsoundness in the inference system? At first it seems that if such an exception propagates out of the kernel, no incorrect theorems can arise (because control has left the kernel). However, in the presence of higher-order functions (e.g. user functions can be passed to kernel code) this is not so clear to me. Tobias On 02/11/2016 13:07, Lawrence Paulson wrote: David Matthews is working on a new release of Poly/ML in which the default type of integers is fixed-precision. A configuration option can restore the former set up, but that might be a mistake: I modified MetiTarski to use large integers only where needed and saw runtime decrease by around 30%. We could do the same. I imagine that we need large integers almost nowhere. Now consider that every bound variable is represented internally by an integer. Larry ___ 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] Integers in Poly/ML
The difference is substantial and uniform. I attach log files summarising MetiTarski’s performance by nearly 900 examples. You will note that total CPU time is way down, and problems consistently run much faster using fixed-precision arithmetic. Both runs involve the new version of Poly/ML, compiled with GMP.Note that MetiTarski makes heavy use of large integers, hundreds or thousands of digits long, because of its use of rational numbers.I actually can’t think of many places where Isabelle would need large integers, so it would probably benefit even more than MetiTarski does. Larry On 2 Nov 2016, at 12:51, Makariuswrote:I am surprised that MetiTarski shows such a relatively big speedup. Doesit really happen in a sustained manner for typical uses, and not just inisolated cases?My guess for Isabelle is between 0.1-5%, but it needs to be proven byconcrete measurements. Changing type int to be a fixed-width machineword (and thus no int at all), will not work without significant work onthe sources. Already about 10 years ago, we switched in the oppositedirection, to make type int a proper integer even for SML/ML. That was agreat improvement for tool development, and a slowdown for SML/NJ of20-40% -- its IntInf implementation is very poor. STATUS-Metit-2016-10-11-60-test3-polyml.log Description: Binary data STATUS-Metit-2016-10-31-60-fixed-int.log Description: Binary data ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Integers in Poly/ML
On 02/11/16 13:07, Lawrence Paulson wrote: > David Matthews is working on a new release of Poly/ML in which the default > type of integers is fixed-precision. A configuration option can restore the > former set up, but that might be a mistake: I modified MetiTarski to use > large integers only where needed and saw runtime decrease by around 30%. We > could do the same. I imagine that we need large integers almost nowhere. Now > consider that every bound variable is represented internally by an integer. I am surprised that MetiTarski shows such a relatively big speedup. Does it really happen in a sustained manner for typical uses, and not just in isolated cases? My guess for Isabelle is between 0.1-5%, but it needs to be proven by concrete measurements. Changing type int to be a fixed-width machine word (and thus no int at all), will not work without significant work on the sources. Already about 10 years ago, we switched in the opposite direction, to make type int a proper integer even for SML/ML. That was a great improvement for tool development, and a slowdown for SML/NJ of 20-40% -- its IntInf implementation is very poor. Anyway, I have always been in close contact with David Matthews concerning various performance improvements. The present idea is to introduce a new type (e.g. called "index") that is a short machine word and used for the de-Bruijn index in a term and also for indexname. Further experimentation will be needed to see how far such a symbolic index can be pushed elsewhere. E.g. type "serial" is another candidate, but FixedInt has only 31 bits on our standard platform, and overflows at approx. 10E9. This limits the total livetime of an Isabelle process, notably an interactive one or a dumped image. Switching to 64bit by default would avoid this, but it costs 20-30% overall performance penalty, and requires a reasonably big machine (16 GB or better 32 GB). I am still trying to avoid the discontinuity towards 64bit -- after the release I will look again how to reduce overall resource requirements -- just another round of Tetris. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Integers in Poly/ML
David Matthews is working on a new release of Poly/ML in which the default type of integers is fixed-precision. A configuration option can restore the former set up, but that might be a mistake: I modified MetiTarski to use large integers only where needed and saw runtime decrease by around 30%. We could do the same. I imagine that we need large integers almost nowhere. Now consider that every bound variable is represented internally by an integer. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev