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

Add a Snapcraft Build and Snap Install Instructions #1639

Merged
merged 3 commits into from
Jan 28, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -118,6 +118,20 @@ If you have access to a remote machine over SSH, this is the recommended way to
Github Codespaces
To allow running Stainless with only a browser, we have provided a sample repository to use Stainless with Github Codespaces. Github Codespaces are cloud machines that can be access via Visual Studio Code locally or in the browser. In our experience (as of October 2023), this flow works well, given the provided Ubuntu Linux virtual machines with 16GB of RAM and substantial processing power. Please see [this repository](https://github.com/samuelchassot/Stainless-codespaces) for further details.

### Snap Store

A package for Stainless is available on the Snap store as [`stainless`](https://snapcraft.io/stainless) with an experimental edge release. It can be used to install and run Stainless on any Snap enabled system (e.g. Ubuntu).

In a terminal, you can type:

```shell
sudo snap install stainless --edge
```

This exposes two commands, the tool `stainless`, as well as `stainless.cli`, running `scala-cli` with Stainless libraries loaded.

Running the commands the first time may take some time as some Scala libraries are downloaded.

### Arch User Repository

A package for Stainless is available on the Arch User Repository (AUR) for ArchLinux as [`stainless-git`](https://aur.archlinux.org/packages/stainless-git), which follows the latest commit on the `main` branch.
Expand Down
5 changes: 5 additions & 0 deletions snap/local/stainless
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
#!/bin/sh

export HOME=$SNAP_USER_DATA

java -jar -Duser.home=$SNAP_USER_DATA $SNAP/usr/share/java/stainless/stainless.jar $@
14 changes: 14 additions & 0 deletions snap/local/stainless-cli
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
#!/bin/sh

set -e

export HOME=$SNAP_USER_DATA
export SCALA_CLI_ROOT="$SNAP/usr/share/java/scala-cli"
export STAINLESS_LIB="$SNAP/usr/lib/stainless"

export SCALA_VER=3.5.2

export STAINLESS_SOURCES="$STAINLESS_LIB/stainless-library.jar"

java -jar -Duser.home=$SNAP_USER_DATA $SCALA_CLI_ROOT/scala-cli.jar -S $SCALA_VER --jar $STAINLESS_SOURCES $@

88 changes: 88 additions & 0 deletions snap/snapcraft.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,88 @@
title: Stainless
name: stainless
version: git # set corrrectly by `override-prime`
summary: Program verifier and model checker for Scala 3
description: |
Stainless is a program verifier and counterexample finder for Scala 3. It uses
SMT solvers (z3, cvc5, princess), function unfolding, and invariant inference to
prove and disprove program safety and termination.
website: https://github.com/epfl-lara/stainless
source-code: https://github.com/epfl-lara/stainless
license: Apache-2.0

# build metadata and dependencies
type: app
base: core24
adopt-info: stainless # the build part `stainless` below
platforms:
amd64:

grade: devel
confinement: strict

# exposed commands and what they refer to internally
apps:
stainless:
command: stainless
plugs: [home]
environment:
JAVA_HOME: $SNAP/usr/lib/jvm/java-17-openjdk-amd64
PATH: $JAVA_HOME/bin:$PATH
cli:
command: stainless-cli
plugs: [home, network, network-bind]
environment:
JAVA_HOME: $SNAP/usr/lib/jvm/java-17-openjdk-amd64
PATH: $JAVA_HOME/bin:$PATH

# actual build
parts:
wrapper:
plugin: dump
source: snap/local
source-type: local

scala-cli:
plugin: nil
override-pull: |
wget -c https://github.com/VirtusLab/scala-cli/releases/download/v1.6.1/scala-cli.jar
override-build: |
install -Dm644 scala-cli.jar "$CRAFT_PART_INSTALL/usr/share/java/scala-cli/scala-cli.jar"

stainless:
plugin: nil
source: https://github.com/epfl-lara/stainless.git
source-branch: main
source-type: git

build-packages: [git, wget, unzip, openjdk-17-jdk]
stage-packages: [openjdk-17-jre-headless, z3, cvc5]

override-pull: |
craftctl default

# just need a recent enough version of sbt to kickstart the build
wget -c https://github.com/sbt/sbt/releases/download/v1.10.7/sbt-1.10.7.zip
unzip sbt-1.10.7.zip

override-build: |
./sbt/bin/sbt universal:stage # make sure stainless-library jars are compiled
./sbt/bin/sbt assembly # pack uber jars

# set snap package version
craftctl set version="$(git describe --long | sed 's/\([^-]*-\)g/r\1/;s/-/./g')"

SCALA_VER="$(grep "val stainlessScalaVersion = " build.sbt | awk '{gsub(/"/, "", $4); print $4}')" # get scala version from build, remove quotes
STAINLESS_VER="$(git describe --abbrev=7 | sed 's/^v//')" # trim and strip v from git versioning e.g. v0.9.1... -> 0.9.1...

mkdir -p $CRAFT_PART_INSTALL/usr/share/java/stainless
cp "./frontends/dotty/target/scala-$SCALA_VER/stainless-dotty-assembly-$STAINLESS_VER.jar" stainless.jar

cp "./frontends/library/target/scala-3.5.2/stainless-library_3-$STAINLESS_VER.jar" stainless-library.jar
cp "./frontends/library/target/scala-3.5.2/stainless-library_3-$STAINLESS_VER-sources.jar" stainless-library-sources.jar

install -Dm644 stainless.jar "$CRAFT_PART_INSTALL/usr/share/java/stainless/stainless.jar"
install -Dm644 stainless-library.jar "$CRAFT_PART_INSTALL/usr/lib/stainless/stainless-library.jar"
install -Dm644 stainless-library-sources.jar "$CRAFT_PART_INSTALL/usr/lib/stainless/stainless-library-sources.jar"
install -Dm644 LICENSE "$CRAFT_PART_INSTALL/usr/share/licenses/stainless/LICENSE"