Re: [isabelle-dev] Integers in Poly/ML

[Makarius]

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", 

Re: [isabelle-dev] Integers in Poly/ML

[Makarius]

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

[Lawrence Paulson]

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

[Makarius]

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

[Lawrence Paulson]

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

[Makarius]

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

[Lawrence Paulson]

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

[Tobias Nipkow]

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 > 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

[Makarius]

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 

Re: [isabelle-dev] Integers in Poly/ML

[Lawrence Paulson]

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

[Makarius]

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

[Tobias Nipkow]

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

[Lawrence Paulson]

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, Makarius  wrote: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

[Makarius]

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