Port native_compute to OCaml 5.

Author: silene

kernel/byterun/coq_values.c

@@ -107,13 +107,20 @@ value coq_tcode_array(value tcodes) {
   CAMLreturn(res);
 }
 
-CAMLprim value coq_obj_set_tag (value arg, value new_tag)
-{
-#if OCAML_VERSION >= 50000
-// Placeholder used by native_compute
-  abort();
-#else
-  Tag_val (arg) = Int_val (new_tag);
-#endif
-  return Val_unit;
+code_t coq_accumulate_addr;
+
+value coq_proxy_accu(value clos) {
+  value v;
+  CAMLassert(Tag_val(clos) == Closure_tag && Wosize_val(clos) == 3);
+  coq_accumulate_addr = Code_val(clos);
+  asm("jmp 1f\n\t"
+      ".align 8\n\t"
+      ".quad 2816\n"
+      "2:\n\t"
+      "mov coq_accumulate_addr@GOTPCREL(%%rip), %%r8\n\t"
+      "jmp *(%%r8)\n"
+      "1:\n\t"
+      "lea 2b(%%rip), %0\n\t"
+      : "=r"(v));
+  return v;
 }

kernel/nativevalues.ml

@@ -121,23 +121,30 @@ let ret_accu = Obj.repr (ref ())
 
 type accu_val = { mutable acc_atm : atom; acc_arg : t list }
 
-external set_tag : Obj.t -> int -> unit = "coq_obj_set_tag"
-
-let mk_accu (a : atom) : t =
-  let rec accumulate data x =
-    if Obj.repr x == ret_accu then Obj.repr data
-    else
-      let data = { data with acc_arg = x :: data.acc_arg } in
-      let ans = Obj.repr (accumulate data) in
-      let () = set_tag ans accumulate_tag in
-      ans
-  in
-  let acc = { acc_atm = a; acc_arg = [] } in
-  let ans = Obj.repr (accumulate acc) in
-  (** FIXME: use another representation for accumulators, this causes naked
-      pointers. *)
-  let () = set_tag ans accumulate_tag in
-  (Obj.obj ans : t)
+(** Returns a pointer to the code of a partial application of [accumulate], yet also recognized as an unscannable block *)
+external get_proxy_accu : (t -> t) -> Obj.t = "coq_proxy_accu"
+
+[@@@warning "-69"]
+type accu_clos = { clos_addr : Obj.t; clos_arity : int; clos_env : Obj.t }
+
+let proxy_accu = ref None
+
+let mk_accu data =
+  let ans = { clos_addr = Option.get !proxy_accu; clos_arity = 2; clos_env = Obj.repr data } in
+  (* [ans] is indistinguishable from [accumulate data] *)
+  (Obj.magic ans : t)
+
+let accumulate data x =
+  if Obj.repr x == ret_accu then (Obj.magic data : t)
+  else mk_accu { data with acc_arg = x :: data.acc_arg }
+
+let () =
+  let data = Obj.magic (ref ()) in
+  proxy_accu := Some (get_proxy_accu (fun x -> accumulate data x))
+
+let mk_accu a : t =
+  let data = { acc_atm = a; acc_arg = [] } in
+  mk_accu data
 
 let get_accu (k : accumulator) =
   (Obj.magic k : Obj.t -> accu_val) ret_accu

tools/configure/configure.ml

@@ -101,10 +101,7 @@ let caml_version_nums { CamlConf.caml_version; _ } =
   generic_version_nums ~name:"the OCaml compiler" caml_version
 
 let check_caml_version prefs caml_version caml_version_nums =
-  if caml_version_nums >= [5;0;0] && prefs.nativecompiler <> NativeNo then
-    let () = cprintf prefs "Your version of OCaml is %s." caml_version in
-    die "You have enabled Coq's native compiler, however it is not compatible with OCaml >= 5.0.0"
-  else if caml_version_nums >= [4;9;0] then
+  if caml_version_nums >= [4;9;0] then
     cprintf prefs "You have OCaml %s. Good!" caml_version
   else
     let () = cprintf prefs "Your version of OCaml is %s." caml_version in