From 85987b12f9b9a9635b407eb76fcdfbd944bcad62 Mon Sep 17 00:00:00 2001 From: John Harrison Date: Fri, 5 Apr 2024 20:27:12 +0000 Subject: [PATCH] Fixed a few things that break after the removal of explicit module identifiers, adding a "float_fabs" binding for the absolute value function on floating-point numbers. Fixed a long-standing problem in the Mizarlight Makefile by using ocamlfind to find camlp5 - this in turn can be installed in an Opam setting by "opam install ocamlfind", and is anyway already used in the main "hol.ml" root file for recent OCamls. --- Formal_ineqs/informal/informal_exp.hl | 2 +- Jordan/float.ml | 4 ++-- Mizarlight/Makefile | 2 +- hol.ml | 10 +++++++--- 4 files changed, 11 insertions(+), 7 deletions(-) diff --git a/Formal_ineqs/informal/informal_exp.hl b/Formal_ineqs/informal/informal_exp.hl index 5210e3de..d863bd06 100644 --- a/Formal_ineqs/informal/informal_exp.hl +++ b/Formal_ineqs/informal/informal_exp.hl @@ -130,7 +130,7 @@ let exp_high_raw pp x = exp_neg_high_raw pp (abs_float x);; let reduce_float x = - let f = abs_float (float_of_ifloat x) in + let f = float_fabs (float_of_ifloat x) in if f <= exp_max_x then false, 0 else diff --git a/Jordan/float.ml b/Jordan/float.ml index 362aa334..29a30628 100644 --- a/Jordan/float.ml +++ b/Jordan/float.ml @@ -1136,7 +1136,7 @@ let (round_outward_float: int -> float -> Num.num) = fun bprec f -> if (f=0.0) then (num 0) else begin - let b = abs_float f in + let b = float_fabs f in let sign = if (f >= 0.0) then I else minus_num in let (x,n) = frexp b in let u = int_of_float( ceil (ldexp x bprec)) in @@ -1149,7 +1149,7 @@ let (round_inward_float: int -> float -> Num.num) = begin (* avoid overflow on 30 bit integers *) let bprec = if (bprec > 25) then 25 else bprec in - let b = abs_float f in + let b = float_fabs f in let sign = if (f >= 0.0) then I else minus_num in let (x,n) = frexp b in let u = int_of_float( floor (ldexp x bprec)) in diff --git a/Mizarlight/Makefile b/Mizarlight/Makefile index a281e506..6fe01e46 100644 --- a/Mizarlight/Makefile +++ b/Mizarlight/Makefile @@ -6,7 +6,7 @@ pa_f.cmo: pa_f.ml; if test `ocamlc -version | cut -c1-3` = "3.0" ; \ then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I +camlp4 pa_f.ml; \ - else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_f.ml; \ + else ocamlfind ocamlc -package camlp5 -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_f.ml; \ fi clean:; rm -f pa_f.cmi pa_f.cmo diff --git a/hol.ml b/hol.ml index 0132fe69..4ff6f2be 100644 --- a/hol.ml +++ b/hol.ml @@ -103,12 +103,16 @@ then loads "bignum_zarith.ml" else loads "bignum_num.ml";; (* ------------------------------------------------------------------------- *) -(* Bind this to a name that is independent of OCaml versions before it *) -(* is potentially overwritten by a theorem of the same name. On older *) -(* OCaml versions it is "Pervasives.sqrt", and on newer ones "Float.sqrt". *) +(* Bind these to names that are independent of OCaml versions before they *) +(* are potentially overwritten by an identifier of the same name. In older *) +(* and newer Ocaml versions these are respectively: *) +(* *) +(* Pervasives.sqrt -> Float.sqrt *) +(* Pervasives.abs_float -> Stdlib.abs_float / Float.abs *) (* ------------------------------------------------------------------------- *) let float_sqrt = sqrt;; +let float_fabs = abs_float;; (* ------------------------------------------------------------------------- *) (* Various tweaks to OCaml and general library functions. *)