bootstrapping for offline dune files

aslp_offline.opam

@@ -9,7 +9,7 @@ license: "BSD-3-Clause"
 homepage: "https://github.com/UQ-PAC/aslp"
 bug-reports: "https://github.com/UQ-PAC/aslp/issues"
 depends: [
-  "dune" {>= "2.8"}
+  "dune" {>= "2.9"}
   "ocaml" {>= "4.14"}
   "asli"
   "odoc" {with-doc}
@@ -23,9 +23,11 @@ build: [
     name
     "-j"
     jobs
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
+  ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/UQ-PAC/aslp.git"

dune-project

@@ -1,4 +1,4 @@
-(lang dune 2.8)
+(lang dune 2.9)
 (name asli)
 (version 0.2.0)
 

libASL/ocaml_backend.ml

@@ -68,7 +68,7 @@ let write_preamble opens st =
 
 let write_epilogue use_pc fid st =
   let conv_pc = "let pc = (mkBits (Z.of_int 64) (Z.of_int pc)) in" in
-  let dis_call = (match use_pc with 
+  let dis_call = (match use_pc with
     | true ->  Printf.sprintf "%s\n  %s enc pc" conv_pc
     | false ->  Printf.sprintf "%s enc"
   ) (name_of_ident fid)
@@ -341,7 +341,7 @@ let write_fn name (ret_tyo,_,targs,args,_,body) st =
  * Directory Setup
  ****************************************************************)
 
-let init_st oc = { depth = 0; skip_seq = false; oc ; ref_vars = IdentSet.empty } 
+let init_st oc = { depth = 0; skip_seq = false; oc ; ref_vars = IdentSet.empty }
 let global_deps = ["Offline_utils"]
 let offline_utils_file = [%blob "../offlineASL/template_offline_utils.ml"]
 
@@ -377,17 +377,18 @@ let write_decoder_file use_pc fn fnsig deps dir =
   write_fn fn fnsig st;
   write_epilogue use_pc fn st;
   close_out oc;
-  m 
+  m
 
-let write_new_dune_file use_pc files dir  : unit = 
+let write_new_dune_file use_pc files dir  : unit =
   let target_gen_files = String.concat "" @@ List.map (fun k ->
     Printf.sprintf "    %s.ml\n" k
   ) files in
-  let oc = open_out (dir ^ "/dune.template") in
-  Printf.fprintf oc "(rule 
-  (targets\n%s
-    dune.template
-  ) 
+  let oc = open_out (dir ^ "/dune.generated.new") in
+  Printf.fprintf oc "; AUTO-GENERATED BY OCAML BACKEND\n";
+  Printf.fprintf oc "(rule
+  (targets
+    dune.generated.new\n%s
+  )
   (deps gen-command)
   (action (with-stdin-from gen-command (run asli)))
 )" target_gen_files ;
@@ -411,8 +412,9 @@ let write_new_dune_file use_pc files dir  : unit =
 
 
 (* Write the dune build file *)
+(* XXX: this function is not used anymore? *)
 let write_dune_file use_pc files dir =
-  let oc = open_out (dir ^ "/dune.template") in
+  let oc = open_out (dir ^ "/dune.inc") in
   Printf.fprintf oc "; AUTO-GENERATED BY OCAML BACKEND
 (library
   (name offlineASL)
@@ -428,7 +430,7 @@ let write_dune_file use_pc files dir =
   (libraries asli.libASL-stage0))";
   close_out oc
 
-let write_ibi dir = 
+let write_ibi dir =
   let oc = open_out (dir ^ "/Offline_utils.ml") in
   output_string oc offline_utils_file ;
   close_out oc
@@ -440,9 +442,9 @@ let run config dfn dfnsig tests fns =
   let files = (write_test_file tests dir)::files in
   let decoder = write_decoder_file config.use_pc dfn dfnsig files dir in
   write_ibi dir ;
-  try 
+  try
   write_new_dune_file config.use_pc (decoder::files@global_deps) dir
-  with 
+  with
     | Sys_error _ as e -> Printf.eprintf "failed to write dune file\n%s" (Printexc.to_string e); Printexc.print_backtrace stderr
 
 module OcamlBackend : Backend = struct

offlineASL/dune.bootstrap

@@ -0,0 +1,22 @@
+; this manually-written file implements the bootstrapping for the offline lifter dune files.
+
+; to bootstrap without a dune.generated file:
+; 
+; 1. cd offlineASL
+; 2. make blank file so dune executes: touch dune.generated
+; 3. write file which calls gen-command: ASLP_OFFLINE_BOOTSTRAP=true dune runtest offlineASL --auto-promote
+; 4. update file with result from gen-command: dune runtest offlineASL --auto-promote
+
+(rule
+ (target dune.generated.new)
+ (action
+  (write-file %{target} "
+  (rule (targets %{target})
+   (deps gen-command)
+   (action (with-stdin-from gen-command (run asli))))"))
+ (enabled_if %{env:ASLP_OFFLINE_BOOTSTRAP=false}))
+
+(rule
+ (alias runtest)
+ (package aslp_offline)
+ (action (diff dune.generated dune.generated.new)))