Merge pull request pysmt#431 from pysmt/installer_version_checker

Installers: Simpler version check via subprocess

pysmt/cmd/check_version.py

@@ -0,0 +1,79 @@
+# Copyright 2014 Andrea Micheli and Marco Gario
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+import sys
+import re
+
+
+def check_version(module):
+    try:
+        if module == "z3":
+            import z3
+            (major, minor, ver, _) = z3.get_version()
+            version = "%d.%d.%d" % (major, minor, ver)
+
+        elif module == "msat":
+            import mathsat
+            version_str = mathsat.msat_get_version()
+            m = re.match(r"^MathSAT5 version (\d+\.\d+\.\d+) .*$", version_str)
+            if m is not None:
+                version = m.group(1)
+
+        elif module == "cudd":
+            import repycudd
+            doc = repycudd.DOCSTRING
+            m = re.match(r"^PyCUDD (\d+\.\d+\.\d+).*", doc)
+            if m is not None:
+                version = m.group(1)
+
+        elif module == "btor":
+            import boolector
+            version = "OK" # Just checking if import succeeds
+
+        elif module == "cvc4":
+            import CVC4
+            version = CVC4.Configuration_getVersionString()
+
+        elif module == "picosat":
+            import picosat
+            version = picosat.picosat_version()
+
+        elif module == "yices":
+            import yicespy
+            v = yicespy.__dict__['__YICES_VERSION']
+            m = yicespy.__dict__['__YICES_VERSION_MAJOR']
+            p = yicespy.__dict__['__YICES_VERSION_PATCHLEVEL']
+            version = "%d.%d.%d" % (v, m, p)
+        else:
+            print("Invalid argument '%s'"  % module)
+            exit(-2)
+
+    except ImportError:
+        version = None
+
+    return version
+
+
+if __name__ == "__main__":
+    if len(sys.argv) != 2:
+        print("Usage: python %s <solver_name>" % sys.argv[0])
+        exit(-1)
+
+    module = sys.argv[1]
+    version = check_version(module)
+
+    if version is None:
+        print("NOT INSTALLED")
+    else:
+        print(version)

pysmt/cmd/installers/base.py

@@ -19,13 +19,15 @@
 import tarfile
 import six
 import struct
+import subprocess
 
 from contextlib import contextmanager
 
 import six.moves
 from six.moves import xrange
 from six.moves.urllib.error import HTTPError, URLError
 
+
 @contextmanager
 def TemporaryPath(path):
     """Context that substitutes the system path to test for API presence or absence"""
@@ -92,7 +94,6 @@ def download_links(self):
         if self.native_link is not None:
             yield self.native_link.format(archive_name=self.archive_name)
 
-
     def download(self):
         """Downloads the archive from one of the mirrors"""
         if not os.path.exists(self.archive_path):
@@ -121,7 +122,6 @@ def unpack(self):
         else:
             raise ValueError("Unsupported archive for extraction: %s" % path)
 
-
     def compile(self):
         """Performs the compilation if needed"""
         pass
@@ -142,21 +142,18 @@ def install(self, force_redo=False):
         self.unpack()
         self.compile()
         self.move()
-
         return
 
     def is_installed(self):
         """Checks if the solver is installed and usable"""
         ver = self.get_installed_version()
         return (ver is not None) and (ver == self.solver_version)
 
-
     def get_installed_version(self):
         """Returns a string representing the version of the solver currently
         installed or None if the solver is not found"""
         return None
 
-
     @staticmethod
     def do_download(url, file_name):
         """Downloads the given url into the given file name"""
@@ -188,32 +185,32 @@ def do_download(url, file_name):
         f.close()
         return True
 
-
     @staticmethod
-    def run_python(script, directory=None, env_variables=None):
+    def run_python(script, directory=None, env_variables=None, get_output=False):
         """Executes a python script"""
         interpreter = 'python'
         if sys.executable:
             interpreter = sys.executable
 
         cmd = '{interpreter} {script}'.format(interpreter=interpreter,
                                               script=script)
-        SolverInstaller.run(cmd, directory=directory, env_variables = env_variables)
+        return SolverInstaller.run(cmd, directory=directory,
+                                   env_variables=env_variables,
+                                   get_output=get_output)
 
     @staticmethod
-    def run(program, directory=None, env_variables=None):
+    def run(program, directory=None, env_variables=None, get_output=False):
         """Executes an arbitrary program"""
-        if directory is not None:
-            cmd = 'cd {directory}; {program}'
-        else:
-            cmd = '{program}'
-
+        environment = os.environ.copy()
         if env_variables is not None:
             for k,v in six.iteritems(env_variables):
-                cmd = "export %s='%s'; %s" % (k, v, cmd)
+                environment[k] = v
 
-        os.system(cmd.format(directory=directory,
-                             program=program))
+        if get_output:
+            output = subprocess.check_output(program.split(), env=environment, cwd=directory)
+            return output.decode("ascii")
+        else:
+            subprocess.check_call(program.split(), env=environment, cwd=directory)
 
     @staticmethod
     def clean_dir(path):
@@ -243,7 +240,6 @@ def mv(source, dest):
             shutil.copy(source, dest)
             os.unlink(source)
 
-
     @staticmethod
     def untar(fname, directory, mode='r:gz'):
         """Extracts the tarfile using the specified mode in the given directory."""
@@ -256,3 +252,28 @@ def unzip(fname, directory):
         myzip = zipfile.ZipFile(fname, "r")
         myzip.extractall(directory)
         myzip.close()
+
+    def get_installed_version_script(self, bindings_dir, package):
+        check_version_script = os.path.abspath(os.path.join(
+                                 os.path.dirname(__file__),
+                                 "..",
+                                 "check_version.py"))
+        env = {}
+        for k in ["LD_LIBRARY_PATH", "PATH", "PYTHONPATH"]:
+            if k in os.environ:
+                env[k] = bindings_dir + os.pathsep + os.environ[k]
+            else:
+                env[k] = bindings_dir
+
+        try:
+            output = self.run_python("%s %s" % (check_version_script, package),
+                                     env_variables=env,
+                                     get_output=True)
+            output = output.strip()
+        except Exception as ex:
+            print("Error while checking %s" % package)
+            return None
+
+        if output == "NOT INSTALLED":
+            return None
+        return output

pysmt/cmd/installers/bdd.py

@@ -68,17 +68,4 @@ def move(self):
 
 
     def get_installed_version(self):
-        with TemporaryPath([self.bindings_dir]):
-            version = None
-            try:
-                import repycudd
-                doc = repycudd.DOCSTRING
-                m = re.match(r"^PyCUDD (\d+\.\d+\.\d+).*", doc)
-                if m is not None:
-                    version = m.group(1)
-            finally:
-                if "repycudd" in sys.modules:
-                    del sys.modules["repycudd"]
-                # Return None, without raising an exception
-                # pylint: disable=lost-exception
-                return version
+        return self.get_installed_version_script(self.bindings_dir, "cudd")

pysmt/cmd/installers/btor.py

@@ -34,18 +34,29 @@ def __init__(self, install_dir, bindings_dir, solver_version,
                                  mirror_link=mirror_link)
 
     def compile(self):
-        # Extract sub-archives
-        SolverInstaller.run("tar xf archives/lingeling*.tar.gz", directory=self.extract_path)
-        SolverInstaller.run("mv lingeling* lingeling", directory=self.extract_path)
-        SolverInstaller.run("tar xf archives/boolector*.tar.gz", directory=self.extract_path)
-        SolverInstaller.run("mv boolector* boolector", directory=self.extract_path)
-
-        # Reconfigure and build python bindings
+        import glob
+        # Build lingeling
+        lingeling_archive = glob.glob(os.path.join(self.extract_path,
+                                                   "archives", "lingeling-*.tar.gz"))[0]
+        SolverInstaller.untar(lingeling_archive, self.extract_path)
+        lingeling_dir = glob.glob(os.path.join(self.extract_path,
+                                               "lingeling*"))[0]
+        SolverInstaller.mv(lingeling_dir,
+                           os.path.join(self.extract_path, "lingeling"))
         SolverInstaller.run("bash ./configure.sh -fPIC",
                           directory=os.path.join(self.extract_path, "lingeling"))
         SolverInstaller.run("make",
                           directory=os.path.join(self.extract_path, "lingeling"))
 
+        # Build Btor
+        boolector_archive = glob.glob(os.path.join(self.extract_path,
+                                                   "archives", "boolector-*.tar.gz"))[0]
+        SolverInstaller.untar(boolector_archive, self.extract_path)
+        boolector_dir = glob.glob(os.path.join(self.extract_path,
+                                               "boolector*"))[0]
+        SolverInstaller.mv(boolector_dir,
+                           os.path.join(self.extract_path, "boolector"))
+
         SolverInstaller.run("bash ./configure.sh -python",
                           directory=os.path.join(self.extract_path, "boolector"))
         SolverInstaller.run("make",
@@ -63,19 +74,13 @@ def move(self):
                 SolverInstaller.mv(os.path.join(bdir, f), self.bindings_dir)
 
     def get_installed_version(self):
-        with TemporaryPath([self.bindings_dir]):
-            version = None
+        res = self.get_installed_version_script(self.bindings_dir, "btor")
+        version = None
+        if res == "OK":
             vfile = os.path.join(self.extract_path, "boolector", "VERSION")
             try:
-                # The version is read from a file, but we first check
-                # if the module is installed
-                # pylint: disable=unused-import
-                import boolector
                 with open(vfile) as f:
                     version = f.read().strip()
-            finally:
-                if "boolector" in sys.modules:
-                    del sys.modules["boolector"]
-                # Return None, without raising an exception
-                # pylint: disable=lost-exception
-                return version
+            except OSError:
+                return None
+        return version

pysmt/cmd/installers/cvc4.py

@@ -51,32 +51,28 @@ def compile(self):
                             directory=os.path.join(self.extract_path, "contrib"))
 
         # Configure and build CVC4
-        config = "./configure --prefix={bin_path} \
-                              --enable-language-bindings=python \
-                              --with-antlr-dir={dir_path}/antlr-3.4 ANTLR={dir_path}/antlr-3.4/bin/antlr3;\
-                  make; \
-                  make install ".format(bin_path=self.bin_path, dir_path=self.extract_path)
+        config_cmd = "./configure --prefix={bin_path} \
+                                  --enable-language-bindings=python \
+                                  --with-antlr-dir={dir_path}/antlr-3.4 ANTLR={dir_path}/antlr-3.4/bin/antlr3"
+        config_cmd = config_cmd.format(bin_path=self.bin_path,
+                                       dir_path=self.extract_path)
+
         if os.path.exists(sys.executable+"-config"):
             pyconfig = {"PYTHON_CONFIG": sys.executable+"-config"}
         else:
             pyconfig = {}
-        SolverInstaller.run(config,
-                            directory=self.extract_path,
+
+        SolverInstaller.run(config_cmd,  directory=self.extract_path,
+                            env_variables=pyconfig)
+        SolverInstaller.run("make", directory=self.extract_path,
                             env_variables=pyconfig)
+        SolverInstaller.run("make install", directory=self.extract_path,
+                            env_variables=pyconfig)
+
 
         # Fix the paths of the bindings
         SolverInstaller.mv(os.path.join(self.bin_path, "lib/pyshared/CVC4.so.4.0.0"),
                            os.path.join(self.bin_path, "lib/pyshared/_CVC4.so"))
 
     def get_installed_version(self):
-        with TemporaryPath([self.bindings_dir]):
-            version = None
-            try:
-                import CVC4
-                version = CVC4.Configuration_getVersionString()
-            finally:
-                if "CVC4" in sys.modules:
-                    del sys.modules["CVC4"]
-                # Return None, without raising an exception
-                # pylint: disable=lost-exception
-                return version
+        return self.get_installed_version_script(self.bindings_dir, "cvc4")

pysmt/cmd/installers/msat.py

@@ -61,17 +61,4 @@ def move(self):
         SolverInstaller.mv(os.path.join(pdir, "mathsat.py"), self.bindings_dir)
 
     def get_installed_version(self):
-        with TemporaryPath([self.bindings_dir]):
-            version = None
-            try:
-                import mathsat
-                version_str = mathsat.msat_get_version()
-                m = re.match(r"^MathSAT5 version (\d+\.\d+\.\d+) .*$", version_str)
-                if m is not None:
-                    version = m.group(1)
-            finally:
-                if "mathsat" in sys.modules:
-                    del sys.modules["mathsat"]
-                # Return None, without raising an exception
-                # pylint: disable=lost-exception
-                return version
+        return self.get_installed_version_script(self.bindings_dir, "msat")

pysmt/cmd/installers/pico.py

@@ -52,7 +52,7 @@ def download(self):
 
     def compile(self):
         picosat_dir = os.path.join(self.extract_path, "picosat-%s" % self.solver_version)
-        SolverInstaller.run('bash configure', directory=picosat_dir,
+        SolverInstaller.run('bash configure.sh', directory=picosat_dir,
                             env_variables={"CFLAGS": " -fPIC"})
         SolverInstaller.run('make', directory=picosat_dir,
                             env_variables={"CFLAGS": " -fPIC"})
@@ -70,14 +70,4 @@ def move(self):
         SolverInstaller.mv(os.path.join(self.extract_path, "picosat.py"), self.bindings_dir)
 
     def get_installed_version(self):
-        with TemporaryPath([self.bindings_dir]):
-            version = None
-            try:
-                import picosat
-                version = picosat.picosat_version()
-            finally:
-                if "picosat" in sys.modules:
-                    del sys.modules["picosat"]
-                # Return None, without raising an exception
-                # pylint: disable=lost-exception
-                return version
+        return self.get_installed_version_script(self.bindings_dir, "picosat")