Accumulators as functions and optionnal accumulators

.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-07-06-00242ff07f"
-  EDGE_CACHEKEY: "edge_ubuntu-V2026-07-06-62b9804f8c"
+  BASE_CACHEKEY: "old_ubuntu_lts-V2026-14-08-1c266a2665"
+  EDGE_CACHEKEY: "edge_ubuntu-V2026-14-08-e139ef8b6a"
   BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
   EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"
 
@@ -329,6 +329,9 @@ build:base+32bit:
     OPAM_VARIANT: "+32bit"
     COQ_EXTRA_CONF: "-native-compiler yes"
     ROCQIDE: "no"
+  artifacts:
+    paths:
+      - _build
   only: *full-ci
 
 build:edge+flambda:

clib/cUnix.ml

@@ -113,9 +113,9 @@ let run_command ?(hook=(fun _ ->())) c =
     (against whitespace or other funny chars in paths), hence no need
     to care about the different quoting conventions of /bin/sh and cmd.exe. *)
 
-let sys_command prog args =
+let sys_command ?(out_file_descr=Unix.stdout) prog args =
   let argv = Array.of_list (prog::args) in
-  let pid = Unix.create_process prog argv Unix.stdin Unix.stdout Unix.stderr in
+  let pid = Unix.create_process prog argv Unix.stdin out_file_descr Unix.stderr in
   waitpid_non_intr pid
 
 (*

clib/cUnix.mli

@@ -56,7 +56,7 @@ val run_command :
     (against whitespace or other funny chars in paths), hence no need
     to care about the different quoting conventions of /bin/sh and cmd.exe. *)
 
-val sys_command : string -> string list -> Unix.process_status
+val sys_command : ?out_file_descr:(Unix.file_descr) -> string -> string list -> Unix.process_status
 
 (** A version of [Unix.waitpid] immune to EINTR exceptions *)
 

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/bench/bench.sh

@@ -49,8 +49,8 @@ check_variable () {
 : "${old_coq_version:=dev}"
 : "${num_of_iterations:=1}"
 : "${timeout:=3h}"
-: "${coq_opam_packages:=rocq-stdlib rocq-bignums coq-hott coq-performance-tests-lite coq-engine-bench-lite rocq-elpi rocq-mathcomp-boot rocq-mathcomp-order rocq-mathcomp-ssreflect rocq-mathcomp-finite-group rocq-mathcomp-algebra rocq-mathcomp-solvable rocq-mathcomp-field rocq-mathcomp-group-representation coq-mathcomp-odd-order rocq-mathcomp-analysis coq-math-classes coq-corn coq-compcert rocq-equations rocq-metarocq-utils rocq-metarocq-common rocq-metarocq-template rocq-metarocq-pcuic rocq-metarocq-safechecker rocq-metarocq-erasure rocq-metarocq-translations coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto-with-bedrock coq-unimath coq-coquelicot coq-iris-examples coq-fourcolor coq-rewriter-perf-SuperFast coq-vst coq-category-theory coq-neural-net-interp-computed-lite}"
-: "${coq_native:=}"
+: "${coq_opam_packages:=rocq-stdlib rocq-bignums coq-hott coq-performance-tests-lite coq-engine-bench-lite rocq-elpi rocq-mathcomp-boot rocq-mathcomp-order rocq-mathcomp-ssreflect rocq-mathcomp-finite-group rocq-mathcomp-algebra rocq-mathcomp-solvable rocq-mathcomp-field rocq-mathcomp-group-representation coq-mathcomp-odd-order coq-mathcomp-analysis coq-math-classes coq-corn coq-compcert rocq-equations rocq-metarocq-utils rocq-metarocq-common rocq-metarocq-template rocq-metarocq-pcuic rocq-metarocq-safechecker rocq-metarocq-erasure rocq-metarocq-translations coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto-with-bedrock coq-unimath coq-coquelicot coq-iris-examples coq-fourcolor coq-rewriter-perf-SuperFast coq-vst coq-category-theory coq-neural-net-interp-computed-lite}"
+: "${coq_native:=1}"
 : "${auto_overlays:=1}"
 
 # example: coq-hott.dev git+https://github.com/some-user/coq-hott#some-branch
@@ -437,6 +437,8 @@ create_opam() {
     opam install -qy -j "$number_of_processors" $initial_opam_packages
     if [ ! -z "$BENCH_DEBUG" ]; then opam repo list; fi
 
+    opam pin add -qy -j "$number_of_processors" git+https://github.com/IBBXEF/malfunction#recusive_types
+
     cd "$coq_dir"
     echo "$1_coq_commit = $COQ_HASH"
 

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#5b5b625cd98e7cbd60325cc2634ee6cbab033236 && \
     opam clean -a -c
 
 # set the locale for the benefit of Python

dev/ci/docker/old_ubuntu_lts/Dockerfile

@@ -55,7 +55,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"
 
@@ -70,6 +70,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#5b5b625cd98e7cbd60325cc2634ee6cbab033236 && \
     opam clean -a -c && \
     find ~ '(' -name '*.cmt' -o -name '*.cmti' ')' -delete
 
@@ -81,6 +82,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#5b5b625cd98e7cbd60325cc2634ee6cbab033236 && \
     opam clean -a -c && \
     find ~ '(' -name '*.cmt' -o -name '*.cmti' ')' -delete
 

kernel/byterun/rocq_values.c

@@ -108,61 +108,3 @@ value rocq_tcode_array(value tcodes) {
   }
   CAMLreturn(res);
 }
-
-/* The rocq_curry2_1 function returns a pointer to some code that
-   immediately branches to caml_curry2_1. It can be used as field 0 of
-   an OCaml closure, as long as field 3 contains a closure whose code
-   pointer accepts exactly two arguments (the first argument is stored
-   in field 2).
-
-   Since the word before the branch indicates to the garbage collector
-   that this block should be ignored, the code pointer can be used
-   inside blocks that do not have tag 247. This 2043 value is the
-   result of Caml_out_of_heap_header(2, Abstract_tag).
-
-   Keep the compile-time checks in sync with rocq_configure.c */
-
-#ifdef NO_NATIVE_COMPUTE
-
-value rocq_curry2_1_addr(value v) {
-  return Val_unit;
-}
-
-#elif defined(NO_NAKED_POINTERS)
-
-__attribute__((weak))
-void caml_curry2_1() {
-  abort();
-}
-
-#if defined(__GNUC__) && defined(__amd64__)
-
-asm(".align 8\n\t"
-    ".quad 2043\n"
-    "rocq_curry2_1:\n\t"
-    "jmp caml_curry2_1\n");
-
-#elif defined(__GNUC__) && defined(__i386__)
-
-asm(".align 4\n\t"
-    ".long 2043\n"
-    "rocq_curry2_1:\n\t"
-    "jmp caml_curry2_1\n");
-
-#else
-#error "Unsupported architecture for native_compute."
-#endif
-
-value rocq_curry2_1_addr(value v) {
-  extern void rocq_curry2_1();
-  return (value)&rocq_curry2_1;
-}
-
-#else // not NO_NAKED_POINTERS
-
-value rocq_curry2_1_addr(value v) {
-  extern void caml_curry2_1() __attribute__((weak));
-  return (value)&caml_curry2_1;
-}
-
-#endif

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].