Re: [isabelle-dev] Proper sign of gcd / lcm on type int

[Pierpaolo Bernardi]

About signs in divisions etc. I found the following paper very useful:

http://research.microsoft.com/apps/pubs/default.aspx?id=151917

Maybe someone else will find it useful too.

Cheers


On Fri, Jun 3, 2016 at 9:29 PM, Makarius  wrote:
> On 03/06/16 18:49, David Matthews wrote:
>
>> The Poly/ML implementation was based on the idea that something called a
>> "multiple" ought to follow the usual rules of multiplication; nothing
>> stronger than that.  I don't think I found anything that indicated what
>> the sign should be.  The GCD code uses GMP's GCD if possible; the LCM
>> code is just derived from that.
>>
>> I have no strong opinions on this and I'm happy to change it.  There's
>> also the question of whether to add it to the IntInf structure and
>> signature despite the incompatibility with the "official" library
>> definition.
>
> How is the situation wrt. planned updates of the SML Basic Library
> specification?
>
> Maybe this is a chance to add IntInf.gcd and IntInf.lcm officially,
> which a clear specification about the sign, whatever that might be.
>
>
> Makarius
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Proper sign of gcd / lcm on type int

[Makarius]

On 03/06/16 18:49, David Matthews wrote:

> The Poly/ML implementation was based on the idea that something called a
> "multiple" ought to follow the usual rules of multiplication; nothing
> stronger than that.  I don't think I found anything that indicated what
> the sign should be.  The GCD code uses GMP's GCD if possible; the LCM
> code is just derived from that.
> 
> I have no strong opinions on this and I'm happy to change it.  There's
> also the question of whether to add it to the IntInf structure and
> signature despite the incompatibility with the "official" library
> definition.

How is the situation wrt. planned updates of the SML Basic Library
specification?

Maybe this is a chance to add IntInf.gcd and IntInf.lcm officially,
which a clear specification about the sign, whatever that might be.


Makarius


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Proper sign of gcd / lcm on type int

[David Matthews]

On 02/06/2016 08:19, Manuel Eberl wrote:

I do think that we should enforce the same thing in the ML
implementation of gcd/lcm. Any definition of gcd/lcm for integers where
either of them may be negative does not make much sense to me. My guess
would be that lcm can be negative in the implementation you mentioned
because the author defined "lcm a b = a * b / gcd a b" with the unstated
assumption that it is only called for non-negative numbers. Or perhaps
they thought the sign does not matter.


The Poly/ML implementation was based on the idea that something called a 
"multiple" ought to follow the usual rules of multiplication; nothing 
stronger than that.  I don't think I found anything that indicated what 
the sign should be.  The GCD code uses GMP's GCD if possible; the LCM 
code is just derived from that.


I have no strong opinions on this and I'm happy to change it.  There's 
also the question of whether to add it to the IntInf structure and 
signature despite the incompatibility with the "official" library 
definition.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] PolyML bundle build steps

[Matthew Fernandez]

Hi Makarius et al,

Apologies if is already known, but I could not find any obvious reference to it.

The PolyML tarball that comes bundled with Isabelle has a script `build` that 
automates compilation.
Very handy. However, when moving files towards the end, it seems to attempt 
something that doesn't
work out:

  ...
  mv: cannot move 'src/x86_64-linux/lib/pkgconfig' to 'x86_64-linux/pkgconfig': 
Directory not empty
  rmdir: failed to remove 'src/x86_64-linux/lib': Directory not empty
  ...

It looks to me like it is the result of these lines in `build`:

  ...
  91 mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
  92 rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"
  ...

The failure doesn't seem to affect the resulting build artefacts, but I don't 
think these lines are
intended to fail. This occurred when running `./build src x86_64-linux 
--with-gmp`. Just wanted to
let you know in case this was not a known situation.

Thanks,
Matt



The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev