Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

On macos, depqbf gives a Dl error #4

Closed
wants to merge 5 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions .travis-ci.sh
Original file line number Diff line number Diff line change
Expand Up @@ -14,15 +14,15 @@ case "$TRAVIS_OS_NAME" in
;;
osx)
brew update > /dev/null
brew install opam # 'gmp' and 'coreutils' are already installed on travis
brew install opam libffi depqbf # 'gmp' and 'coreutils' are already installed on travis
;;
esac

opam init -y
eval `opam config env`
opam install -y ocamlfind ounit
opam install -y ocamlfind ounit ctypes ctypes-foreign

./configure --enable-quantor --enable-tests
./configure --enable-quantor --enable-tests --enable-depqbf
make
make test

Expand Down
2 changes: 2 additions & 0 deletions .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@ addons:
packages:
- ocaml
- opam
- libffi-dev
- depqbf

script: bash -ex .travis-ci.sh
matrix:
Expand Down
5 changes: 4 additions & 1 deletion _oasis
Original file line number Diff line number Diff line change
Expand Up @@ -60,9 +60,12 @@ Library "qbf-depqbf"
BuildDepends: qbf, ctypes, ctypes.foreign
FindlibName: depqbf
FindlibParent: qbf
CCLib: -L/usr/local/lib -lqdpll
Build$: flag(depqbf)
Install$: flag(depqbf)
if system(macosx)
CCLib: -force_load /usr/local/lib/libqdpll.a
else
CCLib: -L/usr/local/lib -lqdpll

Library "qbf-random"
Path: src/random/
Expand Down
2 changes: 1 addition & 1 deletion libs/quantor-3.2/configure
Original file line number Diff line number Diff line change
Expand Up @@ -223,7 +223,7 @@ RAWCC=unknown
for cc in $CC
do
case $cc in
*gcc* | *cc*) RAWCC=$cc; break;;
*gcc* | *cc* | *clang*) RAWCC=$cc; break;;
*) ;;
esac
done
Expand Down
23 changes: 19 additions & 4 deletions myocamlbuild.ml
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(* OASIS_START *)
(* DO NOT EDIT (digest: 20db17568fe48367d23ee78777635427) *)
(* DO NOT EDIT (digest: 11a9f54dabb16e5b905c670ece0d3cb3) *)
module OASISGettext = struct
(* # 22 "src/oasis/OASISGettext.ml" *)

Expand Down Expand Up @@ -925,13 +925,28 @@ let package_default =
]);
(["oasis_library_qbf_depqbf_cclib"; "link"],
[
(OASISExpr.EBool true,
(OASISExpr.EBool true, S []);
(OASISExpr.ETest ("system", "macosx"),
S
[
A "-cclib";
A "-force_load";
A "-cclib";
A "/usr/local/lib/libqdpll.a"
]);
(OASISExpr.ENot (OASISExpr.ETest ("system", "macosx")),
S
[A "-cclib"; A "-L/usr/local/lib"; A "-cclib"; A "-lqdpll"
])
]);
(["oasis_library_qbf_depqbf_cclib"; "ocamlmklib"; "c"],
[(OASISExpr.EBool true, S [A "-L/usr/local/lib"; A "-lqdpll"])])
[
(OASISExpr.EBool true, S []);
(OASISExpr.ETest ("system", "macosx"),
S [A "-force_load"; A "/usr/local/lib/libqdpll.a"]);
(OASISExpr.ENot (OASISExpr.ETest ("system", "macosx")),
S [A "-L/usr/local/lib"; A "-lqdpll"])
])
];
includes =
[
Expand All @@ -948,6 +963,6 @@ let conf = {MyOCamlbuildFindlib.no_automatic_syntax = false}

let dispatch_default = MyOCamlbuildBase.dispatch_default conf package_default;;

# 952 "myocamlbuild.ml"
# 967 "myocamlbuild.ml"
(* OASIS_STOP *)
Ocamlbuild_plugin.dispatch dispatch_default;;
38 changes: 20 additions & 18 deletions setup.ml
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
(* setup.ml generated for the first time by OASIS v0.4.5 *)

(* OASIS_START *)
(* DO NOT EDIT (digest: 14ce46a41e04f605c23fdafce0b3eff0) *)
(* DO NOT EDIT (digest: 05029dd4d92564ba7404305910398aec) *)
(*
Regenerated by OASIS v0.4.9~HEAD
Regenerated by OASIS v0.4.10
Visit http://oasis.forge.ocamlcore.org for more information and
documentation about functions used in this file.
*)
Expand Down Expand Up @@ -6010,17 +6010,14 @@ module InternalInstallPlugin = struct

let install =

let in_destdir =
let in_destdir fn =
try
let destdir =
destdir ()
in
(* Practically speaking destdir is prepended
* at the beginning of the target filename
*)
fun fn -> destdir^fn
(* Practically speaking destdir is prepended at the beginning of the
target filename
*)
(destdir ())^fn
with PropList.Not_set _ ->
fun fn -> fn
fn
in

let install_file ~ctxt ?(prepend_destdir=true) ?tgt_fn src_file envdir =
Expand Down Expand Up @@ -6465,7 +6462,7 @@ module InternalInstallPlugin = struct
end


# 6468 "setup.ml"
# 6465 "setup.ml"
module OCamlbuildCommon = struct
(* # 22 "src/plugins/ocamlbuild/OCamlbuildCommon.ml" *)

Expand Down Expand Up @@ -6837,7 +6834,7 @@ module OCamlbuildDocPlugin = struct
end


# 6840 "setup.ml"
# 6837 "setup.ml"
module CustomPlugin = struct
(* # 22 "src/plugins/custom/CustomPlugin.ml" *)

Expand Down Expand Up @@ -6969,7 +6966,7 @@ module CustomPlugin = struct
end


# 6972 "setup.ml"
# 6969 "setup.ml"
open OASISTypes;;

let setup_t =
Expand Down Expand Up @@ -7577,7 +7574,11 @@ let setup_t =
bs_ccopt = [(OASISExpr.EBool true, [])];
bs_cclib =
[
(OASISExpr.EBool true,
(OASISExpr.EBool true, []);
(OASISExpr.ETest ("system", "macosx"),
["-force_load"; "/usr/local/lib/libqdpll.a"]);
(OASISExpr.ENot
(OASISExpr.ETest ("system", "macosx")),
["-L/usr/local/lib"; "-lqdpll"])
];
bs_dlllib = [(OASISExpr.EBool true, [])];
Expand Down Expand Up @@ -8242,16 +8243,17 @@ let setup_t =
plugin_data = []
};
oasis_fn = Some "_oasis";
oasis_version = "0.4.9~HEAD";
oasis_digest = Some "@\138*M\253b\147\182\215\148?,|t\157k";
oasis_version = "0.4.10";
oasis_digest =
Some "\001\r\206\219\027\011\185'\236s\139\r\164\225\018\241";
oasis_exec = None;
oasis_setup_args = [];
setup_update = false
};;

let setup () = BaseSetup.setup setup_t;;

# 8255 "setup.ml"
# 8257 "setup.ml"
let setup_t = BaseCompat.Compat_0_4.adapt_setup_t setup_t
open BaseCompat.Compat_0_4
(* OASIS_STOP *)
Expand Down
1 change: 1 addition & 0 deletions tests/depqbf/test_depqbf3.ml
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ let add_clause s l =
let test_depqbf3 _ =
let s = D.create () in
D.configure s "--incremental-use";
D.configure s "--dep-man=simple";
let level1 = D.new_scope s Qbf.Forall in
D.add s (mk 1);
D.add s (mk 2);
Expand Down