made native compilation compile to malfunction

.gitlab-ci.yml

@@ -40,8 +40,8 @@ variables:
   # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
   # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10)
   # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10)
-  BASE_CACHEKEY: "old_ubuntu_lts-V2026-06-10-d4125f9d9e"
-  EDGE_CACHEKEY: "edge_ubuntu-V2026-06-10-0c389ac2f4"
+  BASE_CACHEKEY: "old_ubuntu_lts-V2026-06-17-3f4ccef838"
+  EDGE_CACHEKEY: "edge_ubuntu-V2026-06-17-d451657c63"
   BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
   EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"
 

config/dune

@@ -28,4 +28,4 @@
    %{project_root}/dev/header.c
    ; Needed to generate include lists for coq_makefile
    plugin_list)
- (action (chdir %{project_root} (run %{project_root}/tools/configure/configure.exe -quiet -relocatable))))
+ (action (chdir %{project_root} (run %{project_root}/tools/configure/configure.exe -quiet -relocatable -native-compiler yes))))

dev/ci/docker/edge_ubuntu/Dockerfile

@@ -53,7 +53,7 @@ RUN mkdir -p ~/.config/dune && printf '(lang dune 2.1)\n(jobs %s)\n' $NJOBS > ~/
 
 # Edge opam is the set of edge packages required by Coq
 ENV COMPILER="4.14.2" \
-    BASE_OPAM="zarith.1.14 ounit2.2.2.7 camlzip.1.14" \
+    BASE_OPAM="zarith.1.14 ounit2.2.2.7 camlzip.1.14 ocaml-compiler-libs" \
     CI_OPAM="ocamlgraph.2.0.0 cppo.1.8.0" \
     BASE_OPAM_EDGE="dune.3.23.1 dune-build-info.3.23.1 dune-release.2.2.1 ocamlfind.1.9.8 odoc.3.2.1" \
     CI_OPAM_EDGE="memprof-limits.0.3.0 elpi.3.7.1 ppx_import.1.12.0 cmdliner.2.1.1 sexplib.v0.16.0 ppx_sexp_conv.v0.16.0 ppx_hash.v0.16.0 ppx_compare.v0.16.0 ppx_deriving_yojson.3.9.1 yojson.2.2.2 uri.4.4.0 ppx_yojson_conv.v0.16.0 ppx_inline_test.v0.16.1 ppx_assert.v0.16.0 ppx_optcomp.v0.16.0 lsp.1.26.0 sel.0.8.0" \
@@ -68,6 +68,7 @@ RUN opam init -a --disable-sandboxing --bare && eval $(opam env) && \
     opam repo add archive git+https://github.com/ocaml/opam-repository-archive && \
     opam update && \
     opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM $CI_OPAM_EDGE && \
+    opam pin add git+https://github.com/IBBXEF/malfunction#recusive_types && \
     opam clean -a -c
 
 # set the locale for the benefit of Python

dev/ci/docker/old_ubuntu_lts/Dockerfile

@@ -50,7 +50,7 @@ RUN mkdir -p ~/.config/dune && printf '(lang dune 2.1)\n(jobs %s)\n' $NJOBS > ~/
 ENV COMPILER="4.14.0"
 
 # Common OPAM packages
-ENV BASE_OPAM="zarith.1.11 ounit2.2.2.6 yojson.1.7.0 camlzip.1.10" \
+ENV BASE_OPAM="zarith.1.11 ounit2.2.2.6 yojson.1.7.0 camlzip.1.10 ocaml-compiler-libs" \
     CI_OPAM="ocamlgraph.2.0.0 cppo.1.6.9" \
     BASE_ONLY_OPAM="dune.3.21.1 stdlib-shims.0.1.0 ocamlfind.1.9.1 odoc.3.2.1 num.1.4"
 
@@ -65,6 +65,7 @@ RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opa
     opam repo add archive git+https://github.com/ocaml/opam-repository-archive && \
     opam update && \
     opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM $BASE_ONLY_OPAM && \
+    opam pin add git+https://github.com/IBBXEF/malfunction#recusive_types && \
     opam clean -a -c && \
     find ~ '(' -name '*.cmt' -o -name '*.cmti' ')' -delete
 
@@ -76,6 +77,7 @@ RUN opam switch create "${COMPILER}+32bit" \
     opam update && \
     i386 env CC='gcc -m32' opam install zarith.1.11 && \
     opam install $BASE_OPAM && \
+    opam pin add git+https://github.com/IBBXEF/malfunction#recusive_types && \
     opam clean -a -c && \
     find ~ '(' -name '*.cmt' -o -name '*.cmti' ')' -delete
 

kernel/float64.mli

@@ -34,6 +34,8 @@ val to_string : t -> string
 
 val compile : t -> string
 
+val compile_mlf : t -> string
+
 val of_float : float -> t
 
 (** All NaNs are normalized to [Stdlib.nan].

kernel/float64_common.ml

@@ -41,6 +41,15 @@ let of_string = float_of_string
 let compile f =
   Printf.sprintf "Float64.of_float (%s)" (to_hex_string f)
 
+  (* Compiles a float to malfunction code *)
+let compile_mlf f = (* malfunction does not support writing -1.1, so we have to be careful *)
+  if Float.is_nan f then "(apply (global $Float64 $of_float) nan)"
+  else if Float.is_infinite f then begin
+    if f < 0. then Printf.sprintf "(apply (global $Float64 $of_float) neg_infinity)"
+    else Printf.sprintf "(apply (global $Float64 $of_float) infinity)"
+  end else if f < 0. then Printf.sprintf "(apply (global $Float64 $of_float) (neg.f64 %.17e))" (-. f) (* malfunction supports scientific notation *)
+  else Printf.sprintf "(apply (global $Float64 $of_float) %.17e)" f
+
 let of_float f = f
 
 let to_float f = if is_nan f then nan else f

kernel/float64_common.mli

@@ -34,6 +34,8 @@ val to_string : t -> string
 
 val compile : t -> string
 
+val compile_mlf : t -> string
+
 val of_float : float -> t
 
 (** All NaNs are normalized to [Stdlib.nan].