diff --git a/src/backends/C/c_backend_makefile.ml b/src/backends/C/c_backend_makefile.ml index 38f7c80a1d9a59010d5b4c10349d33b6670c37f3..0a7820f39222299107dce4d6bee11472a1cb314a 100644 --- a/src/backends/C/c_backend_makefile.ml +++ b/src/backends/C/c_backend_makefile.ml @@ -63,7 +63,7 @@ let pp_print_dependencies arrow_suffix fmt deps = List.map (fun dep -> (if dep.local then dep.name - else Version.include_path ^ "/" ^ dep.name) + else Sites_paths.include_path ^ "/" ^ dep.name) ^ ".c") compiled_deps in @@ -136,7 +136,7 @@ functor binname Sys.executable_name (Filename.dirname (Filename.dirname Sys.executable_name)) - Version.include_path + Sites_paths.include_path (* Main binary *) basename "run" diff --git a/src/dune b/src/dune index bddbd9510095a3188978fcb8f5994affa613f516..39d94634b688173801488ff3ae6630558241a411 100644 --- a/src/dune +++ b/src/dune @@ -6,12 +6,11 @@ (include_subdirs unqualified) (library - (name lustrec_interface) + (name lustrec_core) (package lustrec) (modules_without_implementation scheduling_type machine_code_types) (modules lustre_types - lustre_utils utils location dimension @@ -19,37 +18,21 @@ real types options - version clocks delay - scheduling_type + log + corelang machine_code_types spec_types - spec_common - lustre_live - log + scheduling_type printers - corelang basic_library + version type_predef + annotations clock_predef - delay_predef error global - annotations - machine_code_common - arrow - options_management - stateless - c_backend_common - typing - ocaml_utils - backends - lustrec_mpfr - normalization - arrow_taint - machine_types - splitting compiler_common parse parser_lustre @@ -58,9 +41,34 @@ lexer_lustre lexerLustreSpec automata - clock_calculus) + stateless + typing + clock_calculus + backends + normalization + machine_types + splitting) + (wrapped false) + (libraries ocamlgraph menhirLib zarith unix)) + +(library + (name lustrec_interface) + (package lustrec) + (modules + lustre_utils + spec_common + lustre_live + delay_predef + machine_code_common + arrow + sites_paths + options_management + c_backend_common + ocaml_utils + lustrec_mpfr + arrow_taint) (wrapped false) - (libraries sites ocamlgraph zarith unix str menhirLib)) + (libraries lustrec_core sites str)) (library (name plugin_register) @@ -71,7 +79,6 @@ (generate_sites_module (module sites) - ; (sites lustrec) (plugins (lustrec plugins) (lustrec verifiers))) @@ -126,7 +133,7 @@ c_backend_main plugins) (wrapped false) - (libraries sites lustrec_interface plugin_register)) + (libraries lustrec_interface plugin_register)) (executable (name main_lustre_compiler) @@ -139,13 +146,12 @@ (name main_lustre_testgen) (public_name lustret) (modules main_lustre_testgen mutation pathConditions) - (libraries lustrec_lib)) + (libraries lustrec_core lustrec_lib)) (library (name verifier_register) (package lustrec) (wrapped false) - ; (modules_without_implementation verifierType) (modules verifierList verifierType) (libraries lustrec_interface)) diff --git a/src/main_lustre_testgen.ml b/src/main_lustre_testgen.ml index 8f15747c693158f073e267a1fa98202b35a11e73..8871b296c8913dd289ab42ada5a78e7e01dcd704 100644 --- a/src/main_lustre_testgen.ml +++ b/src/main_lustre_testgen.ml @@ -158,11 +158,11 @@ let testgen_source dirname basename extension = Format.fprintf cmake_fmt "include(\"%s/helpful_functions.cmake\")@." - Version.testgen_path; + Sites_paths.testgen_path; Format.fprintf cmake_fmt "include(\"%s/FindLustre.cmake\")@." - Version.testgen_path; + Sites_paths.testgen_path; Format.fprintf cmake_fmt "LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )@."; Format.fprintf cmake_fmt "@[<v 2>FOREACH(lus_file ${LFILES})@ "; Format.fprintf cmake_fmt "get_lustre_name_ext(${lus_file} L E)@ "; diff --git a/src/options_management.ml b/src/options_management.ml index c7f00109c98faa6b91e96e4b687eeb9e2f414ab4..80f2f691d47596e089fdcf9854708b4997483c4f 100644 --- a/src/options_management.ml +++ b/src/options_management.ml @@ -20,7 +20,7 @@ let print_version () = User provided include directory: @[<h>%a@]@]@." Version.number Version.codename - Version.include_path + Sites_paths.include_path (pp_print_list ~pp_sep:pp_print_space pp_print_string) !include_dirs @@ -38,7 +38,7 @@ let add_include_dir dir = perform a fold_right to respect the order *) let search_lib_path (local, full_file_name) = let paths = - if local then !include_dirs else Version.include_path :: !include_dirs + if local then !include_dirs else Sites_paths.include_path :: !include_dirs in let name = List.fold_right diff --git a/src/sites_paths.ml b/src/sites_paths.ml new file mode 100644 index 0000000000000000000000000000000000000000..ba37a8483373ecdfdd7748836605a2a400494398 --- /dev/null +++ b/src/sites_paths.ml @@ -0,0 +1,2 @@ +let include_path = Sites.Sites.include_ |> List.hd +let testgen_path = Sites.Sites.testgen |> List.hd diff --git a/src/sites_paths.mli b/src/sites_paths.mli new file mode 100644 index 0000000000000000000000000000000000000000..e66b83918fdc814bcc59e1c60ca6d9f3818a3872 --- /dev/null +++ b/src/sites_paths.mli @@ -0,0 +1,2 @@ +val include_path : string +val testgen_path : string diff --git a/src/version.ml b/src/version.ml index de05425ea4e648489077d422d0c971a58b7122a8..9012783777c879fde447d519f81bc900686c7844 100644 --- a/src/version.ml +++ b/src/version.ml @@ -1,4 +1,2 @@ let number = "@PACKAGE_VERSION@-@GITBRANCH@" let codename = "@VERSION_CODENAME@" -let include_path = Sites.Sites.include_ |> List.hd -let testgen_path = Sites.Sites.testgen |> List.hd diff --git a/src/version.mli b/src/version.mli index 58fc63e453a2c84f2ed6946ab2c959eae953b185..e1f7bfcf8da9b72039048e6b5a8c4c9c59733c57 100644 --- a/src/version.mli +++ b/src/version.mli @@ -1,4 +1,2 @@ val number : string val codename : string -val include_path : string -val testgen_path : string