[micromega] Switch from Big_int to ZArith.#8743
Merged
fajb merged 6 commits intorocq-prover:masterfrom Sep 16, 2020
Merged
Conversation
ejgallego
requested review from
Zimmi48,
herbelin,
mattam82,
maximedenes and
ppedrot
as code owners
ejgallego
added
kind: cleanup
ejgallego
force-pushed
the
zarith
branch
2 times, most recently
from
2a2f144 to
1294956
Compare
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
Contributor
Author
|
Take care of Nix if you want on the way. |
thery
reviewed
Oct 16, 2018
Contributor
|
is it ok with everybody if we add a new dependency (gmp)? |
Member
Note that we are just replacing dependencies by others. I would much prefer depending on ZArith + GMP than on Num. |
Contributor
|
Num was not the home cooked stuff by Valerie Menissier? gmp seems a bigger chunk |
Member
|
Here's what the This is a legacy library. It used to be part of the core OCaml distribution (in otherlibs/num) but is now distributed separately. New applications that need arbitrary-precision arithmetic should use the Zarith library (https://github.com/ocaml/Zarith) instead of the Num library, and older applications that already use Num are encouraged to switch to Zarith. Zarith delivers much better performance than Num and has a nicer API. |
Contributor
Author
|
@thery has a point in that the transition won't be fully pain-free. Also, I am not sure about the dependency of the frontend on |
Contributor
Author
|
Performance will be interesting, please add to the CI / Bench cool devs in that regard. |
Contributor
|
If the motivation is micromega, I am not sure it will make much difference but I can be wrong. |
This comment has been minimized.
This comment has been minimized.
Contributor
|
I am looking into it.
It does not seem so. Disabling caches does not solve the problem... |
ejgallego
commented
Sep 9, 2020
Contributor
Author
|
Ok one worrying failure: |
Contributor
Author
|
Gonna run a CI with #13002 added and without the debug code so we can bench and also get a complete CI. |
Contributor
Author
|
For perennial, the problem is: so likely some silly typo again. |
Contributor
Author
|
Ok, this seems finally ready for review and bench. Note that the issue in ocaml/Zarith#58 created some problems in testing, but none in practice; anyways we've added a workaround. Debug code lives in https://github.com/ejgallego/coq/tree/zarith%2Bdebug |
Contributor
|
There is still a problem with the .csdp.cache of the test-suite? |
Contributor
|
I don't remember how this is handled.
Is it supposed to be already there or regenerated?
It should be already there, named: `test-suite/.csdp.cache.test-suite`
|
Contributor
Author
|
The test suite is actually failing due to out of memory! It worked in my machine. Maybe some |
Contributor
Author
@fajb I updated that file, things were working fine in my machine, but indeed the memory consumption is strange as our test suite has noticed. Bench is over by the way: No significative change IMO. |
Contributor
|
@ejgallego the bench looks good. |
Contributor
Should we worry that the memory footprint of |
Contributor
Author
If not reproducible likely not; I don't know how to trigger a bench for 2 development only now tho. |
Contributor
|
@ejgallego No idea. I have never looked at memory consumption. |
Contributor
Author
Thanks, I've launched the CI.
Indeed it seems the OOM could maybe a problem with the csdp cache? Let see what the re-run says. |
soraros
reviewed
Sep 13, 2020
We still link num in `coqc` , that will be removed in a separate step. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
- merlin.in : added zarith - test-suite/Makefile remove .csdp.cache on make clean updated .csdp.cache.test-suite
In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in 1.10, see ocaml/Zarith#58
Contributor
Author
|
@fajb I think we are close to a fixpoint here, would you like to assign? |
fajb
approved these changes
Sep 15, 2020
Contributor
|
@ejgallego fixpoint, eventually! I'll merge as soon as the CI passes. |
Contributor
Author
Failure on coq_tools is spurious [failing everywhere] and not related to this PR. |
Contributor
|
@ejgallego well done. |
Contributor
Author
|
Thanks @fajb ! |
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
13 participants
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.
We replace micromega use of Num by Zarith.