Class path contains multiple SLF4J bindings

[fpoli]

In Prusti we use the Viper JARs provided by the ViperServer artifact. Recently, we started getting the following message on stdout:

SLF4J: Class path contains multiple SLF4J bindings.
SLF4J: Found binding in [jar:file:/home/runner/work/prusti-dev/prusti-dev/viper_tools/backends/silicon.jar!/org/slf4j/impl/StaticLoggerBinder.class]
SLF4J: Found binding in [jar:file:/home/runner/work/prusti-dev/prusti-dev/viper_tools/backends/ch.qos.logback.logback-classic-1.2.3.jar!/org/slf4j/impl/StaticLoggerBinder.class]
SLF4J: See http://www.slf4j.org/codes.html#multiple_bindings for an explanation.
SLF4J: Actual binding is of type [ch.qos.logback.classic.util.ContextSelectorStaticBinder]

Apparently, the same class is in multiple JARs. I suspect that this is caused by the recent changes to Viper's build system.

[aterga]

Maybe this has something to do with the Logback library used in both Silicon and ViperServer. If that's the case, something might have changed in the duplicate resolution policy of "sbt assembly", the one that's specified in ViperServer's build.sbt

[fpoli]

The problem is that both carbon.jar and silicon.jar contain all the dependencies. The dependencies are also provided as separate backends/*.jar files. This means that the ViperServer artifact contains overall three copies of all Viper dependencies.

[ArquintL]

@fpoli I'm not sure whether I understand this issue correctly. Are you saying that we should assemble just one big ViperServer.jar file and release that one (without any other jars)? And would you prefer to download the artifacts from jenkins or should we adopt a similar release mechanism as Prusti-IDE & Gobra-IDE via GitHub releases?

[fpoli]

@fpoli I'm not sure whether I understand this issue correctly. Are you saying that we should assemble just one big ViperServer.jar file and release that one (without any other jars)?

I mean that if the server is released with a folder of *.jar files (which is perfectly fine for me) then using this terminology the jars in the folder should not be "fat/uber" jars like silicon.jar and carbon.jar are, but they should be "skinny".

Releasing the server as a single "fat/uber" jar as you mentioned would also be fine for me, but to do that you would have to solve the same problem with the dependencies: Which one should end up in the final jar if both silicon.jar and carbon.jar provide it?

And would you prefer to download the artifacts from jenkins or should we adopt a similar release mechanism as Prusti-IDE & Gobra-IDE via GitHub releases?

We already download the jars from the url used by the Prusti-IDE. Having GitHub releases would work too.

[ArquintL]

I see thanks a lot for the link! So basically there should be one or more jars containing the dependencies of Silicon, Carbon, and ViperServer (such as SLF4J) and separate jars for Silicon, Carbon, and ViperServer. In particular viperserver.jar should use silicon.jar, carbon.jar, and the common dependencies and not have them directly contained in the jar.

[marcoeilers]

For what it's worth, Nagini has had this output for ages if Silicon and Carbon were both on the classpath (Nagini usually uses Silicon and Carbon fat jars, and doesn't use ViperServer). I'm fine with any solution as long as it's still possible to create Silicon and Carbon fat jars with all dependencies as before.

@fpoli Regarding the conflict resolution if ViperServer is released as one big jar file, is that not something SBT can do by default?

[ArquintL]

I tried to figure out where all the dependent jars are coming from and how I could get SBT to create these: Based on the Jenkins configs, it looks like ViperServer-nightly pulls the fat Silicon and Carbon JARs from the respective build jobs and then calls sbt publishLocal, sbt stage, and sbt assembly. The last sbt operation creates a fat ViperServer JAR, that is however ignored and not used as artifact for this job. I suspect that sbt stage creates all these JARs for (ViperServer) dependencies. target/universal/stage/lib/* is used as artifact, which includes the downloaded Silicon and Carbon fat JARs.

I currently tend to propose in the next Viper meeting to change the Viper Tools as follows:

1. We only distribute fat JARs
2. We replace the backends folder by three separate folders silicon, carbon, and viperserver each containing only a single fat JAR to avoid classpath issues. Although this results in an unnecessarily big artifact (I guess roughly as large as today), using fat JARs seems to be the preferred way for Viper clients.

To address the versioning of nightly releases that Federico would like to have, I would use (in addition to the releases done via Jenkins / our webpage) GitHub releases. Either ViperServer creates the same looking release zip containing the individual backends or each repo (Silicon, Carbon, and ViperServer) creates releases just containing its fat JAR. Thus, if you want versioning (e.g. specify a particular nightly or stable build) then you would need to switch to artifacts released on GitHub.

[aterga]

Hi all,

Couple of comments:

• Historically, we have been distributing fat JARs (called just viper.jar) with Viper IDE until we decided to switch to skinny JARs. It was easier to manage the dependencies this way.
• There's nothing inherently wrong with distributing fat JARs with the IDE, especially to the end users. However, having the ability to use the sbt stage command to obtain the skinny JARs seems useful for developers. So ideally both things should work: sbt stage and sbt assembly (the latter one producing a fat JAR).
• Skinny jars (and sbt stage) shouldn't result in duplicate dependencies. I have no idea why we include fat versions of carbon.jar and silicon.jar into the backends/ directory. I suspect it's an easy fix to not include these fat JARs. I believe sbt stage is smart enough to pick the skinny dependencies.
• Conversely, to assemble fat JARs, one needs to specify the merge strategy for possible conflicts. Take a look at this part in build.sbt: assembly / assemblyMergeStrategy. For example, we have case "logback.xml" => MergeStrategy.first which says "if we encounter that logback.xml comes from more than one dependency (i.e. both Silicon and Carbon), pick the first occurrence and ignore the consecutive ones". This strategy should work for common dependencies of Silicon and Carbon since we assume that both projects adhere to the same version of Silver, hence they must be compatible.
• To me, distributing ViperServer via GitHub seems preferable over Jenkins, so it's great that you're doing this.

[fpoli]

Is the new Github release going to fix this?

[ArquintL]

Is the new Github release going to fix this?

@fpoli yes. There are actually two fixes: Each ViperServer release has a viperserver.jar artifact that is the fat JAR of ViperServer. If you want to use skinny JARs, then viperserver-skinny-jars.zip contains all skinny JARs. This issue should no longer occur when using a fat JAR (as there is simply just 1 JAR) and as silicon.jar (i.e. the fat JAR of Silicon) is no longer included in the above mentioned zip file, it should also no longer occur when using skinny JARs.

One word of caution though: do not depend on the ViperTools artifacts that you currently see in releases. They will move to the viper-ide repo with one of the upcoming PRs