Permalink
Browse files

Update README to add bad workaround for Yices with static GMP on 64-b…

…it Linux
  • Loading branch information...
polazarus committed Nov 28, 2013
1 parent 76a172f commit 1c05e90b15b4f71183641fd2047b9b6b1c33941b
Showing with 12 additions and 7 deletions.
  1. +12 −7 README.markdown
View
@@ -8,7 +8,9 @@ OCamlyices
[Yices][yices] is an efficient SMT solver developed at SRI International.
OCamlyices lets you use this SMT solver inside your own [OCaml][ocaml] program.
Based on [CamlIDL][camlidl], this library allows accessing both Yices APIs (full and light), with most (if not all) features: unsatisfiable cores, bit vectors, and more experimental features (interrupting, switching between APIs).
Based on [CamlIDL][camlidl], this library allows accessing both Yices APIs (full and light),
with most (if not all) features: unsatisfiable cores, bit vectors, and more experimental
features (interrupting, switching between APIs).
**Warning!** Only tested under Linux (32 and 64 bit platforms), but reported to
work under MacOS X…
@@ -20,7 +22,7 @@ First requirement: Yices
[Yices][yices] 1.0.34 or more recent (but not 2) needs to be *installed* on your system.
It can be done in two steps:
1. First download the latest tarball of [Yices 1 from SRI website][yices-dl],
1. First download the latest tarball of [Yices 1 from SRI website][yices-dl].
Prefer the version with GMP statically linked, except on Linux x86_64 (see note below).
2. Install Yices on your system as follow:
@@ -35,10 +37,12 @@ It can be done in two steps:
wget -q -O- http://git.io/sWxMmg | sh -s <yices-XYZ.tar.gz> /opt /opt/lib64
**N.B.:** On Linux x86_64 (and possibly other 64 bit platform), only “Yices with
GMP dynamically linked” is supported at the moment. Indeed, `libyices.a`
**N.B.:** On Linux x86_64 (and possibly other 64-bit platform), “Yices with
GMP dynamically linked” is strongly prefered at the moment. Indeed, `libyices.a`
(provided in “Yices with GMP statically linked”) is not compiled with the
`-fPIC` flag and cannot be compiled with OCamlyices.
`-fPIC` flag and cannot be compiled in a shared library (used for bytecode
compilation). A possible but *inadvisable* workaround is to use the custom
compilation mode (see configure options).
Easy install (with Opam)
@@ -124,8 +128,9 @@ Manual install
Build the OCamlyices for custom bytecode compilation (see ocamlc manual for
more information), rather than using a shared library. As a result, every
program using such a version of OCamlyices will be compiled with the
option `-custom`.
program using such a version of OCamlyices will have to be compiled with the
option `-custom`. Also, in this mode, OCamlyices cannot be used from within
the standard interactive toplevel.
--enable-partial-linking [DEFAULT]
--disbable-partial-linking

0 comments on commit 1c05e90

Please sign in to comment.