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
10 matches
Mail list logo
