Fix build issues with core due to ocaml/dune#567

Switched to jbuilder now :)

.gitignore

@@ -1,15 +1,23 @@
-# OASIS Files
-_build
-*.native
-*.byte
-*.docdir
+*.annot
+*.cmo
+*.cma
+*.cmi
+*.a
+*.o
+*.cmx
+*.cmxs
+*.cmxa
+
+# ocamlbuild working directory
+_build/
 
-setup.data
-setup.log
-setup.ml
+# ocamlbuild targets
+*.byte
+*.native
 
-Makefile
-configure
+# jbuilder generated files
+*/.merlin
+*.install
 
 # External
 _dep
@@ -20,4 +28,7 @@ _comp
 ocamlprof.dump
 gmon.out
 *.tgz
-_tags
+_tags
+_bin
+flambda_flags
+starexec

LICENSE.md

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2018 Saswat Padhi
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

opam → LoopInvGen.opam

@@ -14,16 +14,11 @@ dev-repo: "git+https://github.com:SaswatPadhi/LoopInvGen.git"
 available: [ ocaml-version >= "4.04.2" ]
 
 build: [
-  ["oasis" "setup" "-setup-update" "dynamic"]
-  ["./configure" "--disable-tests" "--disable-debug" "--disable-profile"]
-  [make]
+  [ "jbuilder" "build" "-p" name "-j" jobs ]
 ]
 
 depends: [
-  "ocamlfind"     {build}
-  "base-bytes"    {build}
-  "base-threads"  {build}
-  "oasis"         {build & >= "0.4"}
+  "jbuilder"      {build & >= "1.0+beta10"}
   "alcotest"      {test & >= "0.7"}
   "core"          {>= "0.10"}
   "core_extended" {>= "0.10"}

README.md

@@ -6,21 +6,25 @@ A loop invariant generator.
 
 #### 1. Install `ocaml` >= 4.04.2.
 It is recommended to use an OCaml compiler with [`flambda`][flambda] optimizations enabled.
-For example, with [`opam`](https://opam.ocaml.org/), you could run `opam switch 4.06.1+flambda`.
+For example, with [`opam`](https://opam.ocaml.org/), you could:
+- run `opam switch 4.06.1+flambda` for opam 1.x
+- run `opam switch create 4.06.1+flambda` for opam 2.x
 
 #### 2. Install (for example, using `opam install`) the following packages:
 ```
-  "alcotest"      {>= "0.7"}
   "core"          {>= "0.10"}
   "core_extended" {>= "0.10"}
-  "oasis"         {>= "0.4"}
 ```
 
-#### 3. Run `./create-package.sh -z /PATH/TO/z3`.
+#### 3. `git checkout` the [Z3 project][z3].
+
+#### 4. Run `./create-package.sh -z /PATH/TO/z3`.
 The `create-package.sh` script would build Z3, copy it to `./_dep/`, and then build LoopInvGen.
 Alternatively, you can copy a precompiled version of Z3 to `./_dep/`, and simply run `./create-package.sh`.
 
-For future builds after any chances to the source code, you only need to `make`.
+For future builds after any chances to the source code, you only need to run `jbuilder build`.
+
+You can also configure the build mode to either `fast-compile` (default) or `optimize`, using: `jbuilder build -f @<mode>`.
 
 ## Testing
 
@@ -34,4 +38,5 @@ Run `./loopinvgen.sh /path/to/sygus.sl` to infer the loop invariant for the SuGu
 
 
 [flambda]: https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html
-[travis]:  https://travis-ci.org/SaswatPadhi/LoopInvGen
+[travis]:  https://travis-ci.org/SaswatPadhi/LoopInvGen
+[z3]:      https://github.com/Z3Prover/z3

create-package.sh

@@ -21,8 +21,8 @@ eval set -- "$OPTS"
 
 JOBS="4"
 MAKE_Z3=""
-OPTIMIZE=""
 
+jbuilder build -f @fast-compile
 while true ; do
   case "$1" in
     -z | --make-z3 )
@@ -32,7 +32,7 @@ while true ; do
          JOBS="$2" ;
          shift ; shift ;;
     -O | --optimize )
-         OPTIMIZE="--enable-optimize" ;
+         jbuilder build -f @optimize
          shift ;;
     -- ) shift; break ;;
     * ) break ;;
@@ -54,55 +54,48 @@ if [ -n "$MAKE_Z3" ] ; then
   make -j "$JOBS"
 
   mkdir -p "$LIG/_dep"
-  cp z3 "$LIG/_dep/z3.bin"
+  cp z3 "$LIG/_dep/z3"
   cd "$LIG"
 fi
 
-oasis setup -setup-update dynamic
+jbuilder build @local -p LoopInvGen -j "$JOBS"
 
-make distclean
+rm -rf starexec && mkdir -p starexec/bin
 
-./configure --disable-debug --disable-profile \
-            --disable-tests --disable-docs \
-            $OPTIMIZE
-make -j "$JOBS"
+cp -rL _bin _dep loopinvgen.sh starexec/bin
 
-rm -rf bin && mkdir -p bin
-
-cp _dep/z3.bin bin/z3
-cp _build/src/Record.native \
-   _build/src/Infer.native  \
-   _build/src/Verify.native \
-   loopinvgen.sh            \
-   bin
-
-cat <<EOF > bin/starexec_run_default
+cat <<EOF > starexec/bin/starexec_run_default
 #!/bin/bash
 
-./loopinvgen.sh -t 36000 -p "." -z "./z3" "\$1"
+./loopinvgen.sh -t 36000 -p "." -z "_dep/z3" "\$1"
 EOF
-chmod +x bin/starexec_run_default
+chmod +x starexec/bin/starexec_run_default
 
-cat <<EOF > bin/starexec_run_debug
+cat <<EOF > starexec/bin/starexec_run_debug
 #!/bin/bash
 
 pwd
 ls -lah
-file z3 Record.native Infer.native Verify.native
-ldd z3 Record.native Infer.native Verify.native
-./z3
-./Record.native
+
+file _dep/z3 _bin/lig-record _bin/lig-infer _bin/lig-verify
+ldd _dep/z3 _bin/lig-record _bin/lig-infer _bin/lig-verify
+
+_dep/z3
+_bin/lig-record -h
+_bin/lig-infer -h
+_bin/lig-verify -h
 EOF
-chmod +x bin/starexec_run_debug
+chmod +x starexec/bin/starexec_run_debug
 
-cat <<EOF > starexec_description.txt
+cat <<EOF > starexec/starexec_description.txt
 A loop invariant inference tool built using PIE: precondition inference engine.
 
 https://github.com/SaswatPadhi/LoopInvGen
 EOF
 
-chmod -R 777 bin
-CONTENTS="bin starexec_description.txt"
+chmod -R 777 starexec/bin
 
-tar cvzf LoopInvGen_SyGuS_INV.tgz $CONTENTS
-rm -rf $CONTENTS
+echo -ne "\nPreparing starexec package (starexec/):\n"
+cd starexec
+tar cvzf ../LoopInvGen_SyGuS_INV.tgz ./*
+#rm -rf starexec

loopinvgen.sh

@@ -1,19 +1,27 @@
 #!/bin/bash
 
+BIN_DIR="_bin"
+
+RECORD="$BIN_DIR/lig-record"
+INFER="$BIN_DIR/lig-infer"
+VERIFY="$BIN_DIR/lig-verify"
+
+if [ ! -f $RECORD ] || [ ! -f $INFER ] || [ ! -f $VERIFY ] ; then
+  echo -en "
+Building OCaml modules ...
+" 1>&2 ; jbuilder build @local
+fi
+
 trap 'jobs -p | xargs kill >&2 2> /dev/null' EXIT
 
 INTERMEDIATES_DIR="_log"
 SYGUS_EXT=".sl"
-Z3_PATH="_dep/z3.bin"
+Z3_PATH="_dep/z3"
 
 MIN_STATES=63
 MIN_TIMEOUT=5
 MAX_STATES=1024
 
-RECORD="./Record.native"
-INFER="./Infer.native"
-VERIFY="./Verify.native"
-
 FORKS=2
 STATES=512
 
@@ -56,14 +64,13 @@ Configuration:
     [--max-states, -m <count>]        ($MAX_STATES)\t{> 0}
     [--record-states, -s <count>]     ($STATES)\t{> $MIN_STATES}
     [--timeout, -t <seconds>]         ($TIMEOUT)\t{> $MIN_TIMEOUT}
-    [--z3-path, -z <path>]            (_dep/z3.bin)
+    [--z3-path, -z <path>]            (_dep/z3)
 
 Arguments to Internal Programs:
     [--Record-args, -R \"<args>\"]    for ${RECORD}
     [--Infer-args, -I \"<args>\"]     for ${INFER}
     [--Verify-args, -V \"<args>\"]    for ${VERIFY}
-" 1>&2 ;
-  exit 1 ;
+" 1>&2 ; exit -1
 }
 
 OPTS=`getopt -n 'parse-options' -o :R:I:V:vip:l:cs:m:t:z: --long Record-args:,Infer-args:,Verify-args:,verify,interactive,intermediate-path:,logging:,clean-intermediates,record-states:,max-states:,timeout:,z3-path: -- "$@"`

src/jbuild

@@ -0,0 +1,42 @@
+(jbuild_version 1)
+
+(alias
+    ((name local)
+     (action
+        (progn
+            (bash "mkdir -p ${SCOPE_ROOT}/../../_bin")
+            (bash "ln -srf ${bin:lig-record} ${SCOPE_ROOT}/../../_bin/lig-record")
+            (bash "ln -srf ${bin:lig-infer} ${SCOPE_ROOT}/../../_bin/lig-infer")
+            (bash "ln -srf ${bin:lig-verify} ${SCOPE_ROOT}/../../_bin/lig-verify")))))
+
+(alias
+    ((name optimize)
+     (action
+        (progn
+            (bash "echo -ne 'Current build mode is set to [optimize].\nNote that build may take significantly longer!\nUse (jbuilder build -f @fast-compile) to switch to [fast-compile] mode.'")
+            (bash "echo -ne '(-linkall -O3 -rounds 13)' > ${SCOPE_ROOT}/../../src/flambda_flags")))))
+
+(alias
+    ((name fast-compile)
+     (action
+        (progn
+            (bash "echo -ne 'Current build mode is set to [fast-compile].\nUse (jbuilder build -f @optimize) to generate highly optimized binaries.'")
+            (bash "echo -ne '()' > ${SCOPE_ROOT}/../../src/flambda_flags")))))
+
+(rule
+    ((targets (flambda_flags))
+     (deps ((alias fast)))
+     (mode fallback)
+     (action
+        (bash "cp ${SCOPE_ROOT}/../../src/flambda_flags ."))))
+
+(alias
+    ((name clean)
+     (action
+        (bash "rm -rf ${SCOPE_ROOT}/../../src/flambda_flags ${SCOPE_ROOT}/../../_bin"))))
+
+(executables
+    ((names (Record Infer Verify))
+     (public_names (lig-record lig-infer lig-verify))
+     (ocamlopt_flags (:standard (:include flambda_flags)))
+     (libraries (core core_extended))))