Z3Prover / z3

The Z3 Theorem Prover
Other
10.36k stars 1.48k forks source link

about the maven dependence,can not run normal #1421

Open GOGJIAN opened 6 years ago

GOGJIAN commented 6 years ago

I use the maven add this dependence `

org.sosy-lab
      <artifactId>javasmt-solver-z3</artifactId>
      <version>z3-4.4.1-1558-gf96cfea</version>
  </dependency>`

use the function of examples like this: `public void simpleExample() {

    System.out.println("SimpleExample");
    try {
        Log.open("SimpleExample");
        Log.append("SimpleExample");
    }catch (Exception e){
        e.printStackTrace();
    }finally{
        Log.close();
    }

    {
        Context ctx = new Context();
        /* do something with the context */

        /* be kind to dispose manually and not wait for the GC. */
        ctx.close();
    }
}`

about the Native.java
report the error:java.lang.NoClassDefFoundError: Could not initialize class com.microsoft.z3.Native I don't know how to deal with the error。 please help me,thank you

wintersteiger commented 6 years ago

This sounds like a problem with a Maven package. The problem is almost surely that your system cannot find libz3.so/.dylib/.dll at runtime, which is either because some of the paths are not set up correctly, or there is a mismatch between your system bitness (32/64 bit) and Z3. We do not manage that entry in Maven, however.

@cheshire: Is it correct that you are the maintainer of the Z3 entry at mvnrepository.com? If so, could you advise? Also, there's a typo in my name in there, but ideally I don't want to be listed as a contact at all as I don't/can't maintain those packages.

cheshire commented 6 years ago

@GOGJIAN the package only provides the binaries for 64 bit Linux, are you on that platform? @wintersteiger I had setup that package, yes, but unfortunately I can not maintain it at the moment. We can explore a number of options here:

dah-fari7009 commented 4 years ago

Hello, I just wanted to know if you ever found a solution to this issue

NikolajBjorner commented 4 years ago

There is no support for Maven related issues. But you are invited to submit a solution.

sequencer commented 4 years ago

If providing a build system wrapper to CMake like sbt/mill, would it be possible to PR this wrapper, making it possible to give a Maven release? Or if not possible, would it be possible to release a jar in GitHub release, so that we can download this jar from official release.

NikolajBjorner commented 4 years ago

Sure, the azure-pipelines.yml script runs builds on checkins and the "release.yml" and "nightly.yml" publish packages. If you have a packaging solution it should be possible to add it to these pipelines through a pull request.

NikolajBjorner commented 3 years ago

@sequencer - do you have a pull request on your Maven wrapper?

sequencer commented 3 years ago

Sorry for the delay, I'm totally missed this notification. I think z3/src/api/java/CMakeLists.txt needs some rework, using standard java specified build system to manage the java code, and use the plugin to publish it. I'm a Scala guy, so only familiar with sbt and mill, not sure are these tool acceptable by upstream.

NikolajBjorner commented 3 years ago

A rule of thumb for acceptable tools for upstream are the ones listed as already included in packages: https://docs.microsoft.com/en-us/azure/devops/pipelines/agents/hosted?view=azure-devops&tabs=yaml For example, I see sbt. Adding other goodies is less easy. For example, Z3 releases ocaml bindings but the Windows support for ocaml was never on par with Linux/BSD and it is additional friction every time I have to touch the ML bindings.