Merge PR #10488: Simplify picking between uint63_63.ml and uint63_31.ml + makefile fixes

Reviewed-by: ejgallego
Reviewed-by: vbgl

5 files changed, 12 insertions, 40 deletions

diff --git a/kernel/dune b/kernel/dune
index 4038bf5638..5f7502ef6b 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -3,7 +3,7 @@
  (synopsis "The Coq Kernel")
  (public_name coq.kernel)
  (wrapped false)
- (modules (:standard \ genOpcodeFiles uint63_i386_31 uint63_amd64_63 write_uint63))
+ (modules (:standard \ genOpcodeFiles uint63_31 uint63_63))
  (libraries lib byterun dynlink))
 
 (executable
@@ -16,7 +16,7 @@
 
 (rule
  (targets uint63.ml)
- (deps (:gen-file uint63_%{ocaml-config:architecture}_%{ocaml-config:int_size}.ml))
+ (deps (:gen-file uint63_%{ocaml-config:int_size}.ml))
  (action (copy# %{gen-file} %{targets})))
 
 (documentation
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index 5542716af2..d22ba3468f 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
 type t
 
 val uint_size : int
diff --git a/kernel/uint63_i386_31.ml b/kernel/uint63_31.ml
index b8eccd19fb..b8eccd19fb 100644
--- a/kernel/uint63_i386_31.ml
+++ b/kernel/uint63_31.ml
diff --git a/kernel/uint63_amd64_63.ml b/kernel/uint63_63.ml
index 5c4028e1c8..5c4028e1c8 100644
--- a/kernel/uint63_amd64_63.ml
+++ b/kernel/uint63_63.ml
diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml
deleted file mode 100644
index 57a170c8f5..0000000000
--- a/kernel/write_uint63.ml
+++ /dev/null
@@ -1,38 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Equivalent of rm -f *)
-let safe_remove f =
-  try Unix.chmod f 0o644; Sys.remove f with _ -> ()
-
-(** * Generate an implementation of 63-bit arithmetic *)
-let ml_file_copy input output =
-  safe_remove output;
-  let i = open_in input in
-  let o = open_out output in
-  let pr s = Printf.fprintf o s in
-  pr "(* DO NOT EDIT THIS FILE: automatically generated by ./write_uint63.ml *)\n";
-  pr "(* see uint63_amd64.ml and uint63_x86.ml *)\n";
-  try
-    while true do
-      output_string o (input_line i); output_char o '\n'
-    done
-  with End_of_file ->
-    close_in i;
-    close_out o;
-    Unix.chmod output 0o444
-
-let write_uint63 () =
-  ml_file_copy
-    (if max_int = 1073741823 (* 32-bits *) then "uint63_i386_31.ml"
-     else (* 64 bits *) "uint63_amd64_63.ml")
-    "uint63.ml"
-
-let () = write_uint63 ()