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%.
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 w
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, compile
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 tha
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. After
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 propaga
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
inte
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 ver
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 i
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
> c
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.
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
12 matches
Mail list logo