Move manifest file from src/lib to src/bin

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))

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

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

sail.opam.template

@@ -0,0 +1 @@
+substs: [ "src/bin/manifest.ml" ]

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)

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}%"

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" ->

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
   );
 

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)))

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
 

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

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 =

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