[numeral] [plugins] Remove Coq's `Bigint` module in favor of ZArith. by ejgallego · Pull Request #11742 · rocq-prover/rocq

ejgallego · 2020-03-03T21:49:54Z

We replace Coq's use of Bigint, Big_int and num by the ZArith OCaml
library which is a more modern version.

We switch the core files and easy plugins only for now, the remaining micromega plugins will be done in their own commit.

We thus keep the num library linked for now until micromega is ported.

Co-authored-by: Vincent Laporte Vincent.Laporte@fondation-inria.fr

Kind: feature / infrastructure.

Added / updated test-suite
Corresponding documentation was added / updated
Entry added in the changelog

Overlays:

[coq] Adapt to zarith, Coq's PR coq/coq#8743 rocq-community/bignums#44

ejgallego · 2020-03-03T21:52:10Z

This PR ports Coq to ZArith except for micromega; it is the first part of #8743 ;

The porting is actually quite ortogonal so we could indeed make #8743 self-contained for micromega, but IMO I think this is close enough to be ready that it is not worth it.

ejgallego · 2020-03-04T02:29:52Z

Two problems:

windows build needs to install gmp + zarith
nix also needs gmp + zarith ?
coq_makefile using -linkall makes linking fail in OCaml >= 4.08, workaround pushed.

Bench : https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/875/

ejgallego · 2020-03-04T04:38:35Z

@maximedenes can we install libgmp-dev on pendulum? [I'm afraid my network situation is bad as I'm on the road]

maximedenes · 2020-03-04T08:16:37Z

@maximedenes can we install libgmp-dev on pendulum? [I'm afraid my network situation is bad as I'm on the road]

Done.

maximedenes · 2020-03-04T08:22:16Z

I have a fear releated to this PR: since the porting of micromega failed, how do we know that this is correct? Aren't we just porting less well-tested parts (Big_int is notorious for having has some undetected long-standing critical bugs, for example, IIRC)? I would feel more comfortable if we port everything at once.

Also, what is the motivation for this change if num is still a dependency?

ejgallego · 2020-03-04T16:56:27Z

I have a fear related to this PR: since the porting of micromega failed how do we know that this is correct?

I'm not sure I understand what you mean about correctness; what is the particular concern you have in mind?

I don't think porting of micromega "failed", it just needs more work as there is not a 1-1 mapping of the APIs in a few places.

Aren't we just porting less well-tested parts (Big_int is notorious for having has some undetected long-standing critical bugs, for example, IIRC)?

What does Big_int has to do here? It is not involved in this PR IIANM; what do you mean about less "well-tested" parts? Both omega and the numeral notations are pretty well tested, and I'd say zarith/GMP is way more tested than num/bigint.

I would feel more comfortable if we port everything at once.

These are totally orthogonal components so I don't see any reason porting more stuff should increase the confidence on the current code.

maximedenes · 2020-03-04T17:06:00Z

@ejgallego my worry is not about the correctness of ZArith/GMP, of course, it is precisely about the correctness of the API mapping.

What does Big_int has to do here? It is not involved in this PR

I imagined you were replacing the uses of Big_int by ZArith because that's literally what the PR title says, but I must have misunderstood.

Under that assumption, my point was that uses of Big_int were not well tested. So the replacement by ZArith will also not be well tested.

ejgallego · 2020-03-04T17:14:23Z

I imagined you were replacing the uses of Big_int by ZArith because that's literally what the PR title says, but I must have misunderstood.

This is replacing Bigint, which is Coq's own version, Big_int is the one in OCaml [confusing I know]

@ejgallego my worry is not about the correctness of ZArith/GMP, of course, it is precisely about the correctness of the API mapping.

Under that assumption, my point was that uses of Big_int were not well tested. So the replacement by ZArith will also not be well tested.

Well that's hard to know, tho the API mapping performed this PR seems safe enough to me; I don't think the paths this PR modifies are not so well tested tho, they include omega and numeral notations, these are certainly used in quite a few places in the CI.

ejgallego · 2020-03-04T17:14:44Z

Done.

Thanks, let's see the new bench here https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/877

ejgallego · 2020-03-04T17:16:32Z

By the way micromega mostly works, I just don't have the time to fix it now, but it should not be hard. The problem is almost for sure in the particular spot where exponentation of rationals was used, but indeed there the old num API was allowing clients to do what seems like very weird things; so indeed we will have to improve code likely.

Note also that micromega uses big_int vs the parts of Coq that don't use it.

liyishuai · 2020-08-14T04:33:53Z

What's the status of this PR?

maximedenes · 2020-08-20T14:36:10Z

Sorry, I didn't merge in time because of summer vacations. @ejgallego would you mind rebasing?

We replace Coq's use of `Big_int` and `num` by the ZArith OCaml library which is a more modern version. We switch the core files and easy plugins only for now, more complex numerical plugins will be done in their own commit. We thus keep the num library linked for now until all plugins are ported. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

We could still optimize the functions in that file a bit more if there is need.

Suggested by Pierre Roux

ejgallego · 2020-08-27T17:03:42Z

@ejgallego would you mind rebasing?

Done.

maximedenes · 2020-08-28T16:49:44Z

@coqbot merge now

coqbot-app · 2020-08-28T16:49:47Z

@maximedenes: Please take care of the following overlays:

08743-ejgallego-zarith.sh

maximedenes · 2020-08-28T16:52:57Z

@coqbot Yes @coqbot, I shall do so. I hope you're having a good day. Thanks for merging!

RalfJung · 2020-08-29T07:18:38Z

Is it possible that this broke opam-based Coq builds? #12937

When dependencies change, would be good if the opam package was either fixed at the same time, or the opam maintainers were notified ahead of time.

RalfJung · 2020-08-29T09:34:00Z

 - The [num](https://github.com/ocaml/num) library; note that it is
  included in the OCaml distribution for OCaml versions < 4.06.0

+- The [ZArith library](https://github.com/ocaml/Zarith) >= 1.8


The version given here is inconsistent with what it says in the opam file (1.9.1).

bschommer · 2020-11-11T10:32:26Z

windows build needs to install gmp + zarith

For windows, this branch might be interesting since the libtommath builds fine under windows.

MSoegtropIMC · 2020-11-11T12:47:08Z

windows build needs to install gmp + zarith

For windows, this branch might be interesting since the libtommath builds fine under windows.

Not sure what the issue is on Windows. The Coq platform does build gmp on Windows. The opam package works fine.

bschommer · 2020-11-11T13:07:33Z

windows build needs to install gmp + zarith

For windows, this branch might be interesting since the libtommath builds fine under windows.

Not sure what the issue is on Windows. The Coq platform does build gmp on Windows. The opam package works fine.

If one wants to use the msvc, one does not get to far with the gmp, mpir (the gmp fork with different license and build script for visual studio) gave up on releasing new versions. Of course gmp should normally work if you use mingw or cygwin.

Edit: Also if one wants to vendor zarith packing libtommath additionally would avoid one system dependency.

ejgallego · 2020-11-11T19:02:53Z

@bschommer vendoring zarith would be an option, I'd be happy to finish ocaml/Zarith#73 if the zartih devs give the OK.

ejgallego added kind: redesign The same functionality is being re-implemented in a different way. kind: cleanup Code removal, deprecation, refactorings, etc. kind: infrastructure CI, build tools, development tools. labels Mar 3, 2020

ejgallego requested review from a team as code owners March 3, 2020 21:49

ejgallego requested a review from a team March 3, 2020 21:49

ejgallego requested review from a team as code owners March 3, 2020 21:49

ejgallego mentioned this pull request Mar 3, 2020

[micromega] Switch from Big_int to ZArith. #8743

Merged

ejgallego added this to the 8.12+beta1 milestone Mar 3, 2020

ejgallego force-pushed the zarith+core branch 2 times, most recently from 4a72f50 to dd6ee16 Compare March 4, 2020 05:14

ejgallego requested a review from a team as a code owner March 4, 2020 05:14

ejgallego force-pushed the zarith+core branch from dd6ee16 to 601ac64 Compare March 4, 2020 17:20

maximedenes added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 20, 2020

ejgallego and others added 5 commits August 27, 2020 19:03

[zarith] [notation] Build less intermediate values

3fcd90f

We could still optimize the functions in that file a bit more if there is need.

[numtok] [zarith] Simplifications

694afd3

Suggested by Pierre Roux

[nsatz] num → zarith

5a28133

[zarith] Changelog

21dd85b

ejgallego force-pushed the zarith+core branch from eb46402 to 21dd85b Compare August 27, 2020 17:04

github-actions Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 28, 2020

coqbot-app Bot merged commit 165aca8 into rocq-prover:master Aug 28, 2020

ejgallego deleted the zarith+core branch August 28, 2020 22:54

liyishuai mentioned this pull request Aug 29, 2020

[coq.dev] depends on zarith rocq-prover/opam#1410

Merged

RalfJung mentioned this pull request Aug 29, 2020

[coq] Adapt to zarith, Coq's PR coq/coq#8743 rocq-community/bignums#44

Merged

Alizter mentioned this pull request Aug 29, 2020

CI failing HoTT/Coq-HoTT#1390

Closed

RalfJung reviewed Aug 29, 2020

View reviewed changes

Alizter mentioned this pull request Aug 29, 2020

./configure doesn't check for zarith package #12938

Closed

JasonGross added a commit to JasonGross/coq-packaging that referenced this pull request Aug 29, 2020

Add zarith after rocq-prover/rocq#11742

22da891

JasonGross added a commit to JasonGross/coq-packaging that referenced this pull request Aug 29, 2020

Add zarith after rocq-prover/rocq#11742

cf961fa

jashug mentioned this pull request Aug 30, 2020

Debug printers not getting installed #12945

Closed

spitters mentioned this pull request Jan 18, 2026

rocq-9.0v1 branch fails to build with OCaml 5.x: Unbound module Big_int smtcoq/smtcoq#160

Open

Conversation

ejgallego commented Mar 3, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ejgallego commented Mar 3, 2020

Uh oh!

ejgallego commented Mar 4, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ejgallego commented Mar 4, 2020

Uh oh!

maximedenes commented Mar 4, 2020

Uh oh!

maximedenes commented Mar 4, 2020

Uh oh!

ejgallego commented Mar 4, 2020

Uh oh!

maximedenes commented Mar 4, 2020

Uh oh!

ejgallego commented Mar 4, 2020

Uh oh!

ejgallego commented Mar 4, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ejgallego commented Mar 4, 2020

Uh oh!

liyishuai commented Aug 14, 2020

Uh oh!

maximedenes commented Aug 20, 2020

Uh oh!

ejgallego commented Aug 27, 2020

Uh oh!

maximedenes commented Aug 28, 2020

Uh oh!

coqbot-app Bot commented Aug 28, 2020

Uh oh!

maximedenes commented Aug 28, 2020

Uh oh!

RalfJung commented Aug 29, 2020

Uh oh!

RalfJung Aug 29, 2020

Choose a reason for hiding this comment

Uh oh!

bschommer commented Nov 11, 2020

Uh oh!

MSoegtropIMC commented Nov 11, 2020

Uh oh!

bschommer commented Nov 11, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ejgallego commented Nov 11, 2020

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

12 participants

ejgallego commented Mar 3, 2020 •

edited

Loading

ejgallego commented Mar 4, 2020 •

edited

Loading

ejgallego commented Mar 4, 2020 •

edited

Loading

bschommer commented Nov 11, 2020 •

edited

Loading