diff --git a/dune-project b/dune-project
index d7d4e27a0..2c994dd03 100644
--- a/dune-project
+++ b/dune-project
@@ -48,7 +48,6 @@ http://www.cl.cam.ac.uk/~pes20/sail/.
   (depends
     (dune-site (>= 3.0.2))
     (menhir :build)
-    (sail_manifest (and (= :version) :build))
     (ott (and (>= 0.28) :build))
     (lem (>= "2018-12-14"))
     (linksem (>= "0.3"))
@@ -116,6 +115,7 @@ http://www.cl.cam.ac.uk/~pes20/sail/.
 ")
   (depends
     (libsail (= :version))
+    (sail_manifest (and (= :version) :build))
     (sail_ocaml_backend (and (= :version) :post))
     (sail_c_backend (and (= :version) :post))
     (sail_smt_backend (and (= :version) :post))
diff --git a/libsail.opam b/libsail.opam
index b6b4ddf44..bf39dc9de 100644
--- a/libsail.opam
+++ b/libsail.opam
@@ -32,7 +32,6 @@ depends: [
   "dune" {>= "3.0"}
   "dune-site" {>= "3.0.2"}
   "menhir" {build}
-  "sail_manifest" {= version & build}
   "ott" {>= "0.28" & build}
   "lem" {>= "2018-12-14"}
   "linksem" {>= "0.3"}
@@ -59,4 +58,3 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/rems-project/sail.git"
-substs: [ "src/lib/manifest.ml" ]
diff --git a/libsail.opam.template b/libsail.opam.template
deleted file mode 100644
index 626081053..000000000
--- a/libsail.opam.template
+++ /dev/null
@@ -1 +0,0 @@
-substs: [ "src/lib/manifest.ml" ]
diff --git a/sail.opam b/sail.opam
index 1940f550d..1b78d6f66 100644
--- a/sail.opam
+++ b/sail.opam
@@ -31,6 +31,7 @@ bug-reports: "https://github.com/rems-project/sail/issues"
 depends: [
   "dune" {>= "3.0"}
   "libsail" {= version}
+  "sail_manifest" {= version & build}
   "sail_ocaml_backend" {= version & post}
   "sail_c_backend" {= version & post}
   "sail_smt_backend" {= version & post}
@@ -58,3 +59,4 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/rems-project/sail.git"
+substs: [ "src/bin/manifest.ml" ]
diff --git a/sail.opam.template b/sail.opam.template
new file mode 100644
index 000000000..9a4015580
--- /dev/null
+++ b/sail.opam.template
@@ -0,0 +1 @@
+substs: [ "src/bin/manifest.ml" ]
diff --git a/src/bin/dune b/src/bin/dune
index de1564655..28fa2aecd 100644
--- a/src/bin/dune
+++ b/src/bin/dune
@@ -2,6 +2,14 @@
   (dev
     (flags (:standard -w -33))))
 
+(rule
+  (target manifest.ml)
+  (mode fallback)
+  (action
+    (with-outputs-to %{target}
+      (chdir %{workspace_root}
+        (run sail_manifest -gen_manifest)))))
+
 (executable
   (name sail)
   (public_name sail)
@@ -14,6 +22,9 @@
   (section share)
   (package sail)
   (files
+    (%{workspace_root}/src/lib/util.ml as src/lib/util.ml)
+    (%{workspace_root}/src/lib/sail_lib.ml as src/lib/sail_lib.ml)
+    (%{workspace_root}/src/lib/elf_loader.ml as src/lib/elf_loader.ml)
     (%{workspace_root}/lib/_tags as lib/_tags)
     (%{workspace_root}/lib/_tags_coverage as lib/_tags_coverage)
     (%{workspace_root}/lib/arith.sail as lib/arith.sail)
diff --git a/src/bin/manifest.ml.in b/src/bin/manifest.ml.in
new file mode 100644
index 000000000..fe3a3cf46
--- /dev/null
+++ b/src/bin/manifest.ml.in
@@ -0,0 +1,7 @@
+let dir = "%{sail:share}%"
+
+let commit = "opam-v%{opam-version}%"
+
+let branch = "%{sail:name}%"
+
+let version = "%{sail:version}%"
diff --git a/src/bin/repl.ml b/src/bin/repl.ml
index 8db396905..44c44733a 100644
--- a/src/bin/repl.ml
+++ b/src/bin/repl.ml
@@ -91,32 +91,36 @@ type istate = {
     options : (Arg.key * Arg.spec * Arg.doc) list;
     mode : mode;
     clear : bool;
-    state : Interpreter.lstate * Interpreter.gstate
+    state : Interpreter.lstate * Interpreter.gstate;
+    default_sail_dir : string;
   }
 
 let shrink_istate istate = ({
     ast = istate.ast;
     effect_info = istate.effect_info;
-    env = istate.env
+    env = istate.env;
+    default_sail_dir = istate.default_sail_dir;
   } : Interactive.istate)
                         
 let initial_istate options env effect_info ast = {
     ast = ast;
     effect_info = effect_info;
     env = env;
-    ref_state = ref (Interactive.initial_istate ());
+    ref_state = ref (Interactive.initial_istate Manifest.dir);
     vs_ids = ref (val_spec_ids ast.defs);
     options = options;
     mode = Normal;
     clear = true;
-    state = initial_state ~registers:false empty_ast Type_check.initial_env !Value.primops
+    state = initial_state ~registers:false empty_ast Type_check.initial_env !Value.primops;
+    default_sail_dir = Manifest.dir;
   }
 
 let setup_interpreter_state istate =
   istate.ref_state := {
       ast = istate.ast;
       effect_info = istate.effect_info;
-      env = istate.env
+      env = istate.env;
+      default_sail_dir = istate.default_sail_dir
     };
   { istate with state = initial_state istate.ast istate.env !Value.primops }
 
@@ -170,7 +174,7 @@ let () =
     load_binary addr filename
   ))) |> register_command ~name:"bin" ~help:"Load a raw binary file at :0. Use :elf to load an ELF";
 
-  ActionUnit (fun _ -> print_endline (Reporting.get_sail_dir ()))
+  ActionUnit (fun istate -> print_endline (Reporting.get_sail_dir istate.default_sail_dir))
   |> register_command ~name:"sail_dir" ~help:"print Sail directory location"
 
 (* This is a feature that lets us take interpreter commands like :foo
@@ -557,7 +561,7 @@ let handle_input' istate input =
               failwith "Invalid arguments for :let";
            end
         | ":def" ->
-           let ast = Initial_check.ast_of_def_string_with __POS__ (Preprocess.preprocess None istate.options) arg in
+           let ast = Initial_check.ast_of_def_string_with __POS__ (Preprocess.preprocess istate.default_sail_dir None istate.options) arg in
            let ast, env = Type_check.check istate.env ast in
            { istate with ast = append_ast istate.ast ast; env = env }
         | ":rewrite" ->
diff --git a/src/bin/sail.ml b/src/bin/sail.ml
index faa4c6e8d..685618dcb 100644
--- a/src/bin/sail.ml
+++ b/src/bin/sail.ml
@@ -258,11 +258,11 @@ let rec options = ref ([
 ])
 
 let register_default_target () =
-  Target.register ~name:"default" (fun _ _ _ _ -> ())
+  Target.register ~name:"default" (fun _ _ _ _ _ -> ())
   
 let run_sail tgt =
   Target.run_pre_parse_hook tgt ();
-  let ast, env, effect_info = Frontend.load_files ~target:tgt !options Type_check.initial_env !opt_file_arguments in
+  let ast, env, effect_info = Frontend.load_files ~target:tgt Manifest.dir !options Type_check.initial_env !opt_file_arguments in
   let ast, env = Frontend.descatter effect_info env ast in
   let ast, env =
     List.fold_right (fun file (ast, _) -> Splice.splice ast file)
@@ -274,7 +274,7 @@ let run_sail tgt =
   Target.run_pre_rewrites_hook tgt ast effect_info env;
   let ast, effect_info, env = Rewrites.rewrite effect_info env (Target.rewrites tgt) ast in
 
-  Target.action tgt !opt_file_out ast effect_info env;
+  Target.action tgt Manifest.dir !opt_file_out ast effect_info env;
 
   (ast, env, effect_info)
 
@@ -322,7 +322,7 @@ let main () =
   );
 
   if !opt_show_sail_dir then (
-    print_endline (Reporting.get_sail_dir ());
+    print_endline (Reporting.get_sail_dir Manifest.dir);
     exit 0
   );
  
diff --git a/src/lib/dune b/src/lib/dune
index 06b664fc0..00f769eeb 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -49,14 +49,6 @@
     (progn (run lem -ocaml %{jib} -lib . -lib lem/)
            (run sed -i.bak -f %{sed} %{target}))))
 
-(rule
-  (target manifest.ml)
-  (mode fallback)
-  (action
-    (with-outputs-to %{target}
-      (chdir %{workspace_root}
-        (run sail_manifest -gen_manifest)))))
-
 (menhir
   (modules parser))
 
@@ -70,34 +62,3 @@
   (name libsail)
   (public_name libsail)
   (libraries lem linksem pprint dune-site))
-
-(install
-  (section share)
-  (package libsail)
-  (files
-    (util.ml as src/lib/util.ml)
-    (sail_lib.ml as src/lib/sail_lib.ml)
-    (elf_loader.ml as src/lib/elf_loader.ml)
-    (%{workspace_root}/lib/flow.sail as lib/flow.sail)
-    (%{workspace_root}/lib/vector_dec.sail as lib/vector_dec.sail)
-    (%{workspace_root}/lib/vector_inc.sail as lib/vector_inc.sail)
-    (%{workspace_root}/lib/arith.sail as lib/arith.sail)
-    (%{workspace_root}/lib/elf.sail as lib/elf.sail)
-    (%{workspace_root}/lib/real.sail as lib/real.sail)
-    (%{workspace_root}/lib/option.sail as lib/option.sail)
-    (%{workspace_root}/lib/result.sail as lib/result.sail)
-    (%{workspace_root}/lib/mapping.sail as lib/mapping.sail)
-    (%{workspace_root}/lib/isla.sail as lib/isla.sail)
-    (%{workspace_root}/lib/regfp.sail as lib/regfp.sail)
-    (%{workspace_root}/lib/smt.sail as lib/smt.sail)
-    (%{workspace_root}/lib/string.sail as lib/string.sail)
-    (%{workspace_root}/lib/float.sail as lib/float.sail)
-    (%{workspace_root}/lib/mono_rewrites.sail as lib/mono_rewrites.sail)
-    (%{workspace_root}/lib/generic_equality.sail as lib/generic_equality.sail)
-    (%{workspace_root}/lib/trace.sail as lib/trace.sail)
-    (%{workspace_root}/lib/instr_kinds.sail as lib/instr_kinds.sail)
-    (%{workspace_root}/lib/exception_basic.sail as lib/exception_basic.sail)
-    (%{workspace_root}/lib/reverse_endianness.sail as lib/reverse_endianness.sail)
-    (%{workspace_root}/lib/concurrency_interface.sail as lib/concurrency_interface.sail)
-    (%{workspace_root}/lib/concurrency_interface/v1.sail as lib/concurrency_interface/v1.sail)
-    (%{workspace_root}/lib/prelude.sail as lib/prelude.sail)))
diff --git a/src/lib/frontend.ml b/src/lib/frontend.ml
index a0a09d29b..b53e6746c 100644
--- a/src/lib/frontend.ml
+++ b/src/lib/frontend.ml
@@ -83,14 +83,14 @@ let check_ast (asserts_termination : bool) (env : Type_check.Env.t) (ast : unit
   let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_ast stdout ast else () in
   (ast, env, side_effects)
  
-let load_files ?target:target options type_envs files =
+let load_files ?target:target default_sail_dir options type_envs files =
   let t = Profile.start () in
 
   let parsed_files = List.map (fun f -> (f, Initial_check.parse_file f)) files in
 
   let comments = List.map (fun (f, (comments, _)) -> (f, comments)) parsed_files in
   let target_name = Option.map Target.name target in
-  let ast = Parse_ast.Defs (List.map (fun (f, (_, file_ast)) -> (f, Preprocess.preprocess target_name options file_ast)) parsed_files) in
+  let ast = Parse_ast.Defs (List.map (fun (f, (_, file_ast)) -> (f, Preprocess.preprocess default_sail_dir target_name options file_ast)) parsed_files) in
   let ast = Initial_check.process_ast ~generate:true ast in
   let ast = { ast with comments = comments } in
   
diff --git a/src/lib/frontend.mli b/src/lib/frontend.mli
index 2153a733d..b93d981c8 100644
--- a/src/lib/frontend.mli
+++ b/src/lib/frontend.mli
@@ -76,6 +76,7 @@ val check_ast : bool -> Type_check.Env.t -> unit ast -> Type_check.tannot ast *
    
 val load_files :
   ?target:Target.target ->
+  string ->
   (Arg.key * Arg.spec * Arg.doc) list ->
   Type_check.Env.t ->
   string list ->
diff --git a/src/lib/interactive.ml b/src/lib/interactive.ml
index 503997124..784106a44 100644
--- a/src/lib/interactive.ml
+++ b/src/lib/interactive.ml
@@ -76,12 +76,14 @@ type istate = {
     ast : Type_check.tannot ast;
     effect_info : Effects.side_effect_info;
     env : Type_check.Env.t;
+    default_sail_dir : string;
   }
 
-let initial_istate () = {
+let initial_istate default_sail_dir = {
     ast = empty_ast;
     effect_info = Effects.empty_side_effect_info;
     env = Type_check.initial_env;
+    default_sail_dir = default_sail_dir;
   }
  
 let arg str =
diff --git a/src/lib/interactive.mli b/src/lib/interactive.mli
index 1d2703bff..c1c6e9726 100644
--- a/src/lib/interactive.mli
+++ b/src/lib/interactive.mli
@@ -72,14 +72,16 @@ open Type_check
 val opt_interactive : bool ref
 
 (** Each interactive command is passed this struct, containing the
-   abstract syntax tree, effect into and the type-checking environment *)
+   abstract syntax tree, effect into and the type-checking
+   environment. Also contains the default Sail directory *)
 type istate = {
     ast : Type_check.tannot ast;
     effect_info : Effects.side_effect_info;
     env : Type_check.Env.t;
+    default_sail_dir : string;
   }
 
-val initial_istate : unit -> istate
+val initial_istate : string -> istate
 
 val arg : string -> string
 val command : string -> string
diff --git a/src/lib/manifest.ml.in b/src/lib/manifest.ml.in
deleted file mode 100644
index 7746e8bd4..000000000
--- a/src/lib/manifest.ml.in
+++ /dev/null
@@ -1,7 +0,0 @@
-let dir = "%{libsail:share}%"
-
-let commit = "opam-v%{opam-version}%"
-
-let branch = "%{libsail:name}%"
-
-let version = "%{libsail:version}%"
diff --git a/src/lib/preprocess.ml b/src/lib/preprocess.ml
index bb5988831..e10ddb95d 100644
--- a/src/lib/preprocess.ml
+++ b/src/lib/preprocess.ml
@@ -144,12 +144,12 @@ let wrap_include l file = function
      [Parse_ast.DEF_pragma ("include_start", file, l)]
      @ defs
      @ [Parse_ast.DEF_pragma ("include_end", file, l)]
- 
-let rec preprocess target opts = function
+
+let rec preprocess dir target opts = function
   | [] -> []
   | Parse_ast.DEF_pragma ("define", symbol, _) :: defs ->
      symbols := StringSet.add symbol !symbols;
-     preprocess target opts defs
+     preprocess dir target opts defs
 
   | (Parse_ast.DEF_pragma ("option", command, l) as opt_pragma) :: defs ->
      begin
@@ -159,35 +159,35 @@ let rec preprocess target opts = function
        with
        | Arg.Bad message | Arg.Help message -> raise (Reporting.err_general l message)
      end;
-     opt_pragma :: preprocess target opts defs
+     opt_pragma :: preprocess dir target opts defs
 
   | Parse_ast.DEF_pragma ("ifndef", symbol, l) :: defs ->
      let then_defs, else_defs, defs = cond_pragma l defs in
      if not (StringSet.mem symbol !symbols) then
-       preprocess target opts (then_defs @ defs)
+       preprocess dir target opts (then_defs @ defs)
      else
-       preprocess target opts (else_defs @ defs)
+       preprocess dir target opts (else_defs @ defs)
 
   | Parse_ast.DEF_pragma ("ifdef", symbol, l) :: defs ->
      let then_defs, else_defs, defs = cond_pragma l defs in
      if StringSet.mem symbol !symbols then
-       preprocess target opts (then_defs @ defs)
+       preprocess dir target opts (then_defs @ defs)
      else
-       preprocess target opts (else_defs @ defs)
+       preprocess dir target opts (else_defs @ defs)
 
   | Parse_ast.DEF_pragma ("iftarget", t, l) :: defs ->
      let then_defs, else_defs, defs = cond_pragma l defs in
      begin match target with
-     | Some target when target = t ->
-        preprocess (Some target) opts (then_defs @ defs)
+     | Some t' when t = t' ->
+        preprocess dir target opts (then_defs @ defs)
      | _ ->
-        preprocess target opts (else_defs @ defs)
+        preprocess dir target opts (else_defs @ defs)
      end
        
   | Parse_ast.DEF_pragma ("include", file, l) :: defs ->
      let len = String.length file in
      if len = 0 then
-       (Reporting.warn "" l "Skipping bad $include. No file argument."; preprocess target opts defs)
+       (Reporting.warn "" l "Skipping bad $include. No file argument."; preprocess dir target opts defs)
      else if file.[0] = '"' && file.[len - 1] = '"' then
        let relative = match l with
          | Parse_ast.Range (pos, _) -> Filename.dirname (Lexing.(pos.pos_fname))
@@ -195,44 +195,44 @@ let rec preprocess target opts = function
        in
        let file = String.sub file 1 (len - 2) in
        let include_file = Filename.concat relative file in
-       let include_defs = Initial_check.parse_file ~loc:l (Filename.concat relative file) |> snd |> preprocess target opts in
-       wrap_include l include_file include_defs @ preprocess target opts defs
+       let include_defs = Initial_check.parse_file ~loc:l (Filename.concat relative file) |> snd |> preprocess dir target opts in
+       wrap_include l include_file include_defs @ preprocess dir target opts defs
      else if file.[0] = '<' && file.[len - 1] = '>' then
        let file = String.sub file 1 (len - 2) in
-       let sail_dir = Reporting.get_sail_dir () in
+       let sail_dir = Reporting.get_sail_dir dir in
        let file = Filename.concat sail_dir ("lib/" ^ file) in
-       let include_defs = Initial_check.parse_file ~loc:l file |> snd |> preprocess target opts in
-       wrap_include l file include_defs @ preprocess target opts defs
+       let include_defs = Initial_check.parse_file ~loc:l file |> snd |> preprocess dir target opts in
+       wrap_include l file include_defs @ preprocess dir target opts defs
      else
        let help = "Make sure the filename is surrounded by quotes or angle brackets" in
-       (Reporting.warn "" l ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess target opts defs)
+       (Reporting.warn "" l ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess dir target opts defs)
 
   | Parse_ast.DEF_pragma ("suppress_warnings", _, l) :: defs ->
      begin match Reporting.simp_loc l with
      | None -> () (* This shouldn't happen, but if it does just continue *)
      | Some (p, _) -> Reporting.suppress_warnings_for_file p.pos_fname
      end;
-     preprocess target opts defs
+     preprocess dir target opts defs
 
   (* Filter file_start and file_end out of the AST so when we
      round-trip files through the compiler we don't end up with
      incorrect start/end annotations *)
   | (Parse_ast.DEF_pragma ("file_start", _, _) | Parse_ast.DEF_pragma ("file_end", _, _)) :: defs ->
-     preprocess target opts defs
+     preprocess dir target opts defs
  
   | Parse_ast.DEF_pragma (p, arg, l) :: defs ->
      if not (StringSet.mem p all_pragmas) then
        Reporting.warn "" l ("Unrecognised directive: " ^ p);
-     Parse_ast.DEF_pragma (p, arg, l) :: preprocess target opts defs
+     Parse_ast.DEF_pragma (p, arg, l) :: preprocess dir target opts defs
 
   | Parse_ast.DEF_outcome (outcome_spec, inner_defs) :: defs ->
-     Parse_ast.DEF_outcome (outcome_spec, preprocess target opts inner_defs) :: preprocess target opts defs
+     Parse_ast.DEF_outcome (outcome_spec, preprocess dir target opts inner_defs) :: preprocess dir target opts defs
      
   | (Parse_ast.DEF_default (Parse_ast.DT_aux (Parse_ast.DT_order (_, Parse_ast.ATyp_aux (atyp, _)), _)) as def) :: defs ->
      begin match atyp with
-     | Parse_ast.ATyp_inc -> symbols := StringSet.add "_DEFAULT_INC" !symbols; def :: preprocess target opts defs
-     | Parse_ast.ATyp_dec -> symbols := StringSet.add "_DEFAULT_DEC" !symbols; def :: preprocess target opts defs
-     | _ -> def :: preprocess target opts defs
+     | Parse_ast.ATyp_inc -> symbols := StringSet.add "_DEFAULT_INC" !symbols; def :: preprocess dir target opts defs
+     | Parse_ast.ATyp_dec -> symbols := StringSet.add "_DEFAULT_DEC" !symbols; def :: preprocess dir target opts defs
+     | _ -> def :: preprocess dir target opts defs
      end
 
-  | def :: defs -> def :: preprocess target opts defs
+  | def :: defs -> def :: preprocess dir target opts defs
diff --git a/src/lib/preprocess.mli b/src/lib/preprocess.mli
index c2c43954a..73717d310 100644
--- a/src/lib/preprocess.mli
+++ b/src/lib/preprocess.mli
@@ -69,4 +69,4 @@ val clear_symbols : unit -> unit
 val have_symbol : string -> bool
 val add_symbol : string -> unit
 
-val preprocess : string option -> (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.def list -> Parse_ast.def list
+val preprocess : string -> string option -> (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.def list -> Parse_ast.def list
diff --git a/src/lib/reporting.ml b/src/lib/reporting.ml
index 37cf06a33..c225e7c7a 100644
--- a/src/lib/reporting.ml
+++ b/src/lib/reporting.ml
@@ -269,15 +269,14 @@ let warn ?once_from short_str l explanation =
 
 let simple_warn str = warn str Parse_ast.Unknown ""
 
-let get_sail_dir () =
+let get_sail_dir default_sail_dir =
   match Sys.getenv_opt "SAIL_DIR" with
   | Some path -> path
   | None ->
-     let share_dir = Manifest.dir in
-     if Sys.file_exists share_dir then
-       share_dir
+     if Sys.file_exists default_sail_dir then
+       default_sail_dir
      else
        raise (err_general Parse_ast.Unknown
                 ("Sail share directory "
-                 ^ share_dir
+                 ^ default_sail_dir
                  ^ " does not exist. Make sure Sail is installed correctly, or try setting the SAIL_DIR environment variable"))
diff --git a/src/lib/reporting.mli b/src/lib/reporting.mli
index df7970971..e8e35bc52 100644
--- a/src/lib/reporting.mli
+++ b/src/lib/reporting.mli
@@ -162,5 +162,5 @@ val simple_warn: string -> unit
    $suppress_warnings directive in process_file.ml *)
 val suppress_warnings_for_file : string -> unit
 
-val get_sail_dir : unit -> string
+val get_sail_dir : string -> string
 
diff --git a/src/lib/specialize.ml b/src/lib/specialize.ml
index 3894a6f3a..3608790a8 100644
--- a/src/lib/specialize.ml
+++ b/src/lib/specialize.ml
@@ -638,5 +638,5 @@ let () =
   let open Interactive in
   Action (fun istate ->
     let ast', env', effect_info' = specialize typ_ord_specialization istate.env istate.ast istate.effect_info in
-    { ast = ast'; env = env'; effect_info = effect_info' }
+    { istate with ast = ast'; env = env'; effect_info = effect_info' }
   ) |> register_command ~name:"specialize" ~help:"Specialize Type and Order type variables in the AST"
diff --git a/src/lib/target.ml b/src/lib/target.ml
index 7ff55c7fb..b17a5f324 100644
--- a/src/lib/target.ml
+++ b/src/lib/target.ml
@@ -76,7 +76,7 @@ type target = {
     pre_parse_hook : (unit -> unit);
     pre_rewrites_hook : (tannot ast -> Effects.side_effect_info -> Env.t -> unit);
     rewrites : (string * Rewrites.rewriter_arg list) list;
-    action : string option -> tannot ast -> Effects.side_effect_info -> Env.t -> unit;
+    action : string -> string option -> tannot ast -> Effects.side_effect_info -> Env.t -> unit;
     asserts_termination : bool;
   }
 
@@ -160,7 +160,7 @@ let () =
     match get ~name:name with
     | Some tgt ->
        let ast, effect_info, env = Rewrites.rewrite istate.effect_info istate.env (rewrites tgt) istate.ast in
-       { ast = ast; env = env; effect_info = effect_info }
+       { istate with ast = ast; env = env; effect_info = effect_info }
     | None ->
        print_endline ("No target " ^ name);
        istate
@@ -168,6 +168,6 @@ let () =
                 
   ArgString ("target", fun name -> ArgString ("out", fun out -> ActionUnit (fun istate ->
     match get ~name:name with
-    | Some tgt -> action tgt (Some out) istate.ast istate.effect_info istate.env;
+    | Some tgt -> action tgt istate.default_sail_dir (Some out) istate.ast istate.effect_info istate.env;
     | None -> print_endline ("No target " ^ name)
   ))) |> register_command ~name:"target" ~help:"invoke Sail target. See :list_targets for a list of targets. out parameter is equivalent to command line -o option"
diff --git a/src/lib/target.mli b/src/lib/target.mli
index 7d72c8747..301197781 100644
--- a/src/lib/target.mli
+++ b/src/lib/target.mli
@@ -82,7 +82,7 @@ val run_pre_rewrites_hook : target -> tannot ast -> Effects.side_effect_info ->
 
 val rewrites : target -> Rewrites.rewrite_sequence
   
-val action : target -> string option -> tannot ast -> Effects.side_effect_info -> Env.t -> unit
+val action : target -> string -> string option -> tannot ast -> Effects.side_effect_info -> Env.t -> unit
 
 val asserts_termination : target -> bool
 
@@ -114,7 +114,7 @@ val register :
   ?pre_rewrites_hook:(tannot ast -> Effects.side_effect_info -> Env.t -> unit) ->
   ?rewrites:(string * Rewrites.rewriter_arg list) list ->
   ?asserts_termination:bool ->
-  (string option -> tannot ast -> Effects.side_effect_info -> Env.t -> unit) ->
+  (string -> string option -> tannot ast -> Effects.side_effect_info -> Env.t -> unit) ->
   target
 
 val get_the_target : unit -> target option
diff --git a/src/sail_c_backend/sail_plugin_c.ml b/src/sail_c_backend/sail_plugin_c.ml
index 8782f0e6b..ae90afbac 100644
--- a/src/sail_c_backend/sail_plugin_c.ml
+++ b/src/sail_c_backend/sail_plugin_c.ml
@@ -152,7 +152,7 @@ let c_rewrites =
     ("constant_fold", [String_arg "c"])
   ]
 
-let c_target out_file ast effect_info _ =
+let c_target _ out_file ast effect_info _ =
   let ast, env = Type_error.check Type_check.initial_env ast in
   let close, output_chan = match out_file with Some f -> true, open_out (f ^ ".c") | None -> false, stdout in
   Reporting.opt_warnings := true;
diff --git a/src/sail_coq_backend/sail_plugin_coq.ml b/src/sail_coq_backend/sail_plugin_coq.ml
index 3b374f713..28e07923d 100644
--- a/src/sail_coq_backend/sail_plugin_coq.ml
+++ b/src/sail_coq_backend/sail_plugin_coq.ml
@@ -187,7 +187,7 @@ let output libs files =
       output_coq !opt_coq_output_dir f' !opt_alt_modules_coq !opt_alt_modules2_coq libs effect_info ast)
     files
 
-let coq_target out_file ast effect_info env =
+let coq_target _ out_file ast effect_info env =
   let out_file = match out_file with Some f -> f | None -> "out" in
   output (!opt_libs_coq) [(out_file, effect_info, env, ast)]
 
diff --git a/src/sail_latex_backend/sail_plugin_latex.ml b/src/sail_latex_backend/sail_plugin_latex.ml
index 5d035148b..ab6d916f4 100644
--- a/src/sail_latex_backend/sail_plugin_latex.ml
+++ b/src/sail_latex_backend/sail_plugin_latex.ml
@@ -84,7 +84,7 @@ let latex_options = [
     " semicolon-separated list of abbreviations to fix spacing for in LaTeX output (default 'e.g.;i.e.')");
 ]
 
-let latex_target out_file ast effect_info env =
+let latex_target _ out_file ast effect_info env =
   Reporting.opt_warnings := true;
   let latex_dir = match out_file with None -> "sail_latex" | Some s -> s in
   begin
diff --git a/src/sail_lem_backend/sail_plugin_lem.ml b/src/sail_lem_backend/sail_plugin_lem.ml
index 48cf767d6..ba948e23f 100644
--- a/src/sail_lem_backend/sail_plugin_lem.ml
+++ b/src/sail_lem_backend/sail_plugin_lem.ml
@@ -209,7 +209,7 @@ let output libs files =
       output_lem f' libs effect_info env ast)
     files
 
-let lem_target out_file ast effect_info env =
+let lem_target _ out_file ast effect_info env =
   let out_file = match out_file with Some f -> f | None -> "out" in
   output (!opt_libs_lem) [(out_file, effect_info, env, ast)]
 
diff --git a/src/sail_ocaml_backend/ocaml_backend.ml b/src/sail_ocaml_backend/ocaml_backend.ml
index 18f3b3903..80dcff5c1 100644
--- a/src/sail_ocaml_backend/ocaml_backend.ml
+++ b/src/sail_ocaml_backend/ocaml_backend.ml
@@ -1043,8 +1043,8 @@ let system_checked str =
      prerr_endline (str ^ " was stopped by a signal");
      exit 1
 
-let ocaml_compile spec ast generator_types =
-  let sail_dir = Reporting.get_sail_dir () in
+let ocaml_compile default_sail_dir spec ast generator_types =
+  let sail_dir = Reporting.get_sail_dir default_sail_dir in
   if Sys.file_exists !opt_ocaml_build_dir then () else Unix.mkdir !opt_ocaml_build_dir 0o775;
   let cwd = Unix.getcwd () in
   Unix.chdir !opt_ocaml_build_dir;
diff --git a/src/sail_ocaml_backend/sail_plugin_ocaml.ml b/src/sail_ocaml_backend/sail_plugin_ocaml.ml
index 2426965b3..f88b23038 100644
--- a/src/sail_ocaml_backend/sail_plugin_ocaml.ml
+++ b/src/sail_ocaml_backend/sail_plugin_ocaml.ml
@@ -119,9 +119,9 @@ let ocaml_rewrites =
     ("overload_cast", [])
   ]
  
-let ocaml_target out_file ast effect_info env =
+let ocaml_target default_sail_dir out_file ast effect_info env =
   let out = match out_file with None -> "out" | Some s -> s in
-  Ocaml_backend.ocaml_compile out ast !ocaml_generator_info
+  Ocaml_backend.ocaml_compile default_sail_dir out ast !ocaml_generator_info
    
 let _ =
   Target.register
@@ -160,7 +160,7 @@ let tofrominterp_rewrites =
     ("simple_assignments", [])
   ]
     
-let tofrominterp_target out_file ast _ _ =
+let tofrominterp_target _ out_file ast _ _ =
   let out = match out_file with None -> "out" | Some s -> s in
   ToFromInterp_backend.tofrominterp_output !opt_tofrominterp_output_dir out ast
 
@@ -172,7 +172,7 @@ let _ =
     ~rewrites:tofrominterp_rewrites
     tofrominterp_target
 
-let marshal_target out_file ast _ env =
+let marshal_target _ out_file ast _ env =
   let out_filename = match out_file with None -> "out" | Some s -> s in
   let f = open_out_bin (out_filename ^ ".defs") in
   let remove_prover (l, tannot) =
diff --git a/src/sail_output/sail_plugin_output.ml b/src/sail_output/sail_plugin_output.ml
index 7e5fc84a1..56259b4a6 100644
--- a/src/sail_output/sail_plugin_output.ml
+++ b/src/sail_output/sail_plugin_output.ml
@@ -73,7 +73,7 @@ let output_sail_options = [
     " set a directory to output pretty-printed Sail");
 ]
 
-let sail_target out_file ast _effect_info _env =
+let sail_target _ out_file ast _effect_info _env =
    let close, output_chan = match out_file with
      | Some f -> true, open_out (f ^ ".sail")
      | None -> false, stdout in
diff --git a/src/sail_smt_backend/sail_plugin_smt.ml b/src/sail_smt_backend/sail_plugin_smt.ml
index 02fe1d6e2..3bcd46d4c 100644
--- a/src/sail_smt_backend/sail_plugin_smt.ml
+++ b/src/sail_smt_backend/sail_plugin_smt.ml
@@ -119,7 +119,7 @@ let smt_rewrites =
     ("properties", [])
   ]
 
-let smt_target out_file ast effect_info env =
+let smt_target _ out_file ast effect_info env =
   let open Ast_util in
   let props = Property.find_properties ast in
   let prop_ids = Bindings.bindings props |> List.map fst |> IdSet.of_list in