Skip to content

Commit

Permalink
declare some externals in .ml file in dune library "coqrun"
Browse files Browse the repository at this point in the history
this seems to be enough to ensure the C code gets included in the cmxs
  • Loading branch information
SkySkimmer committed Dec 2, 2024
1 parent c6d6537 commit 8555b11
Show file tree
Hide file tree
Showing 2 changed files with 35 additions and 0 deletions.
35 changes: 35 additions & 0 deletions kernel/byterun/rocq_vm_externals.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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) *)
(************************************************************************)

[@@@warning "-32"]

(** We need to declare an external from each C file to convince ocaml
to include the C code in the cmxs for dynlink.
NB: it seems in practice we don't actually need one from each C
file, I guess if we have a.c and b.c and declare an external from
b.c whose implementation involves a.c it is enough to work.
*)

(* rocq_fix_code.c *)
external accumulate : unit -> Obj.t = "rocq_accumulate"

(* rocq_interp.c *)
external push_val : Obj.t -> unit = "rocq_push_val"

(* rocq_values.c *)
external is_accumulate : Obj.t -> bool = "rocq_is_accumulate_code"

(* rocq_float64.c *)
external mul : float -> float -> float = "rocq_fmul_byte" "rocq_fmul"
[@@unboxed] [@@noalloc]

(* rocq_memory.c *)
external init_vm : unit -> unit = "init_rocq_vm"
Empty file.

0 comments on commit 8555b11

Please sign in to comment.