{tools}[GCCcore/11.3.0] Z3 v4.10.2, Z3 v4.8.16, Z3 v4.8.12, ... w/ Python 3.10.4 + 3.9.6 + 3.9.5 + 3.8.6

easybuild/easyconfigs/z/Z3/Z3-4.10.2-GCCcore-11.3.0-Python-3.10.4.eb

@@ -0,0 +1,54 @@
+easyblock = 'PythonBundle'
+
+name = 'Z3'
+version = '4.10.2'
+versionsuffix = '-Python-%(pyver)s'
+_z3_solver_version = '%s.0' % version
+
+homepage = 'https://github.com/Z3Prover/z3'
+description = """Z3 is a theorem prover from Microsoft Research with support for bitvectors,
+booleans, arrays, floating point numbers, strings, and other data types. This
+module includes z3_solver, the Python interface of Z3.
+"""
+
+toolchain = {'name': 'GCCcore', 'version': '11.3.0'}
+toolchainopts = {'pic': True}
+
+builddependencies = [
+    ('binutils', '2.38'),
+    ('CMake', '3.23.1'),
+]
+
+dependencies = [
+    ('Python', '3.10.4'),
+    ('GMP', '6.2.1'),
+]
+
+use_pip = True
+
+_fix_parallelism = """sed -i 's/str(multiprocessing.cpu_count())/"%(parallel)s"/' setup.py &&"""
+_enable_gmp = """sed -i "s/Z3_USE_LIB_GMP.*/Z3_USE_LIB_GMP' : True,/" setup.py &&"""
+
+exts_list = [
+    ('z3-solver', _z3_solver_version, {
+        'modulename': 'z3',
+        'checksums': ['a861081c8f5710996f3f545f12c1137ab38ba4b5b02f0f15d59ba52f6f81d237'],
+        'preinstallopts': _fix_parallelism + _enable_gmp,
+    }),
+]
+
+# make Z3 headers and libraries accessible in their usual location
+_z3_site_path = "lib/python%(pyshortver)s/site-packages/%(namelower)s"
+postinstallcmds = [
+    "cd %%(installdir)s && ln -s %s/include include" % _z3_site_path,
+    "cd %%(installdir)s/lib && ln -s ../%s/lib/libz3.so libz3.so" % _z3_site_path,
+]
+
+sanity_pip_check = True
+
+sanity_check_paths = {
+    'files': ['bin/z3', 'include/z3_api.h', 'lib/libz3.%s' % SHLIB_EXT],
+    'dirs': ['include', 'lib/python%(pyshortver)s/site-packages'],
+}
+
+moduleclass = 'tools'

easybuild/easyconfigs/z/Z3/Z3-4.8.10-GCCcore-10.2.0-Python-3.8.6.eb

@@ -0,0 +1,53 @@
+easyblock = 'PythonBundle'
+
+name = 'Z3'
+version = '4.8.10'
+versionsuffix = '-Python-%(pyver)s'
+_z3_solver_version = '%s.0' % version
+
+homepage = 'https://github.com/Z3Prover/z3'
+description = """Z3 is a theorem prover from Microsoft Research with support for bitvectors,
+booleans, arrays, floating point numbers, strings, and other data types. This
+module includes z3_solver, the Python interface of Z3.
+"""
+
+toolchain = {'name': 'GCCcore', 'version': '10.2.0'}
+toolchainopts = {'pic': True}
+
+builddependencies = [
+    ('binutils', '2.35'),
+]
+
+dependencies = [
+    ('Python', '3.8.6'),
+    ('GMP', '6.2.0'),
+]
+
+use_pip = True
+
+_fix_parallelism = """sed -i 's/str(multiprocessing.cpu_count())/"%(parallel)s"/' setup.py &&"""
+_enable_gmp = "sed -i 's/^GMP=.*/GMP=True/' core/scripts/mk_util.py &&"
+
+exts_list = [
+    ('z3-solver', _z3_solver_version, {
+        'modulename': 'z3',
+        'checksums': ['cd022a66524685bdd8b265027bd22f24c35f8db29a4287d005e0005757ffdc21'],
+        'preinstallopts': _fix_parallelism + _enable_gmp,
+    }),
+]
+
+# make Z3 headers and libraries accessible in their usual location
+_z3_site_path = "lib/python%(pyshortver)s/site-packages/%(namelower)s"
+postinstallcmds = [
+    "cd %%(installdir)s && ln -s %s/include include" % _z3_site_path,
+    "cd %%(installdir)s/lib && ln -s ../%s/lib/libz3.so libz3.so" % _z3_site_path,
+]
+
+sanity_pip_check = True
+
+sanity_check_paths = {
+    'files': ['bin/z3', 'include/z3_api.h', 'lib/libz3.%s' % SHLIB_EXT],
+    'dirs': ['include', 'lib/python%(pyshortver)s/site-packages'],
+}
+
+moduleclass = 'tools'

easybuild/easyconfigs/z/Z3/Z3-4.8.11-GCCcore-10.3.0-Python-3.9.5.eb

@@ -0,0 +1,54 @@
+easyblock = 'PythonBundle'
+
+name = 'Z3'
+version = '4.8.11'
+versionsuffix = '-Python-%(pyver)s'
+_z3_solver_version = '%s.0' % version
+
+homepage = 'https://github.com/Z3Prover/z3'
+description = """Z3 is a theorem prover from Microsoft Research with support for bitvectors,
+booleans, arrays, floating point numbers, strings, and other data types. This
+module includes z3_solver, the Python interface of Z3.
+"""
+
+toolchain = {'name': 'GCCcore', 'version': '10.3.0'}
+toolchainopts = {'pic': True}
+
+builddependencies = [
+    ('binutils', '2.36.1'),
+    ('CMake', '3.20.1'),
+]
+
+dependencies = [
+    ('Python', '3.9.5'),
+    ('GMP', '6.2.1'),
+]
+
+use_pip = True
+
+_fix_parallelism = """sed -i 's/str(multiprocessing.cpu_count())/"%(parallel)s"/' setup.py &&"""
+_enable_gmp = """sed -i "s/Z3_USE_LIB_GMP.*/Z3_USE_LIB_GMP' : True,/" setup.py &&"""
+
+exts_list = [
+    ('z3-solver', _z3_solver_version, {
+        'modulename': 'z3',
+        'checksums': ['3621f464baf48aabbf74bcb85cd97ef46e928af3ca3a28e27d6816601e3b7290'],
+        'preinstallopts': _fix_parallelism + _enable_gmp,
+    }),
+]
+
+# make Z3 headers and libraries accessible in their usual location
+_z3_site_path = "lib/python%(pyshortver)s/site-packages/%(namelower)s"
+postinstallcmds = [
+    "cd %%(installdir)s && ln -s %s/include include" % _z3_site_path,
+    "cd %%(installdir)s/lib && ln -s ../%s/lib/libz3.so libz3.so" % _z3_site_path,
+]
+
+sanity_pip_check = True
+
+sanity_check_paths = {
+    'files': ['bin/z3', 'include/z3_api.h', 'lib/libz3.%s' % SHLIB_EXT],
+    'dirs': ['include', 'lib/python%(pyshortver)s/site-packages'],
+}
+
+moduleclass = 'tools'

easybuild/easyconfigs/z/Z3/Z3-4.8.12-GCCcore-11.2.0-Python-3.9.6.eb

@@ -0,0 +1,54 @@
+easyblock = 'PythonBundle'
+
+name = 'Z3'
+version = '4.8.12'
+versionsuffix = '-Python-%(pyver)s'
+_z3_solver_version = '%s.0' % version
+
+homepage = 'https://github.com/Z3Prover/z3'
+description = """Z3 is a theorem prover from Microsoft Research with support for bitvectors,
+booleans, arrays, floating point numbers, strings, and other data types. This
+module includes z3_solver, the Python interface of Z3.
+"""
+
+toolchain = {'name': 'GCCcore', 'version': '11.2.0'}
+toolchainopts = {'pic': True}
+
+builddependencies = [
+    ('binutils', '2.37'),
+    ('CMake', '3.21.1'),
+]
+
+dependencies = [
+    ('Python', '3.9.6'),
+    ('GMP', '6.2.1'),
+]
+
+use_pip = True
+
+_fix_parallelism = """sed -i 's/str(multiprocessing.cpu_count())/"%(parallel)s"/' setup.py &&"""
+_enable_gmp = """sed -i "s/Z3_USE_LIB_GMP.*/Z3_USE_LIB_GMP' : True,/" setup.py &&"""
+
+exts_list = [
+    ('z3-solver', _z3_solver_version, {
+        'modulename': 'z3',
+        'checksums': ['48f66e52d5b267e6df6fab9fccdefdf7e09a846d9e309bc2dccff983c27da612'],
+        'preinstallopts': _fix_parallelism + _enable_gmp,
+    }),
+]
+
+# make Z3 headers and libraries accessible in their usual location
+_z3_site_path = "lib/python%(pyshortver)s/site-packages/%(namelower)s"
+postinstallcmds = [
+    "cd %%(installdir)s && ln -s %s/include include" % _z3_site_path,
+    "cd %%(installdir)s/lib && ln -s ../%s/lib/libz3.so libz3.so" % _z3_site_path,
+]
+
+sanity_pip_check = True
+
+sanity_check_paths = {
+    'files': ['bin/z3', 'include/z3_api.h', 'lib/libz3.%s' % SHLIB_EXT],
+    'dirs': ['include', 'lib/python%(pyshortver)s/site-packages'],
+}
+
+moduleclass = 'tools'

easybuild/easyconfigs/z/Z3/Z3-4.8.16-GCCcore-11.3.0-Python-3.10.4.eb

@@ -0,0 +1,54 @@
+easyblock = 'PythonBundle'
+
+name = 'Z3'
+version = '4.8.16'
+versionsuffix = '-Python-%(pyver)s'
+_z3_solver_version = '%s.0' % version
+
+homepage = 'https://github.com/Z3Prover/z3'
+description = """Z3 is a theorem prover from Microsoft Research with support for bitvectors,
+booleans, arrays, floating point numbers, strings, and other data types. This
+module includes z3_solver, the Python interface of Z3.
+"""
+
+toolchain = {'name': 'GCCcore', 'version': '11.3.0'}
+toolchainopts = {'pic': True}
+
+builddependencies = [
+    ('binutils', '2.38'),
+    ('CMake', '3.23.1'),
+]
+
+dependencies = [
+    ('Python', '3.10.4'),
+    ('GMP', '6.2.1'),
+]
+
+use_pip = True
+
+_fix_parallelism = """sed -i 's/str(multiprocessing.cpu_count())/"%(parallel)s"/' setup.py &&"""
+_enable_gmp = """sed -i "s/Z3_USE_LIB_GMP.*/Z3_USE_LIB_GMP' : True,/" setup.py &&"""
+
+exts_list = [
+    ('z3-solver', _z3_solver_version, {
+        'modulename': 'z3',
+        'checksums': ['a84ade2852d4c3ca2ae32a3ddc554b8f3da6d5d69efd474b5627ab6db509e787'],
+        'preinstallopts': _fix_parallelism + _enable_gmp,
+    }),
+]
+
+# make Z3 headers and libraries accessible in their usual location
+_z3_site_path = "lib/python%(pyshortver)s/site-packages/%(namelower)s"
+postinstallcmds = [
+    "cd %%(installdir)s && ln -s %s/include include" % _z3_site_path,
+    "cd %%(installdir)s/lib && ln -s ../%s/lib/libz3.so libz3.so" % _z3_site_path,
+]
+
+sanity_pip_check = True
+
+sanity_check_paths = {
+    'files': ['bin/z3', 'include/z3_api.h', 'lib/libz3.%s' % SHLIB_EXT],
+    'dirs': ['include', 'lib/python%(pyshortver)s/site-packages'],
+}
+
+moduleclass = 'tools'

test/easyconfigs/easyconfigs.py

@@ -1054,33 +1054,36 @@ def test_pr_python_packages(self):
                         if exts_default_options.get(key) is None:
                             failing_checks.append("'%s' should be set in exts_default_options in %s" % (key, ec_fn))
 
-            # if Python is a dependency, that should be reflected in the versionsuffix
+            # if Python is a dependency, that should be reflected in the versionsuffix since v3.8.6
+            has_recent_python3_dep = any(LooseVersion(dep['version']) >= LooseVersion('3.8.6')
+                                         for dep in ec['dependencies'] if dep['name'] == 'Python')
+            has_old_python_dep = any(LooseVersion(dep['version']) < LooseVersion('3.8.6')
+                                     for dep in ec['dependencies'] if dep['name'] == 'Python')
             # Tkinter is an exception, since its version always matches the Python version anyway
-            # Python 3.8.6 and later are also excluded, as we consider python 3 the default python
-            # Also whitelist some updated versions of Amber
+            # Z3 is an exception, since it has easyconfigs with and without Python bindings
+            exception_python_suffix = ['Tkinter', 'Z3']
+            # Also whitelist some specific easyconfigs from this check
+            # TODO: clean whitelist in EB 5.0
             whitelist_python_suffix = [
                 'Amber-16-*-2018b-AmberTools-17-patchlevel-10-15.eb',
                 'Amber-16-intel-2017b-AmberTools-17-patchlevel-8-12.eb',
                 'R-keras-2.1.6-foss-2018a-R-3.4.4.eb',
             ]
             whitelisted = any(re.match(regex, ec_fn) for regex in whitelist_python_suffix)
-            has_python_dep = any(LooseVersion(dep['version']) < LooseVersion('3.8.6')
-                                 for dep in ec['dependencies'] if dep['name'] == 'Python')
-            if has_python_dep and ec.name != 'Tkinter' and not whitelisted:
-                if not re.search(r'-Python-[23]\.[0-9]+\.[0-9]+', ec['versionsuffix']):
-                    msg = "'-Python-%%(pyver)s' should be included in versionsuffix in %s" % ec_fn
-                    # This is only a failure for newly added ECs, not for existing ECS
-                    # As that would probably break many ECs
-                    if ec_fn in self.added_ecs_filenames:
-                        failing_checks.append(msg)
-                    else:
-                        print('\nNote: Failed non-critical check: ' + msg)
-            else:
-                has_recent_python3_dep = any(LooseVersion(dep['version']) >= LooseVersion('3.8.6')
-                                             for dep in ec['dependencies'] if dep['name'] == 'Python')
-                if has_recent_python3_dep and re.search(r'-Python-3\.[0-9]+\.[0-9]+', ec['versionsuffix']):
-                    msg = "'-Python-%%(pyver)s' should no longer be included in versionsuffix in %s" % ec_fn
+
+            if ec.name in exception_python_suffix or whitelisted:
+                continue
+            elif has_old_python_dep and not re.search(r'-Python-[23]\.[0-9]+\.[0-9]+', ec['versionsuffix']):
+                msg = "'-Python-%%(pyver)s' should be included in versionsuffix in %s" % ec_fn
+                # This is only a failure for newly added ECs, not for existing ECS
+                # As that would probably break many ECs
+                if ec_fn in self.added_ecs_filenames:
                     failing_checks.append(msg)
+                else:
+                    print('\nNote: Failed non-critical check: ' + msg)
+            elif has_recent_python3_dep and re.search(r'-Python-3\.[0-9]+\.[0-9]+', ec['versionsuffix']):
+                msg = "'-Python-%%(pyver)s' should no longer be included in versionsuffix in %s" % ec_fn
+                failing_checks.append(msg)
 
             # require that running of "pip check" during sanity check is enabled via sanity_pip_check
             if easyblock in ['PythonBundle', 'PythonPackage']: