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
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
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
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
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 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
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
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
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
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
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.
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
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,
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
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
15 matches
Mail list logo
