Package: guix-patches;
Reported by: Nguyễn Gia Phong <mcsinyx <at> disroot.org>
Date: Fri, 10 Jan 2025 13:00:02 UTC
Severity: normal
Tags: patch
Done: Leo Famulari <leo <at> famulari.name>
Bug is archived. No further changes may be made.
View this message in rfc822 format
From: help-debbugs <at> gnu.org (GNU bug Tracking System) To: Leo Famulari <leo <at> famulari.name> Cc: tracker <at> debbugs.gnu.org Subject: bug#75476: closed ([PATCH] gnu: python-pysmt: Update to 0.9.6.) Date: Sun, 02 Feb 2025 22:08:02 +0000
[Message part 1 (text/plain, inline)]
Your message dated Sun, 2 Feb 2025 17:06:53 -0500 with message-id <Z5_sfQBx26rn_ZFb <at> jasmine.lan> and subject line Re: [bug#75476] QA review for 75476 has caused the debbugs.gnu.org bug report #75476, regarding [PATCH] gnu: python-pysmt: Update to 0.9.6. to be marked as done. (If you believe you have received this mail in error, please contact help-debbugs <at> gnu.org.) -- 75476: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=75476 GNU Bug Tracking System Contact help-debbugs <at> gnu.org with problems
[Message part 2 (message/rfc822, inline)]
From: Nguyễn Gia Phong <mcsinyx <at> disroot.org> To: guix-patches <at> gnu.org Cc: Nguyễn Gia Phong <mcsinyx <at> disroot.org> Subject: [PATCH] gnu: python-pysmt: Update to 0.9.6. Date: Fri, 10 Jan 2025 21:59:21 +0900* gnu/packages/python-xyz.scm (python-pysmt): Update to 0.9.6. * gnu/packages/patches/python-pysmt-fix-pow-return-type.patch: Remove file. * gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch: Remove file. * gnu/local.mk (dist_patch_DATA): Unregister them. Change-Id: I4ecdad59abbb1c755a5be081cf3bf75992b36fb3 --- gnu/local.mk | 2 - .../python-pysmt-fix-pow-return-type.patch | 258 ------------------ ...-pysmt-fix-smtlib-serialization-test.patch | 86 ------ gnu/packages/python-xyz.scm | 9 +- 4 files changed, 4 insertions(+), 351 deletions(-) delete mode 100644 gnu/packages/patches/python-pysmt-fix-pow-return-type.patch delete mode 100644 gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch diff --git a/gnu/local.mk b/gnu/local.mk index 1d15be886da3..db2815dd2565 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -2104,8 +2104,6 @@ dist_patch_DATA = \ %D%/packages/patches/python-paste-remove-timing-test.patch \ %D%/packages/patches/python-pyan3-fix-absolute-path-bug.patch \ %D%/packages/patches/python-pyan3-fix-positional-arguments.patch \ - %D%/packages/patches/python-pysmt-fix-pow-return-type.patch \ - %D%/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch \ %D%/packages/patches/python-pytorch-fix-codegen.patch \ %D%/packages/patches/python-pytorch-runpath.patch \ %D%/packages/patches/python-pytorch-system-libraries.patch \ diff --git a/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch b/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch deleted file mode 100644 index 0ec2d41b3c48..000000000000 --- a/gnu/packages/patches/python-pysmt-fix-pow-return-type.patch +++ /dev/null @@ -1,258 +0,0 @@ -Backport of an upstream patch which fixes a test failure with our -packaged version of the Z3 SMT solver. - -Taken from: https://github.com/pysmt/pysmt/commit/f522e8cd8f3e75ff85f5eae29b427e18a6701859 - -diff --git a/pysmt/formula.py b/pysmt/formula.py -index ea4b46c..6cb9cbf 100644 ---- a/pysmt/formula.py -+++ b/pysmt/formula.py -@@ -252,11 +252,7 @@ class FormulaManager(object): - - if base.is_constant(): - val = base.constant_value() ** exponent.constant_value() -- if base.is_constant(types.REAL): -- return self.Real(val) -- else: -- assert base.is_constant(types.INT) -- return self.Int(val) -+ return self.Real(val) - return self.create_node(node_type=op.POW, args=(base, exponent)) - - def Div(self, left, right): -diff --git a/pysmt/logics.py b/pysmt/logics.py -index ef88dd6..9dc45b1 100644 ---- a/pysmt/logics.py -+++ b/pysmt/logics.py -@@ -495,6 +495,12 @@ QF_NRA = Logic(name="QF_NRA", - real_arithmetic=True, - linear=False) - -+QF_NIRA = Logic(name="QF_NIRA", -+ description="""Quantifier-free integer and real arithmetic.""", -+ quantifier_free=True, -+ integer_arithmetic=True, -+ real_arithmetic=True, -+ linear=False) - - QF_RDL = Logic(name="QF_RDL", - description=\ -@@ -619,41 +625,41 @@ QF_AUFBVLIRA = Logic(name="QF_AUFBVLIRA", - AUTO = Logic(name="Auto", - description="Special logic used to indicate that the logic to be used depends on the formula.") - --SMTLIB2_LOGICS = frozenset([ AUFLIA, -- AUFLIRA, -- AUFNIRA, -- ALIA, -- LRA, -- LIA, -- NIA, -- NRA, -- UFLRA, -- UFNIA, -- UFLIRA, -- QF_ABV, -- QF_AUFBV, -- QF_AUFLIA, -- QF_ALIA, -- QF_AX, -- QF_BV, -- QF_IDL, -- QF_LIA, -- QF_LRA, -- QF_NIA, -- QF_NRA, -- QF_RDL, -- QF_UF, -- QF_UFBV , -- QF_UFIDL, -- QF_UFLIA, -- QF_UFLRA, -- QF_UFNRA, -- QF_UFNIA, -- QF_UFLIRA, -- QF_SLIA -- ]) -- --LOGICS = SMTLIB2_LOGICS | frozenset([ QF_BOOL, BOOL, QF_AUFBVLIRA]) -+SMTLIB2_LOGICS = frozenset([AUFLIA, -+ AUFLIRA, -+ AUFNIRA, -+ ALIA, -+ LRA, -+ LIA, -+ NIA, -+ NRA, -+ UFLRA, -+ UFNIA, -+ UFLIRA, -+ QF_ABV, -+ QF_AUFBV, -+ QF_AUFLIA, -+ QF_ALIA, -+ QF_AX, -+ QF_BV, -+ QF_IDL, -+ QF_LIA, -+ QF_LRA, -+ QF_NIA, -+ QF_NRA, -+ QF_RDL, -+ QF_UF, -+ QF_UFBV, -+ QF_UFIDL, -+ QF_UFLIA, -+ QF_UFLRA, -+ QF_UFNRA, -+ QF_UFNIA, -+ QF_UFLIRA, -+ QF_SLIA -+ ]) -+ -+LOGICS = SMTLIB2_LOGICS | frozenset([QF_BOOL, BOOL, QF_AUFBVLIRA, QF_NIRA]) - - QF_LOGICS = frozenset(_l for _l in LOGICS if _l.quantifier_free) - -@@ -668,8 +674,8 @@ PYSMT_LOGICS = frozenset([QF_BOOL, QF_IDL, QF_LIA, QF_LRA, QF_RDL, QF_UF, QF_UFI - QF_BV, QF_UFBV, - QF_ABV, QF_AUFBV, QF_AUFLIA, QF_ALIA, QF_AX, - QF_AUFBVLIRA, -- QF_NRA, QF_NIA, UFBV, BV, -- ]) -+ QF_NRA, QF_NIA, QF_NIRA, UFBV, BV, -+ ]) - - # PySMT Logics includes additional features: - # - constant arrays: QF_AUFBV becomes QF_AUFBV* -@@ -697,7 +703,6 @@ for l in PYSMT_LOGICS: - ext_logics.add(nl) - - -- - LOGICS = LOGICS | frozenset(ext_logics) - PYSMT_LOGICS = PYSMT_LOGICS | frozenset(ext_logics) - -diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py -index 3fb42b9..210b771 100644 ---- a/pysmt/solvers/z3.py -+++ b/pysmt/solvers/z3.py -@@ -595,6 +595,8 @@ class Z3Converter(Converter, DagWalker): - None, None, - 0, None, - expr.ast) -+ print("Z3: SMTLIB") -+ print(s) - stream_in = StringIO(s) - r = parser.get_script(stream_in).get_last_formula(self.mgr) - key = (askey(expr), None) -diff --git a/pysmt/test/examples.py b/pysmt/test/examples.py -index 73455ee..b653185 100644 ---- a/pysmt/test/examples.py -+++ b/pysmt/test/examples.py -@@ -898,12 +898,12 @@ def get_full_example_formulae(environment=None): - logic=pysmt.logics.QF_NRA - ), - -- Example(hr="((p ^ 2) = 0)", -- expr=Equals(Pow(p, Int(2)), Int(0)), -+ Example(hr="((p ^ 2) = 0.0)", -+ expr=Equals(Pow(p, Int(2)), Real(0)), - is_valid=False, - is_sat=True, -- logic=pysmt.logics.QF_NIA -- ), -+ logic=pysmt.logics.QF_NIRA -+ ), - - Example(hr="((r ^ 2.0) = 0.0)", - expr=Equals(Pow(r, Real(2)), Real(0)), -diff --git a/pysmt/test/test_back.py b/pysmt/test/test_back.py -index bceb45b..7a0ad63 100644 ---- a/pysmt/test/test_back.py -+++ b/pysmt/test/test_back.py -@@ -55,10 +55,10 @@ class TestBasic(TestCase): - res = msat.converter.back(term) - self.assertFalse(f == res) - -- def do_back(self, solver_name, z3_string_buffer=False): -+ def do_back(self, solver_name, via_smtlib=False): - for formula, _, _, logic in get_example_formulae(): - if logic.quantifier_free: -- if logic.theory.custom_type and z3_string_buffer: -+ if logic.theory.custom_type and via_smtlib: - # Printing of declare-sort from Z3 is not conformant - # with the SMT-LIB. We might consider extending our - # parser. -@@ -67,7 +67,7 @@ class TestBasic(TestCase): - s = Solver(name=solver_name, logic=logic) - term = s.converter.convert(formula) - if solver_name == "z3": -- if z3_string_buffer: -+ if via_smtlib: - res = s.converter.back_via_smtlib(term) - else: - res = s.converter.back(term) -@@ -84,8 +84,8 @@ class TestBasic(TestCase): - - @skipIfSolverNotAvailable("z3") - def test_z3_back_formulae(self): -- self.do_back("z3", z3_string_buffer=False) -- self.do_back("z3", z3_string_buffer=True) -+ self.do_back("z3", via_smtlib=True) -+ self.do_back("z3", via_smtlib=False) - - - if __name__ == '__main__': -diff --git a/pysmt/type_checker.py b/pysmt/type_checker.py -index b700fcf..7ce05aa 100644 ---- a/pysmt/type_checker.py -+++ b/pysmt/type_checker.py -@@ -33,6 +33,8 @@ class SimpleTypeChecker(walkers.DagWalker): - - def __init__(self, env=None): - walkers.DagWalker.__init__(self, env=env) -+ # Return None if the type cannot be computed rather than -+ # raising an exception. - self.be_nice = False - - def _get_key(self, formula, **kwargs): -@@ -42,7 +44,7 @@ class SimpleTypeChecker(walkers.DagWalker): - """ Returns the pysmt.types type of the formula """ - res = self.walk(formula) - if not self.be_nice and res is None: -- raise PysmtTypeError("The formula '%s' is not well-formed" \ -+ raise PysmtTypeError("The formula '%s' is not well-formed" - % str(formula)) - return res - -@@ -114,7 +116,7 @@ class SimpleTypeChecker(walkers.DagWalker): - - def walk_bv_comp(self, formula, args, **kwargs): - # We check that all children are BV and the same size -- a,b = args -+ a, b = args - if a != b or (not a.is_bv_type()): - return None - return BVType(1) -@@ -187,7 +189,7 @@ class SimpleTypeChecker(walkers.DagWalker): - if args[0].is_bool_type(): - raise PysmtTypeError("The formula '%s' is not well-formed." - "Equality operator is not supported for Boolean" -- " terms. Use Iff instead." \ -+ " terms. Use Iff instead." - % str(formula)) - elif args[0].is_bv_type(): - return self.walk_bv_to_bool(formula, args) -@@ -324,10 +326,7 @@ class SimpleTypeChecker(walkers.DagWalker): - def walk_pow(self, formula, args, **kwargs): - if args[0] != args[1]: - return None -- # Exponent must be positive for INT -- if args[0].is_int_type() and formula.arg(1).constant_value() < 0 : -- return None -- return args[0] -+ return REAL - - # EOC SimpleTypeChecker - diff --git a/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch b/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch deleted file mode 100644 index eee555f80783..000000000000 --- a/gnu/packages/patches/python-pysmt-fix-smtlib-serialization-test.patch +++ /dev/null @@ -1,86 +0,0 @@ -Backport of an upstream patch fixing a test suite failure. - -Taken from: https://github.com/pysmt/pysmt/commit/a246669a487aff69f5da34570ef867841d18508a - -diff --git a/pysmt/test/smtlib/test_parser_examples.py b/pysmt/test/smtlib/test_parser_examples.py -index cca4194..c0852be 100644 ---- a/pysmt/test/smtlib/test_parser_examples.py -+++ b/pysmt/test/smtlib/test_parser_examples.py -@@ -29,6 +29,7 @@ from pysmt.shortcuts import Iff - from pysmt.shortcuts import read_smtlib, write_smtlib, get_env - from pysmt.exceptions import PysmtSyntaxError - -+ - class TestSMTParseExamples(TestCase): - - def test_parse_examples(self): -@@ -41,7 +42,6 @@ class TestSMTParseExamples(TestCase): - buf = StringIO() - script_out = smtlibscript_from_formula(f_out) - script_out.serialize(outstream=buf) -- #print(buf) - - buf.seek(0) - parser = SmtLibParser() -@@ -49,7 +49,6 @@ class TestSMTParseExamples(TestCase): - f_in = script_in.get_last_formula() - self.assertEqual(f_in.simplify(), f_out.simplify()) - -- - @skipIfNoSolverForLogic(logics.QF_BV) - def test_parse_examples_bv(self): - """For BV we represent a superset of the operators defined in SMT-LIB. -@@ -108,7 +107,18 @@ class TestSMTParseExamples(TestCase): - self.assertValid(Iff(f_in, f_out), f_in.serialize()) - - def test_dumped_logic(self): -- # Dumped logic matches the logic in the example -+ # Dumped logic matches the logic in the example. -+ # -+ # There are a few cases where we use a logic -+ # that does not exist in SMT-LIB, and the SMT-LIB -+ # serialization logic will find a logic that -+ # is more expressive. We need to adjust the test -+ # for those cases (see rewrite dict below). -+ rewrite = { -+ logics.QF_BOOL: logics.QF_UF, -+ logics.BOOL: logics.LRA, -+ logics.QF_NIRA: logics.AUFNIRA, -+ } - fs = get_example_formulae() - - for (f_out, _, _, logic) in fs: -@@ -121,14 +131,9 @@ class TestSMTParseExamples(TestCase): - for cmd in script_in: - if cmd.name == "set-logic": - logic_in = cmd.args[0] -- if logic == logics.QF_BOOL: -- self.assertEqual(logic_in, logics.QF_UF) -- elif logic == logics.BOOL: -- self.assertEqual(logic_in, logics.LRA) -- else: -- self.assertEqual(logic_in, logic, script_in) -+ self.assertEqual(logic_in, rewrite.get(logic, logic)) - break -- else: # Loops exited normally -+ else: # Loops exited normally - print("-"*40) - print(script_in) - -@@ -136,7 +141,7 @@ class TestSMTParseExamples(TestCase): - fs = get_example_formulae() - - fdi, tmp_fname = mkstemp() -- os.close(fdi) # Close initial file descriptor -+ os.close(fdi) # Close initial file descriptor - for (f_out, _, _, _) in fs: - write_smtlib(f_out, tmp_fname) - # with open(tmp_fname) as fin: -@@ -197,7 +202,6 @@ class TestSMTParseExamples(TestCase): - f_in = script.get_last_formula() - self.assertSat(f_in) - -- - def test_int_promotion_define_fun(self): - script = """ - (define-fun x () Int 8) diff --git a/gnu/packages/python-xyz.scm b/gnu/packages/python-xyz.scm index ceb26960e3e7..201a75fa4fa7 100644 --- a/gnu/packages/python-xyz.scm +++ b/gnu/packages/python-xyz.scm @@ -160,6 +160,7 @@ ;;; Copyright © 2024 Evgeny Pisemsky <mail <at> pisemsky.site> ;;; Copyright © 2024 Markku Korkeala <markku.korkeala <at> iki.fi> ;;; Copyright © 2025 Jordan Moore <lockbox <at> struct.foo> +;;; Copyright © 2025 Nguyễn Gia Phong <mcsinyx <at> disroot.org> ;;; ;;; This file is part of GNU Guix. ;;; @@ -35655,26 +35656,24 @@ (define-public python-claripy (define-public python-pysmt (package (name "python-pysmt") - (version "0.9.5") + (version "0.9.6") (source (origin ;; Fetching from Git as pypi release doesn't include all test files. (method git-fetch) - (patches (search-patches "python-pysmt-fix-pow-return-type.patch" - "python-pysmt-fix-smtlib-serialization-test.patch")) (uri (git-reference (url "https://github.com/pysmt/pysmt") (commit (string-append "v" version)))) (file-name (git-file-name name version)) (sha256 - (base32 "0hrxv23y5ip4ijfx5pvbwc2fq4zg9jz42wc9zqgqm0g0mjc9ckvh")))) + (base32 "0jiw8pa6hfh9ajr953q187qgpdnk3bvaa3wmrxs8ilw5jc41sq8y")))) (build-system pyproject-build-system) (arguments `(#:phases (modify-phases %standard-phases (add-before 'check 'set-pysmt-solver (lambda _ (setenv "PYSMT_SOLVER" "z3")))))) - (native-inputs (list python-pytest)) + (native-inputs (list python-setuptools python-wheel python-pytest)) (propagated-inputs (list z3)) (home-page "https://github.com/pysmt/pysmt") (synopsis base-commit: 461d773adead955e2daead70cee4415f7f0f00be -- 2.46.0
[Message part 3 (message/rfc822, inline)]
From: Leo Famulari <leo <at> famulari.name> To: Nicolas Graves <ngraves <at> ngraves.fr>, Nguyễn Gia Phong <mcsinyx <at> disroot.org> Cc: 75476-done <at> debbugs.gnu.org Subject: Re: [bug#75476] QA review for 75476 Date: Sun, 2 Feb 2025 17:06:53 -0500On Sun, Feb 02, 2025 at 04:09:19PM +0100, Nicolas Graves via Guix-patches via wrote: > user guix > usertag 75476 + reviewed-looks-good > thanks > > Guix QA review form submission: > I've just resent a version to fix git conflicts. Tested on x86-64, lints too. LGTM. > > Items marked as checked: Lint warnings, Package builds, Commit messages Thanks for patch Nguyễn! Pushed as commit fa0ab2f70fa3a363d84f9dd795f008e632d2c145: https://git.savannah.gnu.org/cgit/guix.git/commit/?id=4fccad83875cf8f5846b181525f814ce5c240ef9 And thanks to Nicolas for the review!
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.