Fix Z.gcd when exactly one argument is zero #39
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
OK, why not? But your patch only handles the case where both arguments are small integers. The case gcd(0,big_number) would require extra modifications. |
|
On 18/10/2018 10:07, Antoine Miné wrote:
OK, why not? But your patch only handles the case where both arguments are small integers. The case gcd(0,big_number) would require extra modifications.
Unfortunately, a similar modification in the slow path produces
segmentation faults…
As per the documentation
https://gmplib.org/manual/Low_002dlevel-Functions.html#index-mpn_005fgcd, this
is expected. Any hint on how to work around this is welcome.
Also, is there any sense in stating gcd(0,0)=0, given that gcd(a,a)=a holds for a > 0 ?
The higher-level function mpz_gcd does this
(https://gmplib.org/manual/Number-Theoretic-Functions.html#index-mpz_005fgcd).
|
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Oct 18, 2018
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
gcdext remains defined only if both arguments are non-zero
|
OK. I added support for gcd(0,large_integer) and gcd(0,0). |
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Oct 18, 2018
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Oct 18, 2018
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Oct 18, 2018
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Oct 23, 2018
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Oct 25, 2018
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Oct 25, 2018
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Nov 17, 2018
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Nov 17, 2018
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Nov 20, 2018
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Dec 6, 2018
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Jan 31, 2019
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Mar 4, 2019
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
|
Your last change Antoine looks good to me. I’ve run the test-suite of Coq on branch coq/coq#8743 without Emilio’s workaround using this fix: there are a few issues but none seems related to a failing GCD computation. Thanks again. |
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Mar 12, 2019
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
vbgl
pushed a commit
to vbgl/coq
that referenced
this pull request
Mar 13, 2019
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
vbgl
pushed a commit
to ejgallego/coq
that referenced
this pull request
Mar 13, 2019
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Mar 20, 2019
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Mar 21, 2019
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
|
Thanks for merging. Can we expect a release including this change? Thanks. |
Yes, I've made a 1.8 release with this fix. |
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Apr 8, 2019
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Mar 2, 2020
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Mar 2, 2020
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
ejgallego
added a commit
to ejgallego/coq
that referenced
this pull request
Mar 2, 2020
We workaround a bug in Zarith's `gcd`. Indeed, `gcd n 0` when `n != 0` should be `n`. The problem can be witnessed here: ``` utop # Big_int_Z.(gcd_big_int zero_big_int unit_big_int);; Exception: Division_by_zero. utop # Big_int.(gcd_big_int zero_big_int unit_big_int);; - : Big_int.big_int = <big_int 1> ``` c.f: ocaml/Zarith#39
sim642
added a commit
to goblint/analyzer
that referenced
this pull request
Nov 26, 2021
Congruences tests need zarith.1.8 to pass: ocaml/Zarith#39 in https://github.com/ocaml/Zarith/releases/tag/release-1.8.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The GCD operator is well defined when exactly one of its argument is zero. It should not raise a division-by-zero exception.