diff options
| -rw-r--r-- | Makefile.build | 5 | ||||
| -rw-r--r-- | configure.ml | 1 | ||||
| -rw-r--r-- | kernel/dune | 4 | ||||
| -rw-r--r-- | kernel/uint63.mli | 10 | ||||
| -rw-r--r-- | kernel/uint63_31.ml (renamed from kernel/uint63_i386_31.ml) | 0 | ||||
| -rw-r--r-- | kernel/uint63_63.ml (renamed from kernel/uint63_amd64_63.ml) | 0 | ||||
| -rw-r--r-- | kernel/write_uint63.ml | 38 |
7 files changed, 15 insertions, 43 deletions
diff --git a/Makefile.build b/Makefile.build index d1ed9a6f96..cfce870812 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 -w $@ ########################################################################### # Main targets (coqtop.opt, coqtop.byte) 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 () |