search

viperproject / viperserver

HTTP server that manages verification requests to different tools from the Viper tool stack.
Other
10 stars 17 forks source link

Dependencies update in Viper Server #8

Closed viper-admin closed 4 years ago

viper-admin commented 6 years ago

Pull request :twisted_rightwards_arrows: created by @fabiopakk on 2018-10-31 15:45 Last updated on 2019-01-29 14:47 Original Bitbucket pull request id: 8

Participants:

  • @alexanderjsummers (reviewer)
  • @aterga (reviewer)
  • @mschwerhoff (reviewer) :heavy_check_mark:
  • @fabiopakk

Source: https://github.com/viperproject/viperserver/commit/5beaf1a14e3d9edce2e979f2684e3cf499de1a46 on branch fabiopakk_dependencies_update Destination: https://github.com/viperproject/viperserver/commit/9d5937d4a56be1101a744476bae079fde9f95abe on branch master Marge commit: https://github.com/viperproject/viperserver/commit/9145a09eff6863e805fbc7329930b3359eb6c9a3

State: MERGED

viper-admin commented 5 years ago

@mschwerhoff approved :heavy_check_mark: the pull request on 2018-11-05 13:55

viper-admin commented 5 years ago

@aterga commented on 2018-11-08 15:45

Location: project/plugins.sbt

sbt-native-packager is needed to enable “sbt stage” that produces fine-grained JAR files for the entire project and its dependencies. We distribute those via Viper IDE. For more details, see https://www.scala-sbt.org/sbt-native-packager/gettingstarted.html

viper-admin commented 5 years ago

@fabiopakk commented on 2018-11-09 14:14

Location: project/plugins.sbt

sbt-native-packager is needed to enable “sbt stage” that produces fine-grained JAR files for the entire project and its dependencies. We distribute those via Viper IDE. For more details, see https://www.scala-sbt.org/sbt-native-packager/gettingstarted.html

Update: added plugin and loaded it in build.sbt. sbt stage is now supported.

viper-admin commented 5 years ago

@aterga commented on 2018-11-15 14:46

I see that the build succeeds on the build server. However, when I try locally running `sbt assembly` I get compilation errors, e.g.,

[error] /private/tmp/viper-server-pull-request-for-fabio/viperserver/src/main/scala/viper/server/VerificationWorker.scala:361:29: not found: type Method

I have silver, silicon, carbon, viperserver all on the same level.

viper-admin commented 5 years ago

@fabiopakk commented on 2018-11-16 09:03

Perhaps a wrong branch in one of the repos? Also a good idea to remove all ‘target' directories for a clean build.

viper-admin commented 5 years ago

@alexanderjsummers commented on 2019-01-28 20:40

Hi all,

I also can’t compile locally. I have tried both this version and the latest version in the branch. In both cases, there still seem to be dependencies on local directory copies of the dependencies and/or folders created by the build itself. I have tried cleaning everything, including manually removing all created directories.

I would really like to have a version of the build which collects the artifacts on the build server from the latest builds; there are bug fixes that we need for our current work, but I can’t make use of them in the IDE.

Cheers, Alex

viper-admin commented 5 years ago

@aterga commented on 2019-01-28 21:56

I managed to assemble and run ViperServer from this branch. I think we can proceed with merging this in for now, because there are urgent Viper fixes that the IDE users need to receive soon.

On a side note, it took many steps to get the project to compile, most of which feel redundant.

  1. sbt assembly in ./silver
  2. ln -s ../silver/ silver in ./carbon
  3. sbt assembly in ./carbon
  4. ln -s ../silver/ silver in ./silicon
  5. sbt assembly in ./silicon
  6. ln -s ../silver/ silver in ./viperserver
  7. ln -s ../carbon/ carbon in ./viperserver
  8. ln -s ../silicon/ silicon in ./viperserver
  9. Finally, sbt stage in ./viperserver

If I accidentally forget about one of these steps and run sbt stage right away, I would need to know that ln -s ... will silently fail to create a link since a directory with that name already exists, and the build will fail.

If there is a good reason why all these steps cannot be lifted or automated, then at least we should carefully document them (currently, the docs seem incomplete).

However, I think that we discussed that we cannot use this SBT build approach in the long run. If compilation of ViperServer depends on fat JARs of sub-projects, then how do we make sure that those projects (carbon, silicon) were compiled for the same version of Silver?

viper-admin commented 5 years ago

@fabiopakk commented on 2019-01-29 14:47

Gentlemen,

From README.MD you have (Windows session):

  1. mklink /D silver
  2. mklink /D silicon
  3. mklink /D carbon
  4. sbt compile // could also be sbt stage

Of course steps 1, 2 and 3 need only to be done once. After that, sbt stage is all you need. There's no need for intermediary sbt assembly, the point is that SBT will figure it out and do everything that is necessary, provided it knows where everything is and the dependencies' respective instructions. To know where the dependencies live, today’s SBT needs symbolic links. After that, SBT can find all build.sbt files it needs and figures the intermediary steps (and the sequence of steps as well), so that all you need to type is the last SBT command you have in mind.

I suppose here that silver, carbon and silicon were installed following their own instructions in Readme.rst or Readme.md, which were updated.

@alexanderjsummers , if want to get specific jar files from Jenkings instead of compiling from source, you can. You must place jar files in the lib directory. The build.sbt files of all projects must be accessible, though. I suggest using a scheme such as the following build jobs: silicon, carbon and ViperServer. Let me know if need instructions on how to do that.

Regards,

Fábio