Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

reinstate z3 package from @Drup with a stable release #10815

Closed
wants to merge 2 commits into from

Conversation

c-cube
Copy link
Contributor

@c-cube c-cube commented Nov 22, 2017

Trying to resurrect the package for Z3 and its OCaml bindings.

Previously:

Licensing problems should be gone, since Z3 is now under MIT. I added a package for the last release and the dev-repo field.

@camelus
Copy link
Contributor

camelus commented Nov 22, 2017

✅ All lint checks passed 894b545
  • These packages passed lint tests: Z3.4.5.0

✅ Installability check (7787 → 7788)
  • new installable packages (1): Z3.4.5.0

@c-cube
Copy link
Contributor Author

c-cube commented Nov 22, 2017

I don't get why the datakit tests fail so fast, and I don't know how to access the error files to check why…

@c-cube
Copy link
Contributor Author

c-cube commented Nov 22, 2017

Not sure what's wrong exactly…

@kit-ty-kate
Copy link
Member

On MacOS X, Travis fails with:

#=== ERROR while installing Z3.4.5.0 ==========================================#
Some files in ~/.opam/system/install/Z3.install couldn't be installed:
  - /Users/travis/.opam/system/build/Z3.4.5.0/build/libz3.so to /Users/travis/.opam/system/lib/Z3

@c-cube
Copy link
Contributor Author

c-cube commented Nov 23, 2017

Ah, yeah, the .install written by @Drup might be linux-specific :-(
But there are also weird failures on some specific linux distributions


messages: [
"Before installing any package depending on Z3, please export the following variable:
export LD_LIBRARY_PATH=\"$(ocamlfind printconf destdir)/stublibs:${LD_LIBRARY_PATH}\""
Copy link
Contributor

Choose a reason for hiding this comment

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

Did you try to get rid of that ? I feel like this is not really acceptable if it gets into opam's main repository.

Copy link
Member

Choose a reason for hiding this comment

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

It would be good to get rid of this, indeed. Why is it needed?

Copy link
Contributor

Choose a reason for hiding this comment

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

At the time, it was needed because the package recompile Z3 entirely, Z3's build system was complicated and because I'm not very good at C(++) linking rules.
Now, I think it would be better to rely on system-provided .so/.h files, but it needs modifying Z3's build system or just plain extracting the OCaml part, and building it outside.
opam's LLVM package does the former, so I guess it works.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

modifying Z3's build system? :-/
this sounds super awful…

@gasche
Copy link
Member

gasche commented Dec 10, 2017

Ping. Do we have a chance to have a nice solution this time around? (I think many people would be interested in having an easy way to use Z3 using opam.) If not, we may want to close the PR.

@c-cube
Copy link
Contributor Author

c-cube commented Dec 10, 2017

Sorry I haven't updated this. I don't know of a solution that would be simple enough (building manually seems a bit too scary, especially when Z3 maintainers themselves are moving to cmake).

So I'm closing this until a better, cleaner solution is found…

@c-cube c-cube closed this Dec 10, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

6 participants