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

Reviewed-by: ejgallego
Reviewed-by: vbgl

8 files changed, 21 insertions, 60 deletions

diff --git a/Makefile.build b/Makefile.build
index d1ed9a6f96..610af5fe40 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -396,9 +396,8 @@ doc_gram_rsts: doc/tools/docgram/orderedGrammar
 ###########################################################################
 # Specific rules for Uint63
 ###########################################################################
-kernel/uint63.ml: kernel/write_uint63.ml kernel/uint63_i386_31.ml kernel/uint63_amd64_63.ml
-	$(SHOW)'WRITE $@'
-	$(HIDE)(cd kernel && ocaml unix.cma $(shell basename $<))
+kernel/uint63.ml: kernel/uint63_$(OCAML_INT_SIZE).ml
+	rm -f $@ && cp $< $@ && chmod a-w $@
 
 ###########################################################################
 # Main targets (coqtop.opt, coqtop.byte)
@@ -642,12 +641,6 @@ gramlib/.pack/gramlib__G%: gramlib/g% | gramlib/.pack
 # Specific rules for gramlib to pack it Dune / OCaml 4.08 style
 GRAMOBJS=$(addsuffix .cmo, $(GRAMFILES))
 
-gramlib/.pack/%: COND_BYTEFLAGS+=-no-alias-deps -w -49
-gramlib/.pack/%: COND_OPTFLAGS+=-no-alias-deps -w -49
-
-gramlib/.pack/gramlib.%: COND_OPENFLAGS=
-gramlib/.pack/gramlib__%: COND_OPENFLAGS=-open Gramlib
-
 gramlib/.pack/gramlib.cma: $(GRAMOBJS) gramlib/.pack/gramlib.cmo
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $^
@@ -701,14 +694,15 @@ kernel/kernel.cmxa: kernel/kernel.mllib
 COND_IDEFLAGS=$(if $(filter ide/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,)
 COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,)
 
-# For module packing
-COND_OPENFLAGS=
+COND_GRAMFLAGS=$(if $(filter gramlib/.pack/%,$<),-no-alias-deps -w -49,) $(if $(filter gramlib/.pack/gramlib__%,$<),-open Gramlib,)
+
+COND_KERFLAGS=$(if $(filter kernel/%,$<),-w +a-4-44-50,)
 
 COND_BYTEFLAGS= \
- $(COND_IDEFLAGS) $(COND_PRINTERFLAGS) $(MLINCLUDES) $(BYTEFLAGS) $(COND_OPENFLAGS)
+ $(COND_IDEFLAGS) $(COND_PRINTERFLAGS) $(MLINCLUDES) $(BYTEFLAGS) $(COND_GRAMFLAGS) $(COND_KERFLAGS)
 
 COND_OPTFLAGS= \
- $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS) $(COND_OPENFLAGS)
+ $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS) $(COND_GRAMFLAGS) $(COND_KERFLAGS)
 
 plugins/micromega/%.cmi: plugins/micromega/%.mli
 	$(SHOW)'OCAMLC    $<'
@@ -718,8 +712,6 @@ plugins/nsatz/%.cmi: plugins/nsatz/%.mli
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $<
 
-kernel/%.cmi: COND_BYTEFLAGS+=-w +a-4-44-50
-
 %.cmi: %.mli
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<
@@ -732,8 +724,6 @@ plugins/nsatz/%.cmo: plugins/nsatz/%.ml
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $<
 
-kernel/%.cmo: COND_BYTEFLAGS+=-w +a-4-44-50
-
 %.cmo: %.ml
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<
@@ -783,8 +773,6 @@ user-contrib/%.cmx: user-contrib/%.ml
 	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $<
 
-kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50
-
 %.cmx: %.ml
 	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $<
diff --git a/Makefile.ide b/Makefile.ide
index cb026cdf43..0a11f83a18 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -121,7 +121,7 @@ $(COQIDEBYTE): $(LINKIDE)
 ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile
 	@rm -f $@
 	cp $< $@
-	@chmod -w $@
+	@chmod a-w $@
 
 ide/%.cmi: ide/%.mli
 	$(SHOW)'OCAMLC    $<'
diff --git a/configure.ml b/configure.ml
index 3ced82718e..cef4faaf1a 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1141,6 +1141,7 @@ let write_makefile f =
   pr "# Your architecture\n";
   pr "# Can be obtain by UNIX command arch\n";
   pr "ARCH=%s\n" arch;
+  pr "OCAML_INT_SIZE:=%d\n" Sys.int_size;
   pr "HASNATDYNLINK=%s\n\n" natdynlinkflag;
   pr "# Supplementary libs for some systems, currently:\n";
   pr "#  . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket\n";
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 ()