Comments (10)
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
from viperserver.
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
from viperserver.
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.
from viperserver.
@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?
from viperserver.
@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.
from viperserver.
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.
from viperserver.
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?
from viperserver.
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:
- We only distribute fat JARs
- We replace the
backends
folder by three separate folderssilicon
,carbon
, andviperserver
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.
from viperserver.
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
andsbt 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 believesbt 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 havecase "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.
from viperserver.
Is the new Github release going to fix this?
from viperserver.
Related Issues (20)
- Carbon doesn't seem to initialise correctly if paths contain whitespace HOT 7
- Minor: change exception reports to include runnable commands/quoted paths
- Cache does not seem to be initialized HOT 2
- Streaming messages from ViperCoreServer HOT 8
- VerificationWorker should add option --ignoreFile before calling method prepare of SilFrontend HOT 1
- Plugin input with `--plugin` in `customArguments` does not work
- Cannot find file HOT 3
- Some plugin interactions seem to be broken in ViperServer HOT 1
- Move code computing program statistics to Silver. HOT 1
- Minimal ViperConfig for ViperCoreServer
- Wrong error reported when cached HOT 1
- Some regression tests are halting HOT 3
- Revisit the CI HOT 2
- Port Viper IDE to the LSP frontend of ViperServer
- Review the implementation of MessageStreamingTask.enqueueMessage HOT 1
- CI Failure with JDK 15 HOT 2
- Caching swallows counterexamples
- Domain Ordering
- Dependencies update in Viper Server HOT 8
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from viperserver.