search

usi-verification-and-security / opensmt

The opensmt solver
Other
76 stars 18 forks source link

Update the circleci image for `build-recent` #558

Closed aehyvari closed 2 years ago

aehyvari commented 2 years ago

Our CI is currently using a deprecated tag stable for a relatively recent ubuntu distribution cimg/base in CircleCI. The tag should be cimg/base:current.

At the moment, updating the tag breaks pysmt installation in a non-trivial way. First, for yet unknown reason pysmt complains about a missing directory. This seems to be fixable with the following patch on pysmt:

index d15bb7b..5186711 100644
--- a/pysmt/smtlib/parser/__init__.py
+++ b/pysmt/smtlib/parser/__init__.py
@@ -87,7 +87,7 @@ else:
     build_dir = os.path.join(os.path.expanduser('~'), '.pyxbld')
     path = os.path.join(os.path.dirname(__file__), "parser.py")
     name="pysmt.smtlib.parser.parser"
-
+    os.makedirs(path)
     so_path = pyximport.build_module(name, path,
                                      pyxbuild_dir=build_dir)
     mod = imp.load_dynamic(name, so_path)

Second, after this fix, pysmt complains about an unfound module with the following trace.

  File "ModelValidator.py", line 5, in <module>
  File "PyInstaller/loader/pyimod02_importers.py", line 499, in exec_module
  File "pysmt/shortcuts.py", line 38, in <module>
  File "PyInstaller/loader/pyimod02_importers.py", line 499, in exec_module
  File "pysmt/smtlib/parser/__init__.py", line 91, in <module>
  File "pyximport/pyximport.py", line 179, in build_module
  File "pyximport/pyximport.py", line 104, in get_distutils_extension
  File "_distutils_hack/__init__.py", line 92, in create_module
  File "importlib/__init__.py", line 126, in import_module
  File "PyInstaller/loader/pyimod02_importers.py", line 499, in exec_module
  File "setuptools/__init__.py", line 10, in <module>
  File "_distutils_hack/__init__.py", line 92, in create_module
  File "importlib/__init__.py", line 126, in import_module
ModuleNotFoundError: No module named 'setuptools._distutils'
aehyvari commented 2 years ago

One way forward would be to use Dolmen for checking. https://github.com/Gbury/dolmen

aehyvari commented 2 years ago

We are now using dolmen and pySMT for model validation. The issue is closed by #559 and #561.