Merge pull request #3564 from mtzguido/locate

Some refactoring about include paths, finding, locate, etc
FStarLang · Oct 14, 2024 · 84d9ea8 · 84d9ea8
2 parents 0cd990c + 2e37a9e
commit 84d9ea8
Show file tree

Hide file tree

Showing 23 changed files with 308 additions and 281 deletions.
diff --git a/ocaml/fstar-lib/FStarC_Compiler_Util.ml b/ocaml/fstar-lib/FStarC_Compiler_Util.ml
@@ -1163,3 +1163,6 @@ let array_of_list (l:'a list) = FStar_ImmutableArray_Base.of_list l
 let array_length (l:'a FStar_ImmutableArray_Base.t) = FStar_ImmutableArray_Base.length l
 
 let array_index (l:'a FStar_ImmutableArray_Base.t) (i:Z.t) = FStar_ImmutableArray_Base.index l i
+
+let putenv k v = Unix.putenv k v
+let execvp c args = Unix.execvp c (Array.of_list args)
diff --git a/ocaml/fstar-lib/FStarC_Extraction_ML_PrintML.ml b/ocaml/fstar-lib/FStarC_Extraction_ML_PrintML.ml
@@ -538,7 +538,7 @@ let print (out_dir: string option) (ext: string) (ml: mllib) =
      let new_doc = FStarC_Extraction_ML_Code.doc_of_mllib ml in
      iter (fun (n, d) ->
          FStarC_Compiler_Util.write_file
-           (FStarC_Options.prepend_output_dir (BatString.concat "" [n;ext]))
+           (FStarC_Find.prepend_output_dir (BatString.concat "" [n;ext]))
            (FStarC_Extraction_ML_Code.pretty (Prims.parse_int "120") d)
            ) new_doc
   | _ -> failwith "Unrecognized extension"
diff --git a/ocaml/fstar-lib/generated/FStarC_Compiler_Plugins.ml b/ocaml/fstar-lib/generated/FStarC_Compiler_Plugins.ml
diff --git a/ocaml/fstar-lib/generated/FStarC_Find.ml b/ocaml/fstar-lib/generated/FStarC_Find.ml
diff --git a/ocaml/fstar-lib/generated/FStarC_Main.ml b/ocaml/fstar-lib/generated/FStarC_Main.ml
diff --git a/ocaml/fstar-lib/generated/FStarC_Options.ml b/ocaml/fstar-lib/generated/FStarC_Options.ml