Refactoring after PR#53 code review

[mdmitry1]

Regression passed in all five configurations, all Docker images are uploaded

[mdmitry1]

Regression passed after the first refactoring round.

Main fixes:

1. Write access to system directory is removed
2. <repo>/dist directory is removed
3. <repo>/manylinux_2_28 directory is removed
4. Optional git switch is removed
5. Z3_PREFIX is set automatically - tested on Ubuntu 24.04

Validation:

1. pip install <repo> use case - validated on Ubuntu 24.04
2. Manylinux wheel build use case - validated on Ubuntu 22.04

[mdmitry1]

Finished second round of refactoring

1. Fixed build issue in the case of user_config.jam file present in home directory
2. Added meson and ninja to build-system.requires
3. Removed redundant meson and ninja search code
4. For Debian only: started using precompiled gmp libraries
   For manylinux build got compilation error in SMLP C++ code

Validation

DORA test passed in Ubuntu 24.04 python virtual environment with manylinux wheel.

[fbrausse]

4. For manylinux build got compilation error in SMLP C++ code

Could you post the log containing the error? I'll take a look what might have gone wrong. Also the version number of GMP they install might be helpful, if you know it.

[mdmitry1]

1) ../src/reals.hh: In function ‘kay::Z smlp::reals::eager::ubound_log2(const R&)’:
../src/reals.hh:62:39: error: invalid initialization of reference of type ‘const kay::Z&’ {aka ‘const mpz_class&’} from expression of type ‘__gmp_expr<__mpq_struct [1], __gmp_unary_expr<__gmp_expr<__mpq_struct [1], __gmp_unary_expr<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, __gmp_abs_function> >, __gmp_ceil_function> >’

2. gmp version is 6.3.0

[fbrausse]

1. ../src/reals.hh: In function ‘kay::Z smlp::reals::eager::ubound_log2(const R&)’: ../src/reals.hh:62:39: error: invalid initialization of reference of type ‘const kay::Z&’ {aka ‘const mpz_class&’} from expression of type ‘__gmp_expr<__mpq_struct [1], __gmp_unary_expr<__gmp_expr<__mpq_struct [1], __gmp_unary_expr<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, __gmp_abs_function> >, __gmp_ceil_function> >’

2. gmp version is 6.3.0

I can't reproduce this locally, neither with gcc-{13,14,15} nor with clang++-{20,21}. I also don't understand why the ceil function would return an mpq_class, it (kay's, that is) should return an mpz_class object. It could be an include path issue (since kay's ceil doesn't seem to be used) or sth. else. While I can't run manylinux here, yet, the full compile log (including the compiler commands run) might help.

[fbrausse]

Thanks, Dmitry. For now I have a few comments, will test it tomorrow.

[mdmitry1]

Updates according to release plan

[mdmitry1]

Implemented requested changes after review

[mdmitry1]

Synchronized dependencies between pyproject.toml and requirements.txt

[mdmitry1]

Updated python311-dev image index digest

[fbrausse]

First, a couple of remarks from building the wheel locally on my machine (Gentoo, x86_64, multiarch):

• Setting {GMP,BOOST}_ROOT=/usr Z3_PREFIX=/usr, the setup.py script writes *.pc files in seemingly random locations (PWD is /home/kane/tmp10):

  [smlp build] Using BOOST_ROOT=/usr
  [smlp build] $ git clone https://github.com/fbrausse/kay /home/kane/tmp10/build/temp.linux-x86_64-cpython-311/kay
  [smlp build] Looking for libz3.so in: /usr
  [smlp build] Using z3 lib dir: /usr
  [smlp build] Wrote pkg-config file: /home/kane/tmp10/pkgconfig/z3.pc
  [smlp build] Using system z3: /usr/bin/z3
  [smlp build] Using GMP_ROOT=/usr
  [smlp build] pkgconfig dir not writable; writing GMP .pc files to /home/kane/.local/share/pkgconfig
  [smlp build] Wrote pkg-config file: /home/kane/.local/share/pkgconfig/gmp.pc
  [smlp build] Wrote pkg-config file: /home/kane/.local/share/pkgconfig/gmpxx.pc
  

  $HOME/.local/share should not be written to, especially overwriting *.pc files in there can break user's local installations. For some reason, the made-up z3.pc is written directly into the repo's source tree while for boost no *.pc is written (and none is necessary).
• Using the system's boost library, meson fails to find it due to boost_libdir being set to the "lib" subdirectory while on my system "lib64" would be correct. Patching the string constant in setup.py then succeeds.
• Due to me having flint on my system, which meson detects and auto-enables, my locally generated wheel also contains these libraries:

    8232601  03-24-2026 05:09   smlp.libs/libflexiblas-48670b44.so.3.5
   11053361  03-24-2026 05:09   smlp.libs/libflint-6d7b1291.so.16.1.4
     803337  03-24-2026 05:09   smlp.libs/libmpfr-3c9038d0.so.6.2.2
  

  Due to dynamically loading BLAS, the installed wheel then fails for import smlp with:

  >>> import smlp
  flexiblas  Failed to load the BLAS fallback library.  Abort! errormsg="(null)"
  Aborted                python3.11
  

  Hence, we should explicitly disable the flint dependency for utils/poly, e.g., via this patch.

The location of the repair-script under scripts/docker is a bit counter-intuitive. Seeing as we might get additional build scripts (#72), maybe scripts/wheel would be a better place to put it.

With these patches and settings, I was able to successfully build and install the wheel and to run the provided smlp command. I realize that my setup-boost-patch is not necessarily portable, so probably a different solution needs to be found. However, unconditionally disabling flint via the second patch above would be good to do regardless.

Let me also note that running meson for utils/poly without any "native-file", without writing custom *.pc files and without setting any of the LDFLAGS, LD_LIBRARY_PATH, LIBRARY_PATH environment variables actually works on all systems with the appropriate -devel pkgs installed that I checked (Gentoo, Debian, Ubuntu, OpenSUSE), including finding boost on multiarch systems. So I don't understand why those files and settings are necessary.

[fbrausse]

To summarize:

• Should disable building utils/poly against flint.
• Do not write to $HOME/.local. If we want to keep the cached compiled boost and GMP, $HOME/.cache/smlp-wheel would be a more appropriate location for both.
• z3.pc should be put in the build directory.
• Similarly, a directory smlp.egg-info is created in the repo tree. Is there a way to avoid that by, e.g., moving it to build as well?
• Similarly, again, utils/poly/build created by setup.py would be better located under the temporary build directory pip uses.
• Maybe move repair-script to scripts/wheel.

I noticed the new "stub libpythonX.Y.so" generated by setup.py to enable the meson step for utils/poly on systems without it. Once I have the manylinux container running, I'll investigate whether there is a better solution than faking a system library. Edit: For this PR the fake libpython is fine, though.

[fbrausse]

Running the regression tests with the wheel provided by this PR, I get - besides others - a lot of failed tests due to trivial JSON differences where just the order inside an object changes, such as:

--- ../master/Test126_smlp_toy_basic_verify_results.json	2026-03-24 05:35:36.724375983 +0100
+++ Test126_smlp_toy_basic_verify_results.json	2026-03-24 07:22:23.879998772 +0100
@@ -3,12 +3,12 @@
 		"configuration_consistent": "true",
 		"assertion_status": "FAIL",
 		"counter_example": {
-			"x1": 0.0,
-			"p2": 0.0,
-			"y1": 0.2,
 			"x2": 0.0,
+			"y1": 0.2,
+			"x1": 0.0,
 			"p1": 0.2,
-			"y2": 0.0
+			"y2": 0.0,
+			"p2": 0.0
 		},
 		"assertion_feasible": true
 	},

[fbrausse]

I've checked the diffs to master and they all seem to be noise. Quite hard to check, though... I'll open an issue for the notes from my summary above. For this PR being concerned mainly about manylinux wheels, they are not blocking.