From 0c7249b992b59c8d1021251f11166bc44a8c57f3 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 10 Mar 2020 02:22:07 -0700 Subject: [PATCH] [sledge] Change build system to not generate dune files Reviewed By: jvillard Differential Revision: D20322877 fbshipit-source-id: 0034a4163 --- sledge/.gitignore | 4 --- sledge/Makefile | 47 ++++++------------------- sledge/bin/dune | 16 +++++++++ sledge/bin/dune.in | 22 ------------ sledge/dune-common.in | 59 -------------------------------- sledge/dune-workspace | 30 +++++++++++++--- sledge/lib/dune | 14 ++++++++ sledge/lib/dune.in | 21 ------------ sledge/lib/import/dune | 14 ++++++++ sledge/lib/import/dune.in | 22 ------------ sledge/ppx_trace/dune | 5 +++ sledge/sledge.opam | 4 +-- sledge/tools/opam/dev-tools.opam | 1 - 13 files changed, 88 insertions(+), 171 deletions(-) create mode 100644 sledge/bin/dune delete mode 100644 sledge/bin/dune.in delete mode 100644 sledge/dune-common.in create mode 100644 sledge/lib/dune delete mode 100644 sledge/lib/dune.in create mode 100644 sledge/lib/import/dune delete mode 100644 sledge/lib/import/dune.in diff --git a/sledge/.gitignore b/sledge/.gitignore index 6c3a91c5c..546811bc1 100644 --- a/sledge/.gitignore +++ b/sledge/.gitignore @@ -1,9 +1,5 @@ .llvm_build .llvm_install -.merlin -/bin/dune -/lib/dune -/lib/import/dune /llvm/ /test/*/*.bc /test/*/*.bc.err diff --git a/sledge/Makefile b/sledge/Makefile index 552a007d1..5c70c7f91 100644 --- a/sledge/Makefile +++ b/sledge/Makefile @@ -8,11 +8,10 @@ default: exes EXES = bin/sledge INSTALLS = sledge -FMTS = @_build/dbg/lib/fmt @_build/dbg/bin/fmt -DBG_TARGETS = $(patsubst %,_build/dbg/%.exe,$(EXES)) $(patsubst %,_build/dbg/%.install,$(INSTALLS)) _build/dbg/sledge-help.txt +DBG_TARGETS = $(patsubst %,_build/dbg/%.exe,$(EXES)) $(patsubst %,_build/dbg/%.install,$(INSTALLS)) -TARGETS = $(DBG_TARGETS) $(subst dbg,dbg-opt,$(DBG_TARGETS)) $(subst dbg,opt,$(DBG_TARGETS)) +TARGETS = $(DBG_TARGETS) $(subst dbg,dbg-opt,$(DBG_TARGETS)) $(subst dbg,opt,$(DBG_TARGETS)) _build/opt/sledge-help.txt dune_build_dbg = dune build $(DBG_TARGETS) dune_install_dbg = dune install --context=dbg --prefix=_build/_install/dbg sledge 2>/dev/null @@ -23,76 +22,52 @@ dune_install_dbg_opt = $(subst dbg,dbg-opt,$(dune_install_dbg)) dune_build_opt = $(subst dbg,opt,$(dune_build_dbg)) dune_install_opt = $(subst dbg,opt,$(dune_install_dbg)) -DUNEINS = $(shell find lib bin model -name dune.in) -DUNES = $(patsubst %.in,%,$(DUNEINS)) - -.PHONY: dunes -dunes: $(DUNES) - -%/dune: dune-common.in %/dune.in - cat $+ > $@ - -.PHONY: setup -setup: dunes - .PHONY: check -check: setup +check: dune build @check .PHONY: exes -exes: setup +exes: dune build $(TARGETS) $(dune_install_dbg) $(dune_install_dbg_opt) $(dune_install_opt) .PHONY: dbg -dbg: setup +dbg: $(dune_build_dbg) $(dune_install_dbg) .PHONY: do -do: setup +do: $(dune_build_dbg_opt) $(dune_install_dbg_opt) .PHONY: opt -opt: setup +opt: $(dune_build_opt) $(dune_install_opt) .PHONY: watch -watch: setup +watch: dune build --watch --terminal-persistence=clear-on-rebuild $(TARGETS) .PHONY: test -test: setup +test: -dune build @_build/dbg/runtest --auto-promote - dune build $(FMTS) --auto-promote + dune build @fmt --auto-promote .PHONY: ci-test -ci-test: setup +ci-test: dune build @_build/dbg/runtest -BISECT_DIR = $(CURDIR)/_coverage/out - -.PHONY: coverage -coverage: setup - rm -rf _coverage - mkdir -p $(BISECT_DIR) - BISECT_FILE=$(BISECT_DIR)/bisect dune build --force @_build/coverage/runtest - find $(BISECT_DIR) -type f | xargs bisect-ppx-report -I _build/coverage/ -text _coverage/summary.txt -html _coverage/ - @echo "open _coverage/index.html" - .PHONY: clean clean: dune clean - rm -rf _coverage $(DUNES) .PHONY: fmt fmt: dune build @fmt --auto-promote - ocamlformat -i $(DUNEINS) clang-format -i model/llair_intrinsics.h model/cxxabi.cpp ${MAKE} -C test fmt diff --git a/sledge/bin/dune b/sledge/bin/dune new file mode 100644 index 000000000..1b3fca0c6 --- /dev/null +++ b/sledge/bin/dune @@ -0,0 +1,16 @@ +; Copyright (c) Facebook, Inc. and its affiliates. +; +; This source code is licensed under the MIT license found in the +; LICENSE file in the root directory of this source tree. + +(executable + (public_name sledge) + (package sledge) + (libraries dune-build-info llvm llvm.irreader llvm.analysis llvm.scalar_opts + llvm.target llvm.ipo llvm.linker shexp.process yojson trace import + sledgelib model) + (flags + (:standard -open Import -open Sledgelib -open Model)) + (preprocess + (pps ppx_compare ppx_custom_printf ppx_expect ppx_hash ppx_here + ppx_inline_test ppx_let ppx_sexp_conv ppx_sexp_value ppx_trace))) diff --git a/sledge/bin/dune.in b/sledge/bin/dune.in deleted file mode 100644 index 376e16d3b..000000000 --- a/sledge/bin/dune.in +++ /dev/null @@ -1,22 +0,0 @@ -(* -*- tuareg -*- *) -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -let deps = ["import"; "libsledge"; "model"] - -;; -Jbuild_plugin.V1.send -@@ Format.sprintf - {| -(executable - (public_name sledge) - (package sledge) - (libraries dune-build-info llvm llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo llvm.linker shexp.process yojson %s) - %s) -|} - (libraries ("trace" :: deps)) - (flags `exe deps) diff --git a/sledge/dune-common.in b/sledge/dune-common.in deleted file mode 100644 index b62182d00..000000000 --- a/sledge/dune-common.in +++ /dev/null @@ -1,59 +0,0 @@ -(* -*- tuareg -*- *) -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -let common_flags = - {|(-w +a-4-9-18-40-42-44-48@50-66 - -strict-formats -strict-sequence - -short-paths -bin-annot -keep-docs - -unboxed-types)|} - -let ocamlc_flags = - match Jbuild_plugin.V1.context with - | "opt" | "dbg-opt" -> "-w -26-32 -noassert" - | _ -> "-g" - -let ocamlopt_flags = - match Jbuild_plugin.V1.context with - | "opt" | "dbg-opt" -> ocamlc_flags ^ " -w -a -O3" - | _ -> ocamlc_flags - -let coverage_ppx = - match Jbuild_plugin.V1.context with "coverage" -> "bisect_ppx" | _ -> "" - -let ppx_flags = - match Jbuild_plugin.V1.context with - | "dbg" | "dbg-opt" -> "--debug" - | _ -> "" - -let flags exe_or_lib deps = - Printf.sprintf - {|(flags (%s %s)) - (ocamlc_flags (%s)) - (ocamlopt_flags (%s)) - (preprocess - (pps - ppx_compare - ppx_custom_printf - ppx_expect - ppx_hash - ppx_here - ppx_inline_test - ppx_let - ppx_sexp_conv - ppx_sexp_value - ppx_trace - %s - %s)) - %s|} - common_flags - (String.concat " " - (List.map (fun d -> "-open " ^ String.capitalize_ascii d) deps)) - ocamlc_flags ocamlopt_flags ppx_flags coverage_ppx - (match exe_or_lib with `lib -> "(inline_tests)" | _ -> "") - -let libraries deps = String.concat " " deps diff --git a/sledge/dune-workspace b/sledge/dune-workspace index f250274f4..a7b15e663 100644 --- a/sledge/dune-workspace +++ b/sledge/dune-workspace @@ -5,7 +5,29 @@ ; This source code is licensed under the MIT license found in the ; LICENSE file in the root directory of this source tree. -(context (opam (switch sledge) (name dbg) (merlin))) -(context (opam (switch sledge) (name dbg-opt))) -(context (opam (switch sledge) (name opt))) -(context (opam (switch sledge) (name coverage))) +(env + (dbg + (flags + (-w +a-4-9-18-40-42-44-48@50-66 -strict-formats -strict-sequence + -short-paths -bin-annot -keep-locs -keep-docs -opaque)) + (env-vars + (PPX_TRACE_ENABLED 1)) + (inline_tests enabled)) + (opt + (flags + (-w -a -noassert -unboxed-types)) + (ocamlopt_flags (-O3)) + (env-vars + (PPX_TRACE_ENABLED 0)) + (inline_tests disabled)) + (dbg-opt + (flags + (-w -a -noassert -unboxed-types)) + (ocamlopt_flags (-O3)) + (env-vars + (PPX_TRACE_ENABLED 1)) + (inline_tests disabled))) + +(context (opam (switch sledge) (name dbg) (profile dbg) (merlin))) +(context (opam (switch sledge) (name opt) (profile opt))) +(context (opam (switch sledge) (name dbg-opt) (profile dbg-opt))) diff --git a/sledge/lib/dune b/sledge/lib/dune new file mode 100644 index 000000000..89cc52564 --- /dev/null +++ b/sledge/lib/dune @@ -0,0 +1,14 @@ +; Copyright (c) Facebook, Inc. and its affiliates. +; +; This source code is licensed under the MIT license found in the +; LICENSE file in the root directory of this source tree. + +(library + (name sledgelib) + (libraries apron apron.boxMPQ ctypes ctypes.foreign trace import) + (flags + (:standard -open Import)) + (preprocess + (pps ppx_compare ppx_custom_printf ppx_expect ppx_hash ppx_here + ppx_inline_test ppx_let ppx_sexp_conv ppx_sexp_value ppx_trace)) + (inline_tests)) diff --git a/sledge/lib/dune.in b/sledge/lib/dune.in deleted file mode 100644 index e9c1b8fcd..000000000 --- a/sledge/lib/dune.in +++ /dev/null @@ -1,21 +0,0 @@ -(* -*- tuareg -*- *) -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -let deps = ["import"] - -;; -Jbuild_plugin.V1.send -@@ Format.sprintf - {| -(library - (name libsledge) - (libraries apron apron.boxMPQ ctypes ctypes.foreign %s) - %s) -|} - (libraries ("trace" :: deps)) - (flags `lib deps) diff --git a/sledge/lib/import/dune b/sledge/lib/import/dune new file mode 100644 index 000000000..7a05cf0f2 --- /dev/null +++ b/sledge/lib/import/dune @@ -0,0 +1,14 @@ +; Copyright (c) Facebook, Inc. and its affiliates. +; +; This source code is licensed under the MIT license found in the +; LICENSE file in the root directory of this source tree. + +(library + (name import) + (public_name sledge.import) + (libraries core core_kernel.fheap zarith trace) + (flags (:standard)) + (preprocess + (pps ppx_compare ppx_custom_printf ppx_expect ppx_hash ppx_here + ppx_inline_test ppx_let ppx_sexp_conv ppx_sexp_value ppx_trace)) + (inline_tests)) diff --git a/sledge/lib/import/dune.in b/sledge/lib/import/dune.in deleted file mode 100644 index 258310500..000000000 --- a/sledge/lib/import/dune.in +++ /dev/null @@ -1,22 +0,0 @@ -(* -*- tuareg -*- *) -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -let deps = [] - -;; -Jbuild_plugin.V1.send -@@ Format.sprintf - {| -(library - (name import) - (public_name sledge.import) - (libraries core core_kernel.fheap zarith %s) - %s) -|} - (libraries ("trace" :: deps)) - (flags `lib deps) diff --git a/sledge/ppx_trace/dune b/sledge/ppx_trace/dune index dd4d5b14a..45c1c7126 100644 --- a/sledge/ppx_trace/dune +++ b/sledge/ppx_trace/dune @@ -1,3 +1,8 @@ +; Copyright (c) Facebook, Inc. and its affiliates. +; +; This source code is licensed under the MIT license found in the +; LICENSE file in the root directory of this source tree. + (library (name ppx_trace) (kind ppx_rewriter) diff --git a/sledge/sledge.opam b/sledge/sledge.opam index ecef409ed..7d0e5eb3a 100644 --- a/sledge/sledge.opam +++ b/sledge/sledge.opam @@ -6,8 +6,8 @@ bug-reports: "https://github.com/facebook/infer/issues/new?template=sledge_issue dev-repo: "git://github.com/facebook/infer.git" license: "MIT" build: [ - [make "setup"] - ["dune" "build" "-p" name "--profile" "opt" "-j" jobs] + ["dune" "build" "_build/opt/bin/sledge.exe" "-j" jobs] + ["dune" "install" "--context=opt" "sledge"] ] depends: [ "ocaml" diff --git a/sledge/tools/opam/dev-tools.opam b/sledge/tools/opam/dev-tools.opam index 734e5a9c2..316d15fdb 100644 --- a/sledge/tools/opam/dev-tools.opam +++ b/sledge/tools/opam/dev-tools.opam @@ -2,7 +2,6 @@ opam-version: "1.2" name: "dev-tools" version: "0.1" depends: [ - "bisect_ppx" {>= "1.3.4"} "merlin" "ocp-indent" "patdiff"