My friend and I are working on a project that generates a timetable using a Z3 solver in a mobile application. We are using heroku to host the timetable backend and we received this issue while trying to deploy the app, we got an Internal Server Error and upon checking the Heroku logs, we got the following message
2022-06-10T08:10:59.352496+00:00 app[web.1]: Scrapping Successful
2022-06-10T08:10:59.353482+00:00 app[web.1]: [2022-06-10 08:10:59,352] ERROR in app: Exception on /z3 [GET]
2022-06-10T08:10:59.353482+00:00 app[web.1]: Traceback (most recent call last):
2022-06-10T08:10:59.353483+00:00 app[web.1]: File "/app/.heroku/python/lib/python3.10/site-packages/flask/app.py", line 2077, in wsgi_app
2022-06-10T08:10:59.353483+00:00 app[web.1]: response = self.full_dispatch_request()
2022-06-10T08:10:59.353493+00:00 app[web.1]: File "/app/.heroku/python/lib/python3.10/site-packages/flask/app.py", line 1525, in full_dispatch_request
2022-06-10T08:10:59.353494+00:00 app[web.1]: rv = self.handle_user_exception(e)
2022-06-10T08:10:59.353494+00:00 app[web.1]: File "/app/.heroku/python/lib/python3.10/site-packages/flask/app.py", line 1523, in full_dispatch_request
2022-06-10T08:10:59.353494+00:00 app[web.1]: rv = self.dispatch_request()
2022-06-10T08:10:59.353494+00:00 app[web.1]: File "/app/.heroku/python/lib/python3.10/site-packages/flask/app.py", line 1509, in dispatch_request
2022-06-10T08:10:59.353495+00:00 app[web.1]: return self.ensure_sync(self.view_functions[rule.endpoint])(**req.view_args)
2022-06-10T08:10:59.353495+00:00 app[web.1]: File "/app/TimetableZ3run.py", line 18, in show_z3_stuff
2022-06-10T08:10:59.353496+00:00 app[web.1]: timetable = TimeTableSchedulerZ3(scrapper.semesterProcessed, print=True)
2022-06-10T08:10:59.353496+00:00 app[web.1]: File "/app/timetableZ3.py", line 19, in __init__
2022-06-10T08:10:59.353497+00:00 app[web.1]: self.solver = Solver()
2022-06-10T08:10:59.353497+00:00 app[web.1]: NameError: name 'Solver' is not defined
We did install z3-solver and the build logs in heroku showed that it was successful
Building wheels for collected packages: z3
Building wheel for z3 (setup.py): started
Building wheel for z3 (setup.py): finished with status 'done'
Created wheel for z3: filename=z3-0.2.0-py3-none-any.whl size=26638 sha256=26c16f763a170cbdac5f5f86211e524db2dc7cc786b10c04f8ed66a46b836602
Stored in directory: /tmp/pip-ephem-wheel-cache-wz59cycx/wheels/5a/b2/60/55b07a5084cad7ab411e395fb1440a2b1a19598bff535a3955
Successfully built z3
Installing collected packages: z3-solver, certifi, boto, z3, Werkzeug, urllib3, numpy, MarkupSafe, itsdangerous, idna, gunicorn, click, charset-normalizer, requests, Jinja2, Flask
Successfully installed Flask-2.1.2 Jinja2-3.1.2 MarkupSafe-2.1.1 Werkzeug-2.1.2 boto-2.49.0 certifi-2021.10.8 charset-normalizer-2.0.12 click-8.1.3 gunicorn-20.1.0 idna-3.3 itsdangerous-2.1.2 numpy-1.21.4 requests-2.27.1 urllib3-1.26.9 z3-0.2.0 z3-solver-4.8.17.0
-----> Discovering process types
Procfile declares types -> web
-----> Compressing...
Done: 94.6M
We managed to get it working locally with just from z3 import * but it is facing the abovementioned issue when deployed to heroku. When checking the slug in Heroku, we do find the Solver class in z3.py which we found it puzzling because we would have expected it to be imported and work. We also tried from from z3 import Solver and import z3. These all work locally as well, but not on Heroku.
Would really appreciate the help and guidance on this issue. Thank you!
Some other background info :
We used flask as a backend.
The Heroku slug contained z3, z3-0.2.0.dist-info and z3_solver-4.8.17.0.dist-info folders under /app/.heroku/python/lib/python3.10/site-packages.