build with dune instead of ocamlbuild (#79), travis caching

clean build now 17s vs 1m09s before rebuild now 0.5s vs. 4s before travis total now ~16m vs. 29-40m before * tried to use jbuilder (now dune): ppx_import did not work * jbuild -> dune * dune: can not compile pinned goblint-cil b/c no Pretty etc. in its META file * cleanup src/dune: `copy_files` no longer needed because of `include_subdirs` * pin ppx_distr_guards until omp-version available opam pin add ppx_distr_guards https://github.com/vogler/ppx_distr_guards.git * dune: forgot to commit * `make dune` builds, TODO gen&build src/goblint.ml instead of maingoblint * done. clean `make dune` takes 17s vs 1m09s `make`; rerun: 0.5s vs. 4s * make dune default, cleanup/comment make.sh * opam lock * travis: upgrade osx_image as for goblint-cil * travis: cache local opam switch? * ignore Warning 27: unused variable * dune: generate_opam_files * adding cil as git submodule/vendored_dir instead of opam package also works * Revert "travis: cache local opam switch?" TODO: only create switch if _build does not exist and otherwise just install into it? Travis: $ opam switch -y create . --deps-only ocaml-base-compiler.4.09.0 --locked [ERROR] Directory "/Users/travis/build/goblint/analyzer/_opam" already exists, please choose a different name This reverts commit ffcd2fc. * travis (macos): debug why some analysis and solvers are not registered * opam.locked -> goblint.opam.locked * travis (macos): why does ls stop listing files? try find instead. * travis (macos): diff seems fine, list both ls and find * travis: cache _opam (do not create local switch if it exists), debug missing files * travis creates cached directories before they're cached... * travis build now works (generate src/goblint.ml before dune build) Why is this only a problem on travis and not locally? * fix Dockerfile: opam* -> goblint.opam* * only install opam; no brew update * travis (macos): brew install via travis addon which does not run update * travis (macos): homebrew addon does not work without update -> no way around it
goblint · Mar 4, 2020 · 3962b81 · 3962b81
1 parent c3c9d47
commit 3962b81
Show file tree

Hide file tree

Showing 14 changed files with 226 additions and 102 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -1,13 +1,14 @@
 os:
   - linux
   - osx
-osx_image: xcode10
+osx_image: xcode11.2
 language: c
 git:
   submodules: false
 cache:
   directories:
   - $HOME/.opam
+  - _opam
 install: bash -x scripts/travis-ci.sh
 script: ./make.sh headers testci
 addons:

diff --git a/Dockerfile b/Dockerfile
@@ -15,7 +15,7 @@ WORKDIR /home/opam/analyzer
 # Download linux-headers before installing dependencies, so that this can be cached separately.
 RUN ./make.sh headers
 # dependencies and their locked versions; upgraded versions will only be installed after a change to opam.locked
-COPY --chown=opam opam opam.locked /home/opam/analyzer/
+COPY --chown=opam goblint.opam goblint.opam.locked /home/opam/analyzer/
 # The base image uses a local opam repository which can (did) lag behind the online one. If we upgraded locally, we also want it to work in the container and not wait until the change made it into the base image. Thus, add the online version as default before we update.
 RUN opam repository set-url default https://opam.ocaml.org/
 # install locked dependencies

diff --git a/Makefile b/Makefile
@@ -1,5 +1,4 @@
-opt :
+native :
 
 % :
 	@./make.sh $@
-
diff --git a/dune-project b/dune-project
@@ -0,0 +1,38 @@
+(lang dune 1.11)
+(name goblint)
+; build failed with: Files src/.maingoblint.eobjs/native/mutex.cmx and _opam/lib/ocaml/threads/threads.cmxa both define a module named Mutex
+; maybe related: https://github.com/ocaml/dune/issues/1727, https://github.com/ocaml/dune/issues/597
+; (implicit_transitive_deps false) ; does not help about the pulled-in Mutex from ocaml/threads
+(wrapped_executables true) ; prefix compilation unit names; mentioned here: https://github.com/ocaml/ocaml/pull/2218#issuecomment-572043299; doc says it's the default since dune 2.0, but it somehow still fixes the clash
+
+; https://dune.readthedocs.io/en/stable/dune-files.html#generate-opam-files
+(generate_opam_files true)
+
+(source (github goblint/analyzer))
+(homepage "https://goblint.in.tum.de")
+(documentation "https://goblint.github.io/analyzer")
+(authors "Vesal Vojdani, Kalmer Apinis, Ralf Vogler, Michael Schwarz, Julian Erhard")
+(maintainers "Michael Schwarz <[email protected]>" "Ralf Vogler <[email protected]>")
+(license MIT)
+
+(package
+  (name goblint)
+  (synopsis "Static analysis framework for concurrent C")
+  (depends
+    (ocaml (>= 4.04.1)) ; TODO check with travis env matrix as for goblint-cil
+    dune
+    goblint-cil ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
+    batteries
+    xml-light
+    (ppx_distr_guards (>= 0.2))
+    ppx_import
+    ppx_deriving
+    ppx_deriving_yojson
+    ocaml-monadic
+    (ounit2 :with-test)
+    (odoc :with-doc)
+    ; TODO still need the following after switch to dune?
+    ocamlbuild
+    ocamlfind
+  )
+)
diff --git a/goblint.opam b/goblint.opam
@@ -0,0 +1,48 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Static analysis framework for concurrent C"
+maintainer: [
+  "Michael Schwarz <[email protected]>"
+  "Ralf Vogler <[email protected]>"
+]
+authors: [
+  "Vesal Vojdani, Kalmer Apinis, Ralf Vogler, Michael Schwarz, Julian Erhard"
+]
+license: "MIT"
+homepage: "https://goblint.in.tum.de"
+doc: "https://goblint.github.io/analyzer"
+bug-reports: "https://github.com/goblint/analyzer/issues"
+depends: [
+  "ocaml" {>= "4.04.1"}
+  "dune"
+  "goblint-cil"
+  "batteries"
+  "xml-light"
+  "ppx_distr_guards" {>= "0.2"}
+  "ppx_import"
+  "ppx_deriving"
+  "ppx_deriving_yojson"
+  "ocaml-monadic"
+  "ounit2" {with-test}
+  "odoc" {with-doc}
+  "ocamlbuild"
+  "ocamlfind"
+]
+build: [
+  ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/goblint/analyzer.git"
+pin-depends: [
+  [ "goblint-cil.1.7.4" "git+https://github.com/goblint/cil.git" ]
+]
diff --git a/opam.locked → goblint.opam.locked b/opam.locked → goblint.opam.locked
@@ -1,15 +1,19 @@
 opam-version: "2.0"
-name: "goblint"
-maintainer: "Ralf Vogler <[email protected]>"
-authors: "Vesal Vojdani, Kalmer Apinis, Ralf Vogler"
+synopsis: "Static analysis framework for concurrent C"
+maintainer: [
+  "Michael Schwarz <[email protected]>"
+  "Ralf Vogler <[email protected]>"
+]
+authors: [
+  "Vesal Vojdani, Kalmer Apinis, Ralf Vogler, Michael Schwarz, Julian Erhard"
+]
 license: "MIT"
-homepage: "https://github.com/goblint/analyzer"
+homepage: "https://goblint.in.tum.de"
+doc: "https://goblint.github.io/analyzer"
 bug-reports: "https://github.com/goblint/analyzer/issues"
-dev-repo: "git+https://github.com/goblint/analyzer.git"
-build: [make]
-run-test: [make "test"]
 depends: [
   "base" {= "v0.13.1"}
+  "base-bigarray" {= "base"}
   "base-threads" {= "base"}
   "base-unix" {= "base"}
   "batteries" {= "3.0.0"}
@@ -18,39 +22,53 @@ depends: [
   "conf-m4" {= "1"}
   "conf-perl" {= "1"}
   "cppo" {= "1.6.6"}
-  "dune" {= "1.11.4"}
-  "dune-configurator" {= "1.0.0"}
+  "dune" {= "2.3.1"}
+  "dune-configurator" {= "2.3.1"}
+  "dune-private-libs" {= "2.3.1"}
   "easy-format" {= "1.3.2"}
   "goblint-cil" {= "1.7.4"}
   "num" {= "1.3"}
   "ocaml" {= "4.09.0"}
+  "ocaml-base-compiler" {= "4.09.0"}
   "ocaml-compiler-libs" {= "v0.12.1"}
-  "ocaml-migrate-parsetree" {= "1.5.0"}
+  "ocaml-config" {= "1"}
+  "ocaml-migrate-parsetree" {= "1.6.0"}
   "ocaml-monadic" {= "0.4.1"}
   "ocamlbuild" {= "0.14.0"}
   "ocamlfind" {= "1.8.1"}
   "ppx_derivers" {= "1.2.1"}
   "ppx_deriving" {= "4.4.1"}
   "ppx_deriving_yojson" {= "3.5.2"}
-  "ppx_distr_guards" {= "0.1"}
-  "ppx_import" {= "1.7.0"}
+  "ppx_distr_guards" {= "0.2"}
+  "ppx_import" {= "1.7.1"}
   "ppx_tools" {= "6.0+4.08.0"}
   "ppx_tools_versioned" {= "5.2.3"}
-  "ppxfind" {= "1.3"}
+  "ppxfind" {= "1.4"}
   "ppxlib" {= "0.12.0"}
-  "result" {= "1.4"}
+  "result" {= "1.5"}
   "sexplib0" {= "v0.13.0"}
   "stdio" {= "v0.13.0"}
   "xml-light" {= "2.4"}
   "yojson" {= "1.7.0"}
   "zarith" {= "1.9.1"}
 ]
+build: [
+  ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/goblint/analyzer.git"
 pin-depends: [
   [ "goblint-cil.1.7.4" "git+https://github.com/goblint/cil.git" ]
 ]
-synopsis: "Static analysis framework for concurrent C"
-url {
-  src: "https://github.com/goblint/analyzer/archive/goblint-1.0.0.tar.gz"
-  checksum: "md5=dd3ff7266e17f2772a17609d6bd960b8"
-}
+name: "goblint"
 version: "dev"
diff --git a/goblint.opam.template b/goblint.opam.template
@@ -0,0 +1,3 @@
+pin-depends: [
+  [ "goblint-cil.1.7.4" "git+https://github.com/goblint/cil.git" ]
+]
diff --git a/make.sh b/make.sh
@@ -3,16 +3,11 @@ set -e # exit immediately if a command fails
 set -o pipefail # or all $? in pipe instead of returning exit code of the last command only
 
 TARGET=src/goblint
-FLAGS="-cflag -annot -tag bin_annot -X webapp -no-links -use-ocamlfind -j 8 -no-log -ocamlopt opt -cflag -g"
-OCAMLBUILD=ocamlbuild
-EXCLUDE="_build|goblint.ml|apronDomain|poly"
 
-ocb() {
-  command -v opam >/dev/null 2>&1 && eval $(opam config env)
+gen() { # generate configuration files and goblint.ml which opens all modules in src/ such that they will be linked and executed without the need to be referenced somewhere else
   scripts/set_version.sh # generate the version file
-  ls -1 src/**/*.ml | egrep -v $EXCLUDE | perl -pe 's/.*\/(.*)\.ml/open \u$1/g' > $TARGET.ml
+  ls -1 src/**/*.ml | egrep -v "goblint.ml|apronDomain|poly" | perl -pe 's/.*\/(.*)\.ml/open \u$1/g' > $TARGET.ml
   echo "open Maingoblint" >> $TARGET.ml
-  $OCAMLBUILD $FLAGS $*
 }
 
 opam_setup() {
@@ -23,21 +18,36 @@ opam_setup() {
   # opam install camlp4 mongo # camlp4 needed for mongo
 }
 
+# deprecated, use dune which is much faster
+OCBFLAGS="-cflag -annot -tag bin_annot -X webapp -no-links -use-ocamlfind -j 8 -no-log -ocamlopt opt -cflag -g"
+ocb() {
+  command -v opam >/dev/null 2>&1 && eval $(opam config env)
+  gen
+  ocamlbuild $OCBFLAGS $*
+}
+
 rule() {
   case $1 in
+    # new rules using dune
     clean)
-      rm -rf goblint goblint.byte arinc doclist.odocl $TARGET.ml;
-      ocb -clean
-    ;; opt | nat*)
+      git clean -X -f
+      dune clean
+    ;; gen) gen
+    ;; nat*)
+      dune build $TARGET.exe &&
+      cp _build/default/$TARGET.exe goblint
+    ;; release)
+      dune build --profile release $TARGET.exe &&
+      cp _build/default/$TARGET.exe goblint
+    # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable
+
+    # old rules using ocamlbuild
+    ;; ocbnat*)
       ocb -no-plugin $TARGET.native &&
       cp _build/$TARGET.native goblint
     ;; debug)
       ocb -tag debug $TARGET.d.byte &&
       cp _build/$TARGET.d.byte goblint.byte
-    ;; warn)
-      # be pedantic and show all warnings
-      $OCAMLBUILD $FLAGS -no-plugin -cflags "-w +a" $TARGET.native && # copied b/c passing a quoted argument to a function does not work
-      cp _build/$TARGET.native goblint
     ;; profile)
       # gprof (run only generates gmon.out). use: gprof goblint
       ocb -tag profile $TARGET.p.native &&
@@ -46,14 +56,14 @@ rule() {
       # gprof & ocamlprof (run also generates ocamlprof.dump). use: ocamlprof src/goblint.ml
       ocb -ocamlopt ocamloptp $TARGET.p.native &&
       cp _build/$TARGET.p.native goblint
-    ;; docs)
-      rm -rf doc;
-      ls src/**/*.ml | egrep -v $EXCLUDE  | sed 's/.*\/\(.*\)\.ml/\1/' > doclist.odocl;
-      ocb -ocamldoc ocamldoc -docflags -charset,utf-8,-colorize-code,-keep-code doclist.docdir/index.html;
-      rm doclist.odocl;
-      ln -sf _build/doclist.docdir doc
-    ;; tag*)
-      otags -vi `find src/ -iregex [^.]*\.mli?`
+    # ;; docs)
+    #   rm -rf doc;
+    #   ls src/**/*.ml | egrep -v $EXCLUDE  | sed 's/.*\/\(.*\)\.ml/\1/' > doclist.odocl;
+    #   ocb -ocamldoc ocamldoc -docflags -charset,utf-8,-colorize-code,-keep-code doclist.docdir/index.html;
+    #   rm doclist.odocl;
+    #   ln -sf _build/doclist.docdir doc
+    # ;; tag*)
+    #   otags -vi `find src/ -iregex [^.]*\.mli?`
     ;; poly)
       echo "open ApronDomain" >> $TARGET.ml
       echo "open Poly" >> $TARGET.ml
@@ -62,18 +72,8 @@ rule() {
     ;; arinc)
       ocb src/mainarinc.native &&
       cp _build/src/mainarinc.native arinc
-    ;; npm)
-      if test ! -e "webapp/package.json"; then
-        git submodule update --init --recursive webapp
-      fi
-      cd webapp && npm install && npm start
-    ;; jar)
-      echo "Make sure you have the following installed: javac, ant"
-      if test ! -e "g2html/build.xml"; then
-        git submodule update --init --recursive g2html
-      fi
-      cd g2html && ant jar && cd .. &&
-      cp g2html/g2html.jar .
+
+    # setup, dependencies
     ;; deps)
       opam update; opam install -y . --deps-only --locked
     ;; setup)
@@ -90,10 +90,6 @@ rule() {
       cd .git/hooks; ln -s ../../scripts/hooks/pre-commit; cd -
       echo "Installing gem parallel (not needed for ./scripts/update_suite.rb -s)"
       sudo gem install parallel
-    ;; lock)
-      opam lock
-    ;; watch)
-      fswatch --event Updated -e $TARGET.ml src/ | xargs -n1 -I{} make
     ;; headers)
       curl -L -O https://github.com/goblint/linux-headers/archive/master.tar.gz
       tar xf master.tar.gz && rm master.tar.gz
@@ -102,10 +98,30 @@ rule() {
       cp linux-headers/include/linux/compiler-gcc5.h linux-headers/include/linux/compiler-gcc7.h
       cp linux-headers/include/linux/compiler-gcc5.h linux-headers/include/linux/compiler-gcc8.h
       cp linux-headers/include/linux/compiler-gcc5.h linux-headers/include/linux/compiler-gcc9.h
+    ;; lock)
+      opam lock
+    ;; npm)
+      if test ! -e "webapp/package.json"; then
+        git submodule update --init --recursive webapp
+      fi
+      cd webapp && npm install && npm start
+    ;; jar)
+      echo "Make sure you have the following installed: javac, ant"
+      if test ! -e "g2html/build.xml"; then
+        git submodule update --init --recursive g2html
+      fi
+      cd g2html && ant jar && cd .. &&
+      cp g2html/g2html.jar .
+    # ;; watch)
+    #   fswatch --event Updated -e $TARGET.ml src/ | xargs -n1 -I{} make
+
+    # tests, CI
     ;; test)
       ./scripts/update_suite.rb # run regression tests
+    ;; unit)
+      ocamlbuild -use-ocamlfind unittest/mainTest.native && ./mainTest.native
     ;; testci)
-      ruby scripts/update_suite.rb -s -d
+      ruby scripts/update_suite.rb -s -d # -s: run tests sequentially instead of in parallel such that output is not scrambled, -d shows some stats?
     ;; travis) # run a travis docker container with the files tracked by git - intended to debug setup problems on travis-ci.com
       echo "run ./scripts/travis-ci.sh to setup ocaml"
       # echo "bind-mount cwd: beware that cwd of host can be modified and IO is very slow!"
@@ -116,18 +132,17 @@ rule() {
     ;; docker) # build and run a docker image
       docker build --pull -t goblint . | ts -i
       docker run -it goblint bash
-    ;; unit)
-      ocamlbuild -use-ocamlfind unittest/mainTest.native && ./mainTest.native
     ;; server)
       rsync -avz --delete --exclude='/.git' --exclude='server.sh' --exclude-from="$(git ls-files --exclude-standard -oi --directory > /tmp/excludes; echo /tmp/excludes)" . serverseidl6.informatik.tu-muenchen.de:~/analyzer2
       ssh serverseidl6.informatik.tu-muenchen.de 'cd ~/analyzer2; make nat && make test'
+
     ;; *)
       echo "Unknown action '$1'. Try clean, opt, debug, profile, byte, or doc.";;
   esac;
 }
 
 if [ $# -eq 0 ]; then
-  rule nat
+  rule native
 else
   while [ $# -gt 0 ]; do
     rule $1;