python-sat: update packages

.github/workflows/build-python-sat.yml

@@ -35,10 +35,6 @@ permissions:
   contents: read  # to fetch code (actions/checkout)
 
 env:
-  # Upstream pushes no git tag for its releases; this commit sets
-  # VERSION = (1, 9, 'dev', 15) and its tree is byte-identical to the released
-  # sdist. Move it together with the version in docs/packages/python-sat.yaml.
-  PYTHON_SAT_REF: 152884a6d1889f56a61049aaa773be23f0a8d8c1
   MANYLINUX_RISCV64_IMAGE: quay.io/pypa/manylinux_2_39_riscv64
   MUSLLINUX_RISCV64_IMAGE: quay.io/pypa/musllinux_1_2_riscv64
 
@@ -66,11 +62,24 @@ jobs:
       PYTHON_SAT_VERSION: ${{ matrix.version }}
 
     steps:
-      - name: Checkout pysat ${{ env.PYTHON_SAT_REF }}
+      # Upstream pushes no git tag for its releases; each commit below sets
+      # VERSION = (1, 9, 'dev', N) and its tree is the released sdist's. Add the
+      # commit of every new version here, together with docs/packages/python-sat.yaml.
+      - name: Resolve upstream commit for ${{ env.PYTHON_SAT_VERSION }}
+        id: upstream_ref
+        run: |
+          case "$PYTHON_SAT_VERSION" in
+            1.9.dev15) ref=152884a6d1889f56a61049aaa773be23f0a8d8c1 ;;
+            1.9.dev17) ref=5c6d801fb1fae958f6504af5692fa26b807c8e76 ;;
+            *) echo "No upstream commit recorded for python-sat $PYTHON_SAT_VERSION" >&2; exit 1 ;;
+          esac
+          echo "ref=${ref}" >> "$GITHUB_OUTPUT"
+
+      - name: Checkout pysat ${{ steps.upstream_ref.outputs.ref }}
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
         with:
           repository: pysathq/pysat
-          ref: ${{ env.PYTHON_SAT_REF }}
+          ref: ${{ steps.upstream_ref.outputs.ref }}
           persist-credentials: false
 
       - name: Checkout python-wheels
@@ -106,14 +115,18 @@ jobs:
           #   Rewrite that one slot to 0 in the unpacked sdist before installing it.
           # The python-sat wheel itself builds unchanged on musllinux; only this
           # test dependency needs the workaround. Alpine is detected in-container.
+          # From 1.9.dev17 requirements.txt lists pindakaas (a Rust extension with no
+          # riscv64 wheel) instead of pypblib; the tests that need it importorskip it,
+          # so it is left out rather than source-built.
           CIBW_BEFORE_TEST: >-
-            if [ -f /etc/alpine-release ]; then
+            if [ -f /etc/alpine-release ] && grep -q '^pypblib' {project}/requirements.txt; then
             pip download --no-deps --no-binary :all: pypblib==0.0.4 -d /tmp/pypblib &&
             tar -xzf /tmp/pypblib/pypblib-0.0.4.tar.gz -C /tmp/pypblib &&
             sed -i 's|NULL\(, */\* tp_print \*/\)|0\1|' /tmp/pypblib/pypblib-0.0.4/Modules/pblib/*.cpp &&
             CPPFLAGS="-include sys/types.h" pip install /tmp/pypblib/pypblib-0.0.4;
             fi &&
-            pip install -r {project}/requirements.txt
+            grep -v '^pindakaas' {project}/requirements.txt > /tmp/requirements.txt &&
+            pip install -r /tmp/requirements.txt
           CIBW_TEST_REQUIRES: pytest
           CIBW_TEST_SOURCES: tests
           CIBW_TEST_COMMAND: >-

docs/packages/python-sat.yaml

@@ -26,3 +26,4 @@ versions:
     sha256: 4e98da83841abe57e67d39820a0088b2cb8849b688497049bb695445c6e03d57
   - filename: python_sat-1.9.dev15-cp314-cp314t-musllinux_1_2_riscv64.whl
     sha256: 97ddffdf92f0de0da940ca2e5a51064839eb08bc65e26e8246f40729c1dac9ff
+- version: 1.9.dev17

patches/python-sat/1.9.dev17/0001-build-without-the-Lingeling-solver.patch

@@ -0,0 +1,81 @@
+From c2359bfbabe0826799295fb3df2bca120a8c4179 Mon Sep 17 00:00:00 2001
+From: Ludovic Henry <git@ludovic.dev>
+Date: Sun, 27 Sep 2026 22:08:42 +0000
+Subject: [PATCH 1/2] build without the Lingeling solver
+
+Upstream-Status: Inappropriate [licensing: the bundled Lingeling bbc-9230380-160707 licence grants use for evaluation and research only, forbids commercial use and reserves all other rights, so it gives no permission to redistribute it in a binary wheel]
+
+setup.py statically links every solver listed in to_install into the
+pysolvers extension. The Lingeling tarball in solvers/lingeling.tar.gz
+(lingeling-bbc-9230380-160707/COPYING) is not under the MIT terms that
+cover PySAT and the other bundled solvers: it permits use "for
+evaluation and research purposes", prohibits use "in a commercial
+context" and ends with "All other usage is reserved". A third party
+rebuilding and publishing wheels has no grant to redistribute it.
+
+Drop 'lingeling' from to_install. pysolvers.cc guards all Lingeling
+code behind WITH_LINGELING, so the extension builds and links without
+it; pysat.solvers.Lingeling (and Solver(name='lingeling')) then fails
+with an AttributeError on pysolvers.lingeling_new. Remove 'lingeling'
+from the solver lists of the three tests that loop over every solver
+so that they keep exercising the remaining nineteen.
+
+Signed-off-by: Ludovic Henry <git@ludovic.dev>
+---
+ setup.py                   | 2 +-
+ tests/test_accum_stats.py  | 1 -
+ tests/test_cnf.py          | 1 -
+ tests/test_unique_model.py | 1 -
+ 4 files changed, 1 insertion(+), 4 deletions(-)
+
+diff --git a/setup.py b/setup.py
+index 65da94a..837c620 100644
+--- a/setup.py
++++ b/setup.py
+@@ -70,7 +70,7 @@ Details can be found at `https://pysathq.github.io <https://pysathq.github.io>`_
+ #==============================================================================
+ to_install = ['cadical103', 'cadical153', 'cadical195', 'cadical300',
+               'ergo', 'gluecard30', 'gluecard41', 'glucose30', 'glucose41',
+-              'glucose421', 'kissat404', 'lingeling', 'maplechrono',
++              'glucose421', 'kissat404', 'maplechrono',
+               'maplecm', 'maplesat', 'mergesat3', 'minicard', 'minisat22',
+               'minisatgh', 'minisatep']
+
+diff --git a/tests/test_accum_stats.py b/tests/test_accum_stats.py
+index db93994..24f560f 100644
+--- a/tests/test_accum_stats.py
++++ b/tests/test_accum_stats.py
+@@ -10,7 +10,6 @@ solvers = ['cadical103',
+            'gluecard41',
+            'glucose30',
+            'glucose42',
+-           'lingeling',
+            'maplechrono',
+            'maplecm',
+            'maplesat',
+diff --git a/tests/test_cnf.py b/tests/test_cnf.py
+index 00a2205..1511ce1 100644
+--- a/tests/test_cnf.py
++++ b/tests/test_cnf.py
+@@ -14,7 +14,6 @@ solvers = ['cadical103',
+            'glucose30',
+            'glucose41',
+            'glucose42',
+-           'lingeling',
+            'maplechrono',
+            'maplecm',
+            'maplesat',
+diff --git a/tests/test_unique_model.py b/tests/test_unique_model.py
+index 35d86b6..9fd127d 100644
+--- a/tests/test_unique_model.py
++++ b/tests/test_unique_model.py
+@@ -11,7 +11,6 @@ solvers = ['cadical103',
+            'glucose30',
+            'glucose41',
+            'glucose42',
+-           'lingeling',
+            'maplechrono',
+            'maplecm',
+            'maplesat',
+-- 
+2.43.0