From a00ca1b507b638cffa7404ee5e5bba9ddaa1a586 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 24 Jul 2024 17:15:07 +0300 Subject: [PATCH 1/3] Remove goblint.build-info.js and goblint.sites.js --- gobview | 2 +- src/build-info/build_info_js/dune | 5 ----- src/build-info/build_info_js/dune_build_info.ml | 1 - src/sites/sites_js/dune | 6 ------ src/sites/sites_js/goblint_sites.ml | 6 ------ 5 files changed, 1 insertion(+), 19 deletions(-) delete mode 100644 src/build-info/build_info_js/dune delete mode 100644 src/build-info/build_info_js/dune_build_info.ml delete mode 100644 src/sites/sites_js/dune delete mode 100644 src/sites/sites_js/goblint_sites.ml diff --git a/gobview b/gobview index 03b0682f97..1895e62dab 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 03b0682f973eab0d26cf8aea74c63a9e869c9716 +Subproject commit 1895e62dab67cfb05a5981bcfd7f36d46acd2b7e diff --git a/src/build-info/build_info_js/dune b/src/build-info/build_info_js/dune deleted file mode 100644 index 9400f564ff..0000000000 --- a/src/build-info/build_info_js/dune +++ /dev/null @@ -1,5 +0,0 @@ -; goblint.build-info implementation which works with js_of_ocaml and doesn't use dune-build-info -(library - (name goblint_build_info_js) - (public_name goblint.build-info.js) - (implements goblint.build-info)) diff --git a/src/build-info/build_info_js/dune_build_info.ml b/src/build-info/build_info_js/dune_build_info.ml deleted file mode 100644 index 002015cd31..0000000000 --- a/src/build-info/build_info_js/dune_build_info.ml +++ /dev/null @@ -1 +0,0 @@ -let statically_linked_libraries = [] diff --git a/src/sites/sites_js/dune b/src/sites/sites_js/dune deleted file mode 100644 index 4e20871974..0000000000 --- a/src/sites/sites_js/dune +++ /dev/null @@ -1,6 +0,0 @@ -; goblint.sites implementation which works with js_of_ocaml and doesn't use dune-site -(library - (name goblint_sites_js) - (public_name goblint.sites.js) - (implements goblint.sites) - (modules goblint_sites)) diff --git a/src/sites/sites_js/goblint_sites.ml b/src/sites/sites_js/goblint_sites.ml deleted file mode 100644 index 3a7b353064..0000000000 --- a/src/sites/sites_js/goblint_sites.ml +++ /dev/null @@ -1,6 +0,0 @@ -let lib = [] -let lib_stub_include = [] -let lib_stub_src = [] -let lib_runtime_include = [] -let lib_runtime_src = [] -let conf = [] From 5a50fa1e16e63ab3ebe5004dce2a3bf3cb4aba6f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 24 Jul 2024 17:26:08 +0300 Subject: [PATCH 2/3] Unvirtualize goblint.build-info and goblint.sites --- gobview | 2 +- src/build-info/build_info_dune/dune | 6 ------ src/build-info/dune | 8 +------- .../{build_info_dune => }/dune_build_info.ml | 0 src/dune | 8 ++++---- src/sites/dune | 12 +++++------- src/sites/{sites_dune => }/goblint_sites.ml | 0 src/sites/sites_dune/dune | 12 ------------ tests/regression/cfg/util/dune | 4 ++-- tests/unit/dune | 2 +- tests/util/dune | 4 ++-- 11 files changed, 16 insertions(+), 42 deletions(-) delete mode 100644 src/build-info/build_info_dune/dune rename src/build-info/{build_info_dune => }/dune_build_info.ml (100%) rename src/sites/{sites_dune => }/goblint_sites.ml (100%) delete mode 100644 src/sites/sites_dune/dune diff --git a/gobview b/gobview index 1895e62dab..f9ce8bcad3 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 1895e62dab67cfb05a5981bcfd7f36d46acd2b7e +Subproject commit f9ce8bcad3552ad95488bc4988dcc0d5ed57b365 diff --git a/src/build-info/build_info_dune/dune b/src/build-info/build_info_dune/dune deleted file mode 100644 index ec46f4b3d1..0000000000 --- a/src/build-info/build_info_dune/dune +++ /dev/null @@ -1,6 +0,0 @@ -; goblint.build-info implementation which properly uses dune-build-info -(library - (name goblint_build_info_dune) - (public_name goblint.build-info.dune) - (implements goblint.build-info) - (libraries dune-build-info)) diff --git a/src/build-info/dune b/src/build-info/dune index e1a45ef8fc..4ffa1f4550 100644 --- a/src/build-info/dune +++ b/src/build-info/dune @@ -1,15 +1,9 @@ (include_subdirs no) -; virtual library to allow js build (for gobview) without dune-build-info -; dune-build-info seems to be incompatible with js_of_ocaml -; File "gobview/src/.App.eobjs/build_info_data.ml-gen", line 1: -; Error: Could not find the .cmi file for interface -; gobview/src/.App.eobjs/build_info_data.ml-gen. (library (name goblint_build_info) (public_name goblint.build-info) - (libraries batteries.unthreaded) - (virtual_modules dune_build_info)) + (libraries dune-build-info batteries.unthreaded)) (rule (target configVersion.ml) diff --git a/src/build-info/build_info_dune/dune_build_info.ml b/src/build-info/dune_build_info.ml similarity index 100% rename from src/build-info/build_info_dune/dune_build_info.ml rename to src/build-info/dune_build_info.ml diff --git a/src/dune b/src/dune index 5265821b5a..c549fd5d7d 100644 --- a/src/dune +++ b/src/dune @@ -88,7 +88,7 @@ (public_names goblint) (modes byte native) ; https://dune.readthedocs.io/en/stable/dune-files.html#linking-modes (modules goblint) - (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std) + (libraries goblint.lib goblint.sites goblint.build-info goblint_std) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall -open Goblint_std) ) @@ -96,7 +96,7 @@ (executable (name privPrecCompare) (modules privPrecCompare) - (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std) + (libraries goblint.lib goblint.sites goblint.build-info goblint_std) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall -open Goblint_std) ) @@ -104,7 +104,7 @@ (executable (name apronPrecCompare) (modules apronPrecCompare) - (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std) + (libraries goblint.lib goblint.sites goblint.build-info goblint_std) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall -open Goblint_std) ) @@ -112,7 +112,7 @@ (executable (name messagesCompare) (modules messagesCompare) - (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std) + (libraries goblint.lib goblint.sites goblint.build-info goblint_std) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall -open Goblint_std) ) diff --git a/src/sites/dune b/src/sites/dune index d8663e37fe..6de3a5a32a 100644 --- a/src/sites/dune +++ b/src/sites/dune @@ -1,12 +1,10 @@ (include_subdirs no) -; virtual library to allow js build (for gobview) without dune-site -; dune-site seems to be incompatible with js_of_ocaml -; File "gobview/src/.App.eobjs/dune_site_data.ml-gen", line 1: -; Error: Could not find the .cmi file for interface -; gobview/src/.App.eobjs/dune_site_data.ml-gen. (library (name goblint_sites) (public_name goblint.sites) - (virtual_modules goblint_sites) - (libraries fpath)) + (libraries dune-site fpath)) + +(generate_sites_module + (module dunesite) + (sites goblint)) diff --git a/src/sites/sites_dune/goblint_sites.ml b/src/sites/goblint_sites.ml similarity index 100% rename from src/sites/sites_dune/goblint_sites.ml rename to src/sites/goblint_sites.ml diff --git a/src/sites/sites_dune/dune b/src/sites/sites_dune/dune deleted file mode 100644 index b7f90a8892..0000000000 --- a/src/sites/sites_dune/dune +++ /dev/null @@ -1,12 +0,0 @@ -; goblint.sites implementation which properly uses dune-site -(library - (name goblint_sites_dune) - (public_name goblint.sites.dune) - (implements goblint.sites) - (modules goblint_sites dunesite) - (private_modules dunesite) ; must also be in modules - (libraries dune-site)) - -(generate_sites_module - (module dunesite) - (sites goblint)) diff --git a/tests/regression/cfg/util/dune b/tests/regression/cfg/util/dune index fb3c5e6899..4c41de07e4 100644 --- a/tests/regression/cfg/util/dune +++ b/tests/regression/cfg/util/dune @@ -6,6 +6,6 @@ goblint_common goblint_lib ; TODO: avoid: extract LoopUnrolling and WitnessUtil node predicates from goblint_lib fpath - goblint.sites.dune - goblint.build-info.dune) + goblint.sites + goblint.build-info) (preprocess (pps ppx_deriving.std))) diff --git a/tests/unit/dune b/tests/unit/dune index 5f0b909a77..6c3083dc1a 100644 --- a/tests/unit/dune +++ b/tests/unit/dune @@ -2,7 +2,7 @@ (test (name mainTest) - (libraries ounit2 qcheck-ounit goblint.std goblint.common goblint.lib goblint.constraint goblint.solver goblint.cdomain.value goblint.sites.dune goblint.build-info.dune) + (libraries ounit2 qcheck-ounit goblint.std goblint.common goblint.lib goblint.constraint goblint.solver goblint.cdomain.value goblint.sites goblint.build-info) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall)) diff --git a/tests/util/dune b/tests/util/dune index 6637217651..fb630bd15b 100644 --- a/tests/util/dune +++ b/tests/util/dune @@ -5,7 +5,7 @@ goblint_std goblint_lib yaml - goblint.sites.dune - goblint.build-info.dune) + goblint.sites + goblint.build-info) (flags :standard -open Goblint_std) (preprocess (pps ppx_deriving.std))) From a5ab08b1a744f647ea4ef86a24173b6d545c103f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 24 Jul 2024 17:27:39 +0300 Subject: [PATCH 3/3] Remove unused goblint.build-info and goblint.sites dependency from most executables --- gobview | 2 +- src/dune | 8 ++++---- src/index.mld | 6 ------ tests/regression/cfg/util/dune | 4 +--- tests/unit/dune | 2 +- tests/util/dune | 4 +--- 6 files changed, 8 insertions(+), 18 deletions(-) diff --git a/gobview b/gobview index f9ce8bcad3..4e965cf1bb 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit f9ce8bcad3552ad95488bc4988dcc0d5ed57b365 +Subproject commit 4e965cf1bb7be5e7ceef2a40586ea445682cca64 diff --git a/src/dune b/src/dune index c549fd5d7d..2ba497c629 100644 --- a/src/dune +++ b/src/dune @@ -88,7 +88,7 @@ (public_names goblint) (modes byte native) ; https://dune.readthedocs.io/en/stable/dune-files.html#linking-modes (modules goblint) - (libraries goblint.lib goblint.sites goblint.build-info goblint_std) + (libraries goblint.lib goblint_std) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall -open Goblint_std) ) @@ -96,7 +96,7 @@ (executable (name privPrecCompare) (modules privPrecCompare) - (libraries goblint.lib goblint.sites goblint.build-info goblint_std) + (libraries goblint.lib goblint_std) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall -open Goblint_std) ) @@ -104,7 +104,7 @@ (executable (name apronPrecCompare) (modules apronPrecCompare) - (libraries goblint.lib goblint.sites goblint.build-info goblint_std) + (libraries goblint.lib goblint_std) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall -open Goblint_std) ) @@ -112,7 +112,7 @@ (executable (name messagesCompare) (modules messagesCompare) - (libraries goblint.lib goblint.sites goblint.build-info goblint_std) + (libraries goblint.lib goblint_std) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall -open Goblint_std) ) diff --git a/src/index.mld b/src/index.mld index f0d63a0fc7..a2ef15482e 100644 --- a/src/index.mld +++ b/src/index.mld @@ -44,15 +44,9 @@ The following libraries provide [goblint] package metadata for executables. {2 Library goblint.build-info} {!modules:Goblint_build_info} -This library is virtual and has the following implementations -- goblint.build-info.dune for native executables, -- goblint.build-info.js for js_of_ocaml executables. {2 Library goblint.sites} {!modules:Goblint_sites} -This library is virtual and has the following implementations -- goblint.sites.dune for native executables, -- goblint.sites.js for js_of_ocaml executables. {1 Independent utilities} diff --git a/tests/regression/cfg/util/dune b/tests/regression/cfg/util/dune index 4c41de07e4..8ab300b531 100644 --- a/tests/regression/cfg/util/dune +++ b/tests/regression/cfg/util/dune @@ -5,7 +5,5 @@ goblint_logs goblint_common goblint_lib ; TODO: avoid: extract LoopUnrolling and WitnessUtil node predicates from goblint_lib - fpath - goblint.sites - goblint.build-info) + fpath) (preprocess (pps ppx_deriving.std))) diff --git a/tests/unit/dune b/tests/unit/dune index 6c3083dc1a..07c87e7822 100644 --- a/tests/unit/dune +++ b/tests/unit/dune @@ -2,7 +2,7 @@ (test (name mainTest) - (libraries ounit2 qcheck-ounit goblint.std goblint.common goblint.lib goblint.constraint goblint.solver goblint.cdomain.value goblint.sites goblint.build-info) + (libraries ounit2 qcheck-ounit goblint.std goblint.common goblint.lib goblint.constraint goblint.solver goblint.cdomain.value) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall)) diff --git a/tests/util/dune b/tests/util/dune index fb630bd15b..d37c38dc7c 100644 --- a/tests/util/dune +++ b/tests/util/dune @@ -4,8 +4,6 @@ batteries.unthreaded goblint_std goblint_lib - yaml - goblint.sites - goblint.build-info) + yaml) (flags :standard -open Goblint_std) (preprocess (pps ppx_deriving.std)))