enable use of ocamldebug

debug_sail

@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+SAIL_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+SAIL_BC="$SAIL_DIR/_build/default/src/bin/sail.bc"
+if [ ! -f "$SAIL_BC" ]; then
+    echo "Unable to find debug build of sail, please build it first."
+    echo "  dune build --profile debug"
+    exit 1
+fi
+export SAIL_DIR
+export DUNE_DIR_LOCATIONS="libsail:share:$SAIL_DIR/_build/install/default/share/libsail"
+exec rlwrap ocamldebug $(bash -c "find . -iname '*.cmo' ; find . -iname '*.cma'" | xargs dirname | sort | uniq | sed 's/^\(.*\)$/-I \1/' | tr '\n' ' ') "$SAIL_BC" $*

src/bin/dune

@@ -10,6 +10,7 @@
 
 (executable
  (name sail)
+ (modes native byte)
  (public_name sail)
  (package sail)
  (link_flags -linkall)

src/bin/sail.ml

@@ -76,6 +76,7 @@ let opt_format_backup : string option ref = ref None
 let opt_format_only : string list ref = ref []
 let opt_format_skip : string list ref = ref []
 let opt_slice_instantiation_types : bool ref = ref false
+let is_bytecode = Sys.backend_type = Bytecode
 
 (* Allow calling all options as either -foo_bar, -foo-bar, or
    --foo-bar (for long options). The standard long-opt version
@@ -147,7 +148,7 @@ let add_target_header plugin opts =
 
 let load_plugin opts plugin =
   try
-    Dynlink.loadfile_private plugin;
+    if is_bytecode then Dynlink.loadfile plugin else Dynlink.loadfile_private plugin;
     let plugin_opts = Target.extract_options () |> fix_options |> target_align in
     opts := add_target_header plugin !opts @ plugin_opts
   with Dynlink.Error msg -> prerr_endline ("Failed to load plugin " ^ plugin ^ ": " ^ Dynlink.error_message msg)
@@ -583,6 +584,7 @@ let main () =
 
   options := Arg.align (fix_options !options);
 
+  let plugin_extension = if is_bytecode then ".cma" else ".cmxs" in
   begin
     match Sys.getenv_opt "SAIL_NO_PLUGINS" with
     | Some _ -> ()
@@ -592,7 +594,7 @@ let main () =
             List.iter
               (fun plugin ->
                 let path = Filename.concat dir plugin in
-                if Filename.extension plugin = ".cmxs" then load_plugin options path
+                if Filename.extension plugin = plugin_extension then load_plugin options path
               )
               (Array.to_list (Sys.readdir dir))
         | [] -> ()

src/lib/dune

@@ -107,5 +107,6 @@
  (name libsail)
  (public_name libsail)
  (libraries lem linksem pprint dune-site yojson menhirLib)
+ (modes byte native)
  (instrumentation
   (backend bisect_ppx)))

src/sail_c_backend/dune

@@ -1,12 +1,13 @@
 (executable
  (name sail_plugin_c)
  (modes
-  (native plugin))
+  (native plugin)
+  (byte plugin))
  (libraries libsail))
 
 (install
  (section
   (site
    (libsail plugins)))
  (package sail_c_backend)
- (files sail_plugin_c.cmxs))
+ (files sail_plugin_c.cmxs sail_plugin_c.cma))

src/sail_coq_backend/dune

@@ -9,12 +9,13 @@
 (executable
  (name sail_plugin_coq)
  (modes
-  (native plugin))
+  (native plugin)
+  (byte plugin))
  (libraries libsail))
 
 (install
  (section
   (site
    (libsail plugins)))
  (package sail_coq_backend)
- (files sail_plugin_coq.cmxs))
+ (files sail_plugin_coq.cmxs sail_plugin_coq.cma))

src/sail_doc_backend/dune

@@ -1,7 +1,8 @@
 (executable
  (name sail_plugin_doc)
  (modes
-  (native plugin))
+  (native plugin)
+  (byte plugin))
  (link_flags -linkall)
  (libraries libsail omd yojson base64)
  (embed_in_plugin_libraries omd base64))
@@ -11,4 +12,4 @@
   (site
    (libsail plugins)))
  (package sail_doc_backend)
- (files sail_plugin_doc.cmxs))
+ (files sail_plugin_doc.cmxs sail_plugin_doc.cma))

src/sail_latex_backend/dune

@@ -9,7 +9,8 @@
 (executable
  (name sail_plugin_latex)
  (modes
-  (native plugin))
+  (native plugin)
+  (byte plugin))
  (link_flags -linkall)
  (libraries libsail omd)
  (embed_in_plugin_libraries omd))
@@ -19,4 +20,4 @@
   (site
    (libsail plugins)))
  (package sail_latex_backend)
- (files sail_plugin_latex.cmxs))
+ (files sail_plugin_latex.cmxs sail_plugin_latex.cma))

src/sail_lean_backend/dune

@@ -9,12 +9,13 @@
 (executable
  (name sail_plugin_lean)
  (modes
-  (native plugin))
+  (native plugin)
+  (byte plugin))
  (libraries libsail))
 
 (install
  (section
   (site
    (libsail plugins)))
  (package sail_lean_backend)
- (files sail_plugin_lean.cmxs))
+ (files sail_plugin_lean.cmxs sail_plugin_lean.cma))

src/sail_lem_backend/dune

@@ -9,12 +9,13 @@
 (executable
  (name sail_plugin_lem)
  (modes
-  (native plugin))
+  (native plugin)
+  (byte plugin))
  (libraries libsail))
 
 (install
  (section
   (site
    (libsail plugins)))
  (package sail_lem_backend)
- (files sail_plugin_lem.cmxs))
+ (files sail_plugin_lem.cmxs sail_plugin_lem.cma))

src/sail_ocaml_backend/dune

@@ -9,7 +9,8 @@
 (executable
  (name sail_plugin_ocaml)
  (modes
-  (native plugin))
+  (native plugin)
+  (byte plugin))
  (link_flags -linkall)
  (libraries libsail base64)
  (embed_in_plugin_libraries base64))
@@ -19,4 +20,4 @@
   (site
    (libsail plugins)))
  (package sail_ocaml_backend)
- (files sail_plugin_ocaml.cmxs))
+ (files sail_plugin_ocaml.cmxs sail_plugin_ocaml.cma))

src/sail_output/dune

@@ -1,12 +1,13 @@
 (executable
  (name sail_plugin_output)
  (modes
-  (native plugin))
+  (native plugin)
+  (byte plugin))
  (libraries libsail))
 
 (install
  (section
   (site
    (libsail plugins)))
  (package sail_output)
- (files sail_plugin_output.cmxs))
+ (files sail_plugin_output.cmxs sail_plugin_output.cma))

src/sail_smt_backend/dune

@@ -9,12 +9,13 @@
 (executable
  (name sail_plugin_smt)
  (modes
-  (native plugin))
+  (native plugin)
+  (byte plugin))
  (libraries libsail))
 
 (install
  (section
   (site
    (libsail plugins)))
  (package sail_smt_backend)
- (files sail_plugin_smt.cmxs))
+ (files sail_plugin_smt.cmxs sail_plugin_smt.cma))

src/sail_sv_backend/dune

@@ -9,7 +9,8 @@
 (executable
  (name sail_plugin_sv)
  (modes
-  (native plugin))
+  (native plugin)
+  (byte plugin))
  (libraries libsail))
 
 (menhir
@@ -22,4 +23,4 @@
   (site
    (libsail plugins)))
  (package sail_sv_backend)
- (files sail_plugin_sv.cmxs))
+ (files sail_plugin_sv.cmxs sail_plugin_sv.cma))