Merge pull request #1215 from goblint/improve-gobview-build

Improve GobView build

.github/workflows/locked.yml

@@ -170,7 +170,7 @@ jobs:
         run: ./make.sh nat
 
       - name: Build Gobview
-        run: opam exec -- dune build gobview
+        run: ./make.sh view
 
       - name: Install selenium
         run: pip3 install selenium webdriver-manager

.gitignore

@@ -10,6 +10,7 @@ goblint
 goblint.byte
 goblint.json
 goblint.domaintest
+goblint_http.exe
 src/config*.ml
 tests/bench.txt
 .DS_Store

docs/user-guide/inspecting.md

@@ -18,11 +18,10 @@ For the initial setup:
 
 To build GobView (also for development):
 
-1. Run `dune build gobview` in the analyzer directory to build the web UI
-2. The executable for the http-server can then be found in the directory `./_build/default/gobview/goblint-http-server`. It takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\
-`./_build/default/gobview/goblint-http-server/goblint_http.exe -with-goblint ../analyzer/goblint -goblint --set files[+] "../analyzer/tests/regression/00-sanity/01-assert.c"`
-
-4. Visit <http://localhost:8080>
+1. Run `make view` in the analyzer directory to build the web UI
+2. The executable `goblint_http.exe` takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\
+`./goblint_http.exe tests/regression/00-sanity/01-assert.c`
+3. Visit <http://localhost:8080>
 
 ## Witnesses
 

make.sh

@@ -33,6 +33,9 @@ rule() {
       dune build --profile=release $TARGET.exe &&
       rm -f goblint &&
       cp _build/default/$TARGET.exe goblint
+    ;; view)
+      eval $(opam config env)
+      dune build gobview
     # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable
     ;; js) # https://dune.readthedocs.io/en/stable/jsoo.html
       dune build $TARGET.bc.js &&

scripts/test-gobview.py

@@ -24,10 +24,8 @@ def cleanup(browser, thread):
 # serve GobView in different thread so it does not block the testing
 def serve():
   global p
-  goblint_http_path = '_build/default/gobview/goblint-http-server/goblint_http.exe'
-  p = subprocess.Popen(['./' + goblint_http_path,
-                  '-with-goblint', '../analyzer/goblint',
-                  '-goblint', '--set', 'files[+]', '"../analyzer/tests/regression/00-sanity/01-assert.c"'])
+  goblint_http_path = './goblint_http.exe'
+  p = subprocess.Popen([goblint_http_path, 'tests/regression/00-sanity/01-assert.c'])
 
 print("serving at port", PORT)
 thread = Thread(target=serve, args=())

src/maingoblint.ml

@@ -597,11 +597,7 @@ let do_html_output () =
 
 let do_gobview cilfile =
   let gobview = GobConfig.get_bool "gobview" in
-  let goblint_root = GobFpath.cwd_append (fst (Fpath.split_base (Fpath.v Sys.argv.(0)))) in
-  let dist_dir = Fpath.(goblint_root // (Fpath.v "_build/default/gobview/dist")) in
-  let js_file = Fpath.(dist_dir / "main.js") in
   if gobview then (
-    if Sys.file_exists (Fpath.to_string js_file) then (
       let save_run = GobConfig.get_string "save_run" in
       let run_dir = Fpath.v(if save_run <> "" then save_run else "run") in
       (* copy relevant c files to gobview directory *)
@@ -625,20 +621,7 @@ let do_gobview cilfile =
       (* marshal timing statistics *)
       let stats = Fpath.(run_dir / "stats.marshalled") in
       Serialize.marshal (Timing.Default.root, Gc.quick_stat ()) stats;
-      let dist_files =
-        Sys.files_of (Fpath.to_string dist_dir)
-        |> Enum.filter (fun n -> n <> "dune")
-        |> List.of_enum
-      in
-      List.iter (fun n ->
-          FileUtil.cp
-            [Fpath.to_string (Fpath.(dist_dir / n))]
-            (Fpath.to_string (Fpath.(run_dir / n)))
-        ) dist_files
     )
-    else
-      Logs.error "Warning: Cannot locate GobView."
-  )
 
 let handle_extraspecials () =
   let funs = get_string_list "exp.extraspecials" in