Skip to content

smlp pip package build and test#53

Merged
mdmitry1 merged 34 commits intomasterfrom
smlp_python311
Mar 16, 2026
Merged

smlp pip package build and test#53
mdmitry1 merged 34 commits intomasterfrom
smlp_python311

Conversation

@mdmitry1
Copy link
Collaborator

@mdmitry1 mdmitry1 commented Mar 2, 2026

1. Added SMLP package support for manylinux_2_28
2. Added SMLP package support for Ubuntu >= 22.04

@mdmitry1 mdmitry1 requested review from fbrausse and zurabksmlp March 2, 2026 17:13
Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Initial commit.
Regression passed with non-essential diffs: lines order in some JSON files does not match master.

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added virtual environment test

2. Added mathsat support
@mdmitry1 mdmitry1 marked this pull request as ready for review March 3, 2026 10:18
Copy link
Collaborator

@zurabksmlp zurabksmlp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Have verified that installation works and a couple of regression tests pass, including ne that required GUI. Approving the PR.

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Merge preparation - code will work after feature branch removal

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added OpenSuse support

Copy link
Collaborator Author

@mdmitry1 mdmitry1 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added support of multiple OS:

  1. Ubuntu 22.04
  2. OpenSuse 15.5
  3. Alma Linux 9
  4. Virtual environment - validated on Ubuntu 24.04

mdmitry1 added 2 commits March 7, 2026 20:46
commit 1912a6e1f2cabfec6ba1f1dfde0e0b5d9b3237a2 (HEAD -> master, origin/master, origin/HEAD)
Author: Franz Brauße <dev@karlchenofhell.org>
Date:   Sat Mar 7 15:15:20 2026 +0100

    fix compilation issue for macosx-sdk 26:
@fbrausse
Copy link
Collaborator

I'm running into build errors. First boost: pip-wheel.log.tail.txt
Relevant part is

2026-03-12T07:07:29,935   error: toolset gcc initialization:
2026-03-12T07:07:29,935   error: provided command '"x86_64-linux-gnu-g++"' not found
2026-03-12T07:07:29,936   error: initialized from /home/kane/user-config.jam:1

I'm building in directory /home/kane/intel/smlp-pip. Boost's b2 build process is using a user-config.jam file that has been lying in my home directory since 4 years, apparently.

For reference, the command not found comes from the old ~/user-config.jam file:

using gcc : 12.2 : x86_64-linux-gnu-g++ : <cflags>"-O2 -pipe -fPIC" <cxxflags>"-O2 -pipe -fPIC -std=c++17" <linkflags>"-Wl,-O1 -Wl,--as-needed" <archiver>"x86_64-linux-gnu-ar" <ranlib>"x86_64-linux-gnu-ranlib" ;

using python : 3.9 : /usr/local/bin/python3.9 : /usr/local/include/python3.9 ;

I'm removing this file and continue. However, ideally that file shouldn't influence the build process, so I'm documenting this error here. Can we do something about the b2 run s.t. it ignores any user-config.jam file outside of the build directory?

@fbrausse
Copy link
Collaborator

Next:

  [smlp build] Looking for libz3.so in: /home/kane/.local/lib/python3.11/site-packages/z3/lib
  [smlp build] ERROR: libz3.so not found at /home/kane/.local/lib/python3.11/site-packages/z3/lib.
  Install z3-solver with: python3.11 -m pip install --user z3-solver
  Or set Z3_PREFIX to your z3 package directory, e.g.:
    export Z3_PREFIX=~/.local/lib/python3.11/site-packages/z3
  error: subprocess-exited-with-error

Up to now SMLP did not require the z3-solver pip package to be installed and I don't have it, locally. In fact, utils/poly only needs libz3.so, which one gets by regularly installing Z3 via the distribution's package manager or manually through Z3's releases. In those cases, manually making up the pkg-config file z3.pc as setup.py is doing, is unnecessary.

If the "pip wheel" process requires z3-solver, shouldn't it be part of the dependencies in pyproject.toml? On the other hand, the documentation of the envvars, specifically Z3_PREFIX in setup.py says nothing about a pip package. Either the description in the error message or the one in setup.py should be clarified.

When running env Z3_PREFIX=/usr python3.11 -m pip wheel -v -w dist/ --check-build-dependencies --log pip-wheel.log . (since /usr is the prefix for my Z3 installation), this error occurs:

  [smlp build] Looking for libz3.so in: /usr/lib
  [smlp build] Using z3 lib dir: /usr/lib
  error: [Errno 13] Permission denied: '/usr/lib/pkgconfig/z3.pc'
  error: subprocess-exited-with-error

This z3.pc should not be written outside of the build directory.

@fbrausse
Copy link
Collaborator

After patching setup.py to account for an existing z3.pc:

diff --git a/setup.py b/setup.py
index 9d32ba5..b659a59 100644
--- a/setup.py
+++ b/setup.py
@@ -624,19 +624,22 @@ def _write_z3_pc(z3_lib: Path) -> None:
     pkgconfig_dir = z3_lib / "pkgconfig"
     pkgconfig_dir.mkdir(parents=True, exist_ok=True)
     pc_file = pkgconfig_dir / "z3.pc"
-    pc_file.write_text(
-        f"prefix={prefix}\n"
-        f"libdir={z3_lib}\n"
-        f"includedir={inc_dir}\n"
-        "\n"
-        "Name: z3\n"
-        "Description: Z3 Theorem Prover\n"
-        f"Version: {version}\n"
-        "Libs: -L${libdir} -lz3\n"
-        "Cflags: -I${includedir}\n"
-    )
-    print(f"[smlp build] Wrote pkg-config file: {pc_file}")
 
+    if os.path.exists(pc_file):
+        print(f"[smlp build] Using existing pkg-config file: {pc_file}")
+    else:
+        pc_file.write_text(
+            f"prefix={prefix}\n"
+            f"libdir={z3_lib}\n"
+            f"includedir={inc_dir}\n"
+            "\n"
+            "Name: z3\n"
+            "Description: Z3 Theorem Prover\n"
+            f"Version: {version}\n"
+            "Libs: -L${libdir} -lz3\n"
+            "Cflags: -I${includedir}\n"
+        )
+        print(f"[smlp build] Wrote pkg-config file: {pc_file}")
 
 def _z3_prefix() -> Path:
     """

Then setup.py is downloading and building GMP. I wonder whether it's possible to re-use an existing GMP installation via a mechanism similar to Z3_PREFIX.

@fbrausse
Copy link
Collaborator

fbrausse commented Mar 12, 2026

Next up:

  RuntimeError: [smlp build] meson not found. Run:  python3.11 -m pip install --user meson

However, which meson does print /usr/bin/meson for me and it works.

I did originally believe we fixed this for Konstantin's pip-wheel attempt with:

diff --git a/pyproject.toml b/pyproject.toml
index 0b6d2b1..cccd9ed 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -1,6 +1,7 @@
 [build-system]
 requires = [
     "setuptools>=68",
+    "meson",
     "wheel",
 ]
 build-backend = "setuptools.build_meta"

However, that's not enough, because _meson_bin() in setup.py relies on a pip-installed meson to discover the executable for some reason. I've thus patched this function in setup.py:

diff --git a/setup.py b/setup.py
index b659a59..a5a6852 100644
--- a/setup.py
+++ b/setup.py
@@ -160,7 +160,14 @@ def _meson_bin(build_tmp: Path) -> list[str]:
     reuses it for internal calls like `meson install`, so it must be a real
     executable file — not a -c string.
     """
+    print(f"[smlp build] Trying to locate 'meson'...")
+    meson_location = shutil.which('meson')
+    if meson_location:
+        print(f"[smlp build] Using default 'meson' at {meson_location}")
+        return [meson_location]
+
     # Find where mesonbuild is installed via pip show
+    print(f"[smlp build] Trying to locate 'meson' via pip...")
     mesonbuild_location = None
     result = subprocess.run(
         [sys.executable, "-m", "pip", "show", "meson"],

@fbrausse
Copy link
Collaborator

Next:

  [smlp build] Trying to locate 'meson'...
  [smlp build] Using default 'meson' at /tmp/pip-build-env-m3cfhz_u/overlay/bin/meson
  [smlp build] $ /tmp/pip-build-env-m3cfhz_u/overlay/bin/meson setup --wipe --native-file=/home/kane/intel/smlp-pip/build/temp.linux-x86_64-cpython-311/native.ini -Dkay-prefix=/home/kane/intel/smlp-pip/build/temp.linux-x86_64-cpython-311/kay -Dz3=enabled --prefix /home/kane/intel/smlp-pip/build/temp.linux-x86_64-cpython-311/smlp_install /home/kane/intel/smlp-pip/utils/poly /home/kane/intel/smlp-pip/utils/poly/build
  [smlp build] Using ninja from PATH: /usr/bin/ninja
  [smlp build] $ /usr/bin/ninja -C /home/kane/intel/smlp-pip/utils/poly/build install
  [smlp build] ERROR: could not find installed smlp package under /home/kane/intel/smlp-pip/build/temp.linux-x86_64-cpython-311/smlp_install. Check the Meson/Ninja output above.
  error: subprocess-exited-with-error

Well, in /home/kane/intel/smlp-pip/build/temp.linux-x86_64-cpython-311/smlp_install I have lib/python3.11/site-packages/smlp/, however, setup.py expects dist-packages, not site-packages. I realize that this change may be due to me now not using the generated meson-wrapper script anymore (which does do some weird sys.path manipulation`), but I do rather trust the default settings here.

So:

diff --git a/setup.py b/setup.py
index a5a6852..8a2e4f3 100644
--- a/setup.py
+++ b/setup.py
@@ -773,7 +773,7 @@ def _meson_build(poly_dir: Path, kay_dir: Path,
 
     # Locate the installed smlp package (Meson may use a versioned python path)
     candidates = (list(install_prefix.glob("lib/python*/dist-packages/smlp")) +
-                  list(install_prefix.glob("lib/python3/dist-packages/smlp")))
+                  list(install_prefix.glob("lib/python*/site-packages/smlp")))
     if not candidates:
         sys.exit(
             f"[smlp build] ERROR: could not find installed smlp package under "

(I removed the python3 duplicate because it's included in the * variant.)

Here, lib/python* is way too broad. I believe the setup script somewhere already computed the correct path for the current python version. We should use that method to obtain the relative path here.

However, with this final patch, I get

  Building wheel for smlp (pyproject.toml) ... done
  Created wheel for smlp: filename=smlp-0.1.0-cp311-cp311-linux_x86_64.whl size=687121 sha256=130ef0a2d30d4893bde86acd959f04940640f06f9f866ddfe7f99309a245604d

@fbrausse
Copy link
Collaborator

@mdmitry1 Do you want me to push the above changes to this branch or should I create a new one?

@fbrausse
Copy link
Collaborator

fbrausse commented Mar 12, 2026

A more minor patch for repair_wheel.py:

diff --git a/repair_wheel.py b/repair_wheel.py
old mode 100644
new mode 100755
index 1a7dc45..f38c102
--- a/repair_wheel.py
+++ b/repair_wheel.py
@@ -1,10 +1,10 @@
-#!/usr/bin/env python3.11
+#!/usr/bin/env python3
 """
 Run auditwheel repair on the smlp wheel in dist/ to produce a
 self-contained manylinux wheel with all .so dependencies bundled.
 
 Usage:
-    python3.11 repair_wheel.py [dist_dir]
+    python3 repair_wheel.py [dist_dir]
 
 dist_dir defaults to 'dist/'.
 """

Running repair_wheel.py, produces, besides the fixed .whl file the following weird Java popup for me:
image
It would be better if it didn't, but I guess it's an auditwheel-issue. I'll check their bugtracker.

Besides that, the resulting fixed .whl is called smlp-0.1.0-cp311-cp311-manylinux_2_39_x86_64.whl. I have 2 issues with this:

  1. Since this process has been using (and links) system libraries, it is not platform-independent, and certainly not manylinux_2_39 compatible. For instance, my system uses glibc-2.41, thus libraries might as well depend on those newer symbols. On the other hand, all my system libraries are compiled with -march=native, so they depend on my processor. I'm stressing system libraries here, because those are put into smlp.libs inside the wheel:
    libboost_python311-74f9353f.so.1.83.0
    libflexiblas-48670b44.so.3.5
    libflint-6d7b1291.so.16.1.4
    libgmp-80ff10d6.so.10.5.0
    libmpfr-3c9038d0.so.6.2.2
    libz3-5a43e000.so.4.15.4.0
    
    flexiblas, flint, mpfr and z3 (due to me using Z3_PREFIX) are system libraries here.
  2. The version number 0.1.0 given to this wheel does not match our current release. That should be rather easy to fix.

@fbrausse
Copy link
Collaborator

I noticed another issue: The .whl contains

        0  03-12-2026 07:53   dist/
        0  03-12-2026 07:53   dist/manylinux_2_28/
     2162  03-12-2026 07:53   dist/manylinux_2_28/repair_wheel.py
    35459  03-12-2026 07:53   dist/manylinux_2_28/setup.py
        0  03-12-2026 07:53   manylinux_2_28/
     2162  03-12-2026 07:53   manylinux_2_28/repair_wheel.py
    35459  03-12-2026 07:53   manylinux_2_28/setup.py

It shouldn't.

@fbrausse
Copy link
Collaborator

flexiblas, flint, mpfr and z3 (due to me using Z3_PREFIX) are system libraries here.

This disables flint (and hence, mpfr and BLAS dependencies), also disables static libs, no need for them:

diff --git a/setup.py b/setup.py
index 8a2e4f3..8245423 100644
--- a/setup.py
+++ b/setup.py
@@ -754,6 +754,8 @@ def _meson_build(poly_dir: Path, kay_dir: Path,
         f"--native-file={native_file}",
         f"-Dkay-prefix={kay_dir}",
         "-Dz3=enabled",
+        "-Dflint=disabled",
+        "-Dstatic=false",
         "--prefix", str(install_prefix),
         # Explicitly pass both source dir and build dir as absolute paths
         # so Meson works correctly regardless of cwd
@@ -768,7 +770,7 @@ def _meson_build(poly_dir: Path, kay_dir: Path,
         env=env,
     )
 
-    _run([_ninja_bin(), "-C", str(poly_dir / "build"), "install"],
+    _run([_ninja_bin(), "-vC", str(poly_dir / "build"), "install"],
          cwd=str(poly_dir), env=env)
 
     # Locate the installed smlp package (Meson may use a versioned python path)

@fbrausse
Copy link
Collaborator

Can't force switching branches.

diff --git a/setup.py b/setup.py
index 8245423..5f2c31d 100644
--- a/setup.py
+++ b/setup.py
@@ -812,13 +812,6 @@ class MesonBuildExt(_build_ext):
         branch = os.environ.get("SMLP_BRANCH")
         if branch:
             _run(["git", "switch", branch], cwd=str(REPO_ROOT))
-        else:
-            result = subprocess.run(
-                ["git", "branch", "-r", "--list", "origin/smlp_python311"],
-                capture_output=True, text=True, cwd=str(REPO_ROOT)
-            )
-            if result.stdout.strip():
-                _run(["git", "switch", "smlp_python311"], cwd=str(REPO_ROOT))
 
         installed_pkg = _meson_build(poly_dir, kay_dir, boost_prefix, build_tmp)
 

@mdmitry1
Copy link
Collaborator Author

According to Claude, manylinux build should be done in Docker using below image:
quay.io/pypa/manylinux_2_28_x86_64
In order to reproduced the build, please do the following (after docker installation):

git clone https://git@github.com/SMLP-Systems/smlp smlp_package_build
cd smlp_package_build
git switch smlp_python311
cd package_build/python3.11/manylinux_2_28
./run_docker_build

@fbrausse
Copy link
Collaborator

Thanks, I'm aware of the manylinux docker images. I don't see how that addresses any of the issues or questions I raised in my comments above.

Copy link
Collaborator

@fbrausse fbrausse left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please see the detailed, specific issues and questions raised in my comments above. These should be addressed. A mere reference to some Docker instructions generated by AI does not address any of these concrete requests.

@mdmitry1
Copy link
Collaborator Author

mdmitry1 commented Mar 12, 2026

I don't see any reason to apply any of above changes before this PR is merged.
This is just version 0.1.0 and not production version.

@fbrausse
Copy link
Collaborator

I don't see any reason to apply any of above changes before this PR is merged.

Could you explain to me why software development communities have mostly agreed on using the PR-review procedure? Are there benefits to it in contrast to "just push whatever to master"?

This is just version 0.1.0 and not production version.

Yeah, that's what one of my comments was about. We're not on v0.1.0 anymore, are we?

@mdmitry1
Copy link
Collaborator Author

It is not whatever - it is working prototype.
I believe in iterative test driven development.
According to my experience, it is much more productive than anything else.

@mdmitry1
Copy link
Collaborator Author

With regards to the version - 0.1.0 is not intended for external users - it is just internal milestone.

@mdmitry1
Copy link
Collaborator Author

For the release I was planning to add python3.12 and python3.13 support, so SMLP package will be possible to use by people, who don't have python3.11.
I have already tested both in virtual environment and 4 operating systems.

@fbrausse
Copy link
Collaborator

fbrausse commented Mar 12, 2026

It is not whatever - it is working prototype.

I strongly suggest you put that information into the title or description of the PR. This is the first time I read about this being a prototype. You praised it as extensively tested. If it indeed is a prototype, we should not advertise wheels just yet. In fact, could you please upload one of those wheels you built somewhere so we can take a look and check whether they correspond to what we're building? After all, those wheels would be put out to users. We should be sure about that. Please also consider my comment on the superfluous files.

With regards to the version - 0.1.0 is not intended for external users - it is just internal milestone.

I don't understand. Please clarify how the externally visible package version 0.1.0 for the wheel containing the SMLP software is an "internal milestone", and what the latter actually means in comparison to the actual version of the SMLP software, which, as of this writing is 1.0.1.

I have already tested both in virtual environment and 4 operating systems.

Let me please note that running things inside 4 Docker containers executed on Linux (likely even using the same kernel version) differs from running things on 4 operating systems. In particular, it differs from the environment users¹ might use, which could potentially include a ~/user-config.jam. That's why testing on different configurations (not containers) is important. I suppose, testing also involves feedback. See comments above.

¹ Users here refers to both, pure wheel users, as well as those cloning the repo and doing things with it.

Edit: I've now noticed the two pre-built wheels in dist/. I don't think they should be part of the source distribution. Please remove dist/ in this PR.

Copy link
Collaborator

@fbrausse fbrausse left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've run the regression tests using the pip-installed wheel dist/smlp-0.1.0-cp311-cp311-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl this PR put in dist/. I get differences between master and this PR for the following test numbers: 63, 69, 79, 81, 85, 101, 103, 110, 113.

@fbrausse
Copy link
Collaborator

Copy link
Collaborator

@fbrausse fbrausse left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Never mind, re-running the test script didn't reproduce the differences observed yesterday evening. We need to make the tests more reliable. I'll approve this PR but will open issues regarding the identified problems as discussed earlier.

@mdmitry1 mdmitry1 merged commit 46deb09 into master Mar 16, 2026
@mdmitry1 mdmitry1 deleted the smlp_python311 branch March 16, 2026 08:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants