From 6b117c0b2c969a809e3762145de23431768a76f2 Mon Sep 17 00:00:00 2001
From: NikolajBjorner <nbjorner@microsoft.com>
Date: Mon, 23 Sep 2019 02:45:20 -0700
Subject: [PATCH] move to zarith #2471

Signed-off-by: NikolajBjorner <nbjorner@microsoft.com>
---
 scripts/mk_util.py | 13 ++++++-------
 src/api/ml/META.in |  2 +-
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 54ad7f6d8..0d2d70d84 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1955,9 +1955,8 @@ class MLComponent(Component):
                 OCAML_FLAGS += '-g'
 
             if OCAMLFIND:
-                # Load Big_int, which is no longer part of the standard library, via the num package: https://github.com/ocaml/num
-                OCAMLCF = OCAMLFIND + ' ' + 'ocamlc -package num' + ' ' + OCAML_FLAGS
-                OCAMLOPTF = OCAMLFIND + ' ' + 'ocamlopt -package num' + ' ' + OCAML_FLAGS
+                OCAMLCF = OCAMLC + ' ' + 'ocamlc -package zarith' + ' ' + OCAML_FLAGS
+                OCAMLOPTF = OCAMLOPT + ' ' + 'ocamlopt -package zarith' + ' ' + OCAML_FLAGS
             else:
                 OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
                 OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS
@@ -2285,7 +2284,7 @@ class MLExampleComponent(ExampleComponent):
             out.write('\t%s ' % OCAMLC)
             if DEBUG_MODE:
                 out.write('-g ')
-            out.write('-custom -o ml_example.byte -I api/ml -cclib "-L. -lz3" nums.cma z3ml.cma')
+            out.write('-custom -o ml_example.byte -I -zarith -I api/ml -cclib "-L. -lz3" zarith.cma z3ml.cma')
             for mlfile in get_ml_files(self.ex_dir):
                 out.write(' %s/%s' % (self.to_ex_dir, mlfile))
             out.write('\n')
@@ -2296,7 +2295,7 @@ class MLExampleComponent(ExampleComponent):
             out.write('\t%s ' % OCAMLOPT)
             if DEBUG_MODE:
                 out.write('-g ')
-            out.write('-o ml_example$(EXE_EXT) -I api/ml -cclib "-L. -lz3" nums.cmxa z3ml.cmxa')
+            out.write('-o ml_example$(EXE_EXT) -I -zarith -I api/ml -cclib "-L. -lz3" zarith.cmxa z3ml.cmxa')
             for mlfile in get_ml_files(self.ex_dir):
                 out.write(' %s/%s' % (self.to_ex_dir, mlfile))
             out.write('\n')
@@ -2619,11 +2618,11 @@ def mk_config():
         config.write('LINK=%s\n' % CXX)
         config.write('LINK_FLAGS=\n')
         config.write('LINK_OUT_FLAG=-o \n')
-        config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS)
+        config.write('LINK_EXTRA_FLAGS=-Wl,--whole-archive -lpthread -Wl,--no-whole-archive %s\n' % LDFLAGS)
         config.write('SO_EXT=%s\n' % SO_EXT)
         config.write('SLINK=%s\n' % CXX)
         config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS)
-        config.write('SLINK_EXTRA_FLAGS=-lpthread %s\n' % SLIBEXTRAFLAGS)
+        config.write('SLINK_EXTRA_FLAGS=-Wl,--whole-archive -lpthread -Wl,--no-whole-archive %s\n' % SLIBEXTRAFLAGS)
         config.write('SLINK_OUT_FLAG=-o \n')
         config.write('OS_DEFINES=%s\n' % OS_DEFINES)
         if is_verbose():
diff --git a/src/api/ml/META.in b/src/api/ml/META.in
index e58ebf722..bda80fdc4 100644
--- a/src/api/ml/META.in
+++ b/src/api/ml/META.in
@@ -1,7 +1,7 @@
 # META file for the "z3" package:
 version = "@VERSION@"
 description = "Z3 Theorem Prover (OCaml API)"
-requires = "num threads"
+requires = "zarith threads"
 archive(byte) = "z3ml.cma"
 archive(native) = "z3ml.cmxa"
 archive(byte,plugin) = "z3ml.cma"