Skip to content

SMLP package build and test for python3.12#55

Draft
mdmitry1 wants to merge 137 commits into
masterfrom
smlp_python312
Draft

SMLP package build and test for python3.12#55
mdmitry1 wants to merge 137 commits into
masterfrom
smlp_python312

Conversation

@mdmitry1

@mdmitry1 mdmitry1 commented Mar 10, 2026

Copy link
Copy Markdown
Collaborator
  • python3.12
  • keras==3.14.1
  • tensorflow==2.21.0
  • tensorboard==2.20.0
  • backward compatible with existing python3.11 SMLP version

…upport

2) Downgraded pydoe from 0.9.7 to 0.3.8 due to interface change incompatible with doepy 0.0.1
3) Ported enhanced VNC support from python3.11 version in poly_pareto branch

@mdmitry1 mdmitry1 left a comment

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

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

Reviewed changes

@fbrausse fbrausse left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

I would like to keep the Python-3.11 build in the CI. That Python version is not EOL, yet, see: https://devguide.python.org/versions/

Comment thread .github/workflows/build-wheels.yml Outdated
env:
# see <https://cibuildwheel.pypa.io/en/stable/options/#build-skip>
CIBW_BUILD: cp311-*
CIBW_BUILD: cp312-*

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Suggested change
CIBW_BUILD: cp312-*
CIBW_BUILD: cp311-* cp312-*

This of course requires to be less explicit about export PYTHON=python3.12 in install-z3.sh as well, see the other suggestion.

Comment thread .github/workflows/install-z3.sh Outdated
eval ${P}_R=${R:-\$`echo ${P}_S`/prefix} # install prefix

export PYTHON=python3.11
export PYTHON=python3.12

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Suggested change
export PYTHON=python3.12
export PYTHON=python3

@mdmitry1

Copy link
Copy Markdown
Collaborator Author

There is a problem with Z3 version on python3.12: version 4.8.12 is not supported:

3616 Traceback (most recent call last):
3617    File "/root/z3/z3-z3-4.8.12/scripts/mk_make.py", line 9, in <module>
3618      from mk_util import *
3619    File "/root/z3/z3-z3-4.8.12/scripts/mk_util.py", line 18, in <module>
3620      import distutils.sysconfig
3621  ModuleNotFoundError: No module named 'distutils'

Reproduction - see Build 54

Therefore install-z3.sh script should be adjusted accordingly and we will lose 3 tests due to this issue on python3.12:
154,155,157.

@fbrausse

Copy link
Copy Markdown
Collaborator

Indeed, there are more problems with the Z3 build:

Details
2026-05-22T13:36:48.0951640Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:383: SyntaxWarning: invalid escape sequence '\['
2026-05-22T13:36:48.0953182Z   open_pat = re.compile("\[search path for class files: (.*)\]")
2026-05-22T13:36:48.0977812Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:775: SyntaxWarning: invalid escape sequence '\<'
2026-05-22T13:36:48.0980290Z   system_inc_pat  = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*")
2026-05-22T13:36:48.1035280Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:1719: SyntaxWarning: invalid escape sequence '\%'
2026-05-22T13:36:48.1039691Z   <Compile Include="..\%s\*.cs;*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
2026-05-22T13:36:48.1074195Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:2211: SyntaxWarning: invalid escape sequence '\%'
2026-05-22T13:36:48.1079692Z   <Compile Include="..\%s/*.cs" />
2026-05-22T13:36:48.1138995Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:3094: SyntaxWarning: invalid escape sequence '\M'
2026-05-22T13:36:48.1145300Z   f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />\n')
2026-05-22T13:36:48.1146667Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:3105: SyntaxWarning: invalid escape sequence '\M'
2026-05-22T13:36:48.1152625Z   f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />\n')
2026-05-22T13:36:48.1154006Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:3108: SyntaxWarning: invalid escape sequence '\M'
2026-05-22T13:36:48.1160946Z   f.write('    <Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" />  </ImportGroup>\n')
2026-05-22T13:36:48.1163246Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:3111: SyntaxWarning: invalid escape sequence '\$'
2026-05-22T13:36:48.1168624Z   f.write('    <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n')
2026-05-22T13:36:48.1170206Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:3114: SyntaxWarning: invalid escape sequence '\$'
2026-05-22T13:36:48.1176694Z   f.write('    <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n')
2026-05-22T13:36:48.1178476Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:3119: SyntaxWarning: invalid escape sequence '\$'
2026-05-22T13:36:48.1184114Z   f.write('        <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n')
2026-05-22T13:36:48.1185032Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:3122: SyntaxWarning: invalid escape sequence '\$'
2026-05-22T13:36:48.1190719Z   f.write('    <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n')
2026-05-22T13:36:48.1197219Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:3199: SyntaxWarning: invalid escape sequence '\M'
2026-05-22T13:36:48.1202581Z   f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n')
2026-05-22T13:36:48.1207267Z /root/z3/z3-z3-4.8.12/scripts/mk_util.py:3240: SyntaxWarning: invalid escape sequence '\M'
2026-05-22T13:36:48.1213020Z   f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n')
2026-05-22T13:36:48.1546052Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:142: SyntaxWarning: invalid escape sequence '\-'
2026-05-22T13:36:48.1546919Z   words = re.split('[^\-a-zA-Z0-9_]+', line)
2026-05-22T13:36:48.1550159Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:230: SyntaxWarning: invalid escape sequence '\-'
2026-05-22T13:36:48.1551141Z   words = re.split('[^\-a-zA-Z0-9_]+', line)
2026-05-22T13:36:48.1555265Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:318: SyntaxWarning: invalid escape sequence '\-'
2026-05-22T13:36:48.1556288Z   words = re.split('[^\-a-zA-Z0-9_]+', line)
2026-05-22T13:36:48.1562475Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:444: SyntaxWarning: invalid escape sequence '\-'
2026-05-22T13:36:48.1563445Z   words = re.split('[^\-a-zA-Z0-9_]+', line)
2026-05-22T13:36:48.1567382Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:577: SyntaxWarning: invalid escape sequence '\W'
2026-05-22T13:36:48.1568303Z   words = re.split('\W+', line)
2026-05-22T13:36:48.1570359Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:621: SyntaxWarning: invalid escape sequence '\('
2026-05-22T13:36:48.1571233Z   reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)')
2026-05-22T13:36:48.1572037Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:622: SyntaxWarning: invalid escape sequence '\('
2026-05-22T13:36:48.1573185Z   reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)')
2026-05-22T13:36:48.1574121Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:623: SyntaxWarning: invalid escape sequence '\('
2026-05-22T13:36:48.1575395Z   reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
2026-05-22T13:36:48.1576605Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:695: SyntaxWarning: invalid escape sequence '\('
2026-05-22T13:36:48.1577664Z   tactic_pat   = re.compile('[ \t]*ADD_TACTIC\(.*\)')
2026-05-22T13:36:48.1578472Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:696: SyntaxWarning: invalid escape sequence '\('
2026-05-22T13:36:48.1579285Z   probe_pat    = re.compile('[ \t]*ADD_PROBE\(.*\)')
2026-05-22T13:36:48.1581673Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:762: SyntaxWarning: invalid escape sequence '\('
2026-05-22T13:36:48.1582235Z   initializer_pat      = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)')
2026-05-22T13:36:48.1582941Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:764: SyntaxWarning: invalid escape sequence '\('
2026-05-22T13:36:48.1583520Z   initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)')
2026-05-22T13:36:48.1584099Z /root/z3/z3-z3-4.8.12/scripts/mk_genfile_common.py:765: SyntaxWarning: invalid escape sequence '\('
2026-05-22T13:36:48.1584611Z   finalizer_pat        = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
2026-05-22T13:36:48.2609036Z Traceback (most recent call last):
2026-05-22T13:36:48.2616800Z   File "/root/z3/z3-z3-4.8.12/scripts/mk_make.py", line 9, in <module>
2026-05-22T13:36:48.2617264Z     from mk_util import *
2026-05-22T13:36:48.2617656Z   File "/root/z3/z3-z3-4.8.12/scripts/mk_util.py", line 18, in <module>
2026-05-22T13:36:48.2618048Z     import distutils.sysconfig
2026-05-22T13:36:48.2618347Z ModuleNotFoundError: No module named 'distutils'

@mdmitry1

Copy link
Copy Markdown
Collaborator Author

Alternative for python3.12 is to use pip install z3-solver==4.8.12. This is what is being done inDockerfile.python312-dev.
However, I don't think that we should stay with the old version of z3 going forward.
Better solution should be to isolate this problem and open a z3-solver issue. In Test157 z3 is stuck after the first call and therefore hopefully it should be relatively easy.

@mdmitry1

Copy link
Copy Markdown
Collaborator Author

I just realized that we may use python3.11 for z3 build always, as we are not using z3 python interface.
So adding python3.11 requires just fixing 3 lines of code.
Result - see Build 69

2. Added multiple wheels support to download_artifact.sh
@mdmitry1

mdmitry1 commented May 30, 2026

Copy link
Copy Markdown
Collaborator Author

Regression passed for both wheels.

Commit: 74fe76c
Tag: v1.3.0rc11
Build: 70

Install command:

pip install -i https://test.pypi.org/simple --extra-index-url https://pypi.org/simple smlptech==1.3.0rc11

Results:

python3.11 results
python3.12 results

Next steps are pending resolution of the issues listed below:

  1. Missing input files for some regression tests
  2. Output files of certain regression tests missing in regr_smlp/master directory
  3. Crashing tests in 1.2.0 release

@mdmitry1 mdmitry1 self-assigned this May 31, 2026
@mdmitry1 mdmitry1 added the enhancement New feature or request label May 31, 2026
@mdmitry1

mdmitry1 commented Jun 3, 2026

Copy link
Copy Markdown
Collaborator Author

Justification of the weights assignment change in smlp_terms.py

git branch --show-current
cd $(git rev-parse --show-toplevel)/regr_smlp/code
git diff ../../src/smlp_py/smlp_terms.py
smlp_python312
diff --git a/src/smlp_py/smlp_terms.py b/src/smlp_py/smlp_terms.py
index afb14e9..9aa791e 100644
--- a/src/smlp_py/smlp_terms.py
+++ b/src/smlp_py/smlp_terms.py
@@ -2326,7 +2326,8 @@ class ModelTerms(ScalerTerms):
                         continue
                     else:
                         curr_layer_nodes_count = getattr(layer, 'units', None)
-                        if keras_major_version < 3:
+                        #if keras_major_version < 3:
+                        if True:
                             assert curr_layer_nodes_count == len(list(layer.weights[1])); 
                         else: 
                             # Get weights properly using get_weights() method
../../src/run_smlp.py -data "../data/smlp_toy_num_resp_mult.csv" -out_dir ./ -pref Test172 -mode verify -resp y2 -feat x,p1,p2 -model nn_keras -mrmr_pred 0 -plots f -pred_plots f -resp_plots f -seed 10 -log_time f -nn_keras_epochs 20 -nn_keras_seq_api f -nnet_encoding layered -nn_keras_tuner hyperband -nn_keras_layers_grid "2,2;3,3,3" -save_model_config f -spec ../specs/smlp_toy_num_resp_mult_y2_verify.spec -asrt_names asrt1 -asrt_exprs "2*y2>1" -sw_coef 4 -sw_exp 5 -sw_int 0.5 -solver_path ../../../external/mathsat-5.6.8-linux-x86_64-reentrant/bin/mathsat"" | & sed -n '/INFO:smlp_logger:Input and knob interface constraints are consistent/,$p'
INFO:smlp_logger:Input and knob interface constraints are consistent
[ext ] note : child 60285 exited with code 0
W0000 00:00:1780502614.455679   59596 op_kernel.cc:1858] OP_REQUIRES failed at strided_slice_op.cc:117 : INVALID_ARGUMENT: slice index 9 of dimension 0 out of bounds.
W0000 00:00:1780502614.455715   59596 local_rendezvous.cc:412] Local rendezvous is aborting with status: INVALID_ARGUMENT: slice index 9 of dimension 0 out of bounds.
Traceback (most recent call last):
  File "/app/smlp/regr_smlp/code/../../src/run_smlp.py", line 20, in <module>
    main(sys.argv)
  File "/app/smlp/regr_smlp/code/../../src/run_smlp.py", line 13, in main
    smlpInst.smlp_flow()
  File "/app/smlp/src/smlp_py/smlp_flows.py", line 345, in smlp_flow
    self.queryInst.smlp_verify(syst_expr_dict, args.model, model, 
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/app/smlp/src/smlp_py/smlp_query.py", line 481, in smlp_verify
    self.validate_witness(True, syst_expr_dict, algo, model,
  File "/app/smlp/src/smlp_py/smlp_query.py", line 309, in validate_witness
    self.get_model_exploration_base_components(mode_status_dict, results_file, 
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/app/smlp/src/smlp_py/smlp_query.py", line 126, in get_model_exploration_base_components
    self._modelTermsInst.create_model_exploration_base_components(
  File "/app/smlp/src/smlp_py/smlp_terms.py", line 2357, in create_model_exploration_base_components
    declare_iternal_node_vars(model, resp_name, resp_names)
  File "/app/smlp/src/smlp_py/smlp_terms.py", line 2331, in declare_iternal_node_vars
    assert curr_layer_nodes_count == len(list(layer.weights[1])); 
                                         ^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.12/dist-packages/keras/src/backend/common/variables.py", line 426, in __getitem__
    return self.value.__getitem__(idx)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.12/dist-packages/tensorflow/python/ops/tensor_getitem_override.py", line 311, in _slice_helper_var
    return _slice_helper(var.value(), slice_spec, var)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/local/lib/python3.12/dist-packages/tensorflow/python/util/traceback_utils.py", line 167, in error_handler
    raise e.with_traceback(filtered_tb) from None
  File "/usr/local/lib/python3.12/dist-packages/tensorflow/python/framework/ops.py", line 6027, in raise_from_not_ok_status
    raise core._status_to_exception(e) from None  # pylint: disable=protected-access
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
tensorflow.python.framework.errors_impl.InvalidArgumentError: {{function_node __wrapped__StridedSlice_device_/job:localhost/replica:0/task:0/device:CPU:0}} slice index 9 of dimension 0 out of bounds. [Op:StridedSlice] name: strided_slice/

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants