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

Update to master #1411

Closed
wants to merge 17 commits into from
Closed
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
25 changes: 14 additions & 11 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ on:
workflow_dispatch:

env:
SOLVER_PKG_VERSION: "snapshot-20220721"
SOLVER_PKG_VERSION: "snapshot-20220812"
# The CACHE_VERSION can be updated to force the use of a new cache if
# the current cache contents become corrupted/invalid. This can
# sometimes happen when (for example) the OS version is changed but
Expand All @@ -20,7 +20,7 @@ env:

jobs:
config:
runs-on: ubuntu-20.04
runs-on: ubuntu-22.04
outputs:
name: ${{ steps.config.outputs.name }}
version: ${{ steps.config.outputs.version }}
Expand Down Expand Up @@ -58,20 +58,20 @@ jobs:
strategy:
fail-fast: false
matrix:
os: [ubuntu-20.04, macos-12, windows-2019]
ghc-version: ["8.8.4", "8.10.7", "9.0.2", "9.2.2"]
os: [ubuntu-22.04, macos-12, windows-2019]
ghc-version: ["8.8.4", "8.10.7", "9.0.2", "9.2.4"]
exclude:
# https://gitlab.haskell.org/ghc/ghc/-/issues/18550
- os: windows-2019
ghc-version: 8.10.7
- os: windows-2019
ghc-version: 9.0.2
- os: windows-2019
ghc-version: 9.2.2
ghc-version: 9.2.4
include:
# We include one job from an older Ubuntu LTS release to increase our
# coverage of possible Linux configurations.
- os: ubuntu-18.04
- os: ubuntu-22.04
ghc-version: 8.8.4
outputs:
test-lib-json: ${{ steps.test-lib.outputs.targets-json }}
Expand Down Expand Up @@ -147,6 +147,8 @@ jobs:
cmd="cat \$1.stdout"
if ${{ runner.os == 'Windows' }}; then
cmd="cat \$1.stdout.mingw32 2>/dev/null || $cmd"
elif ${{ runner.os == 'macOS' }}; then
cmd="cat \$1.stdout.darwin 2>/dev/null || $cmd"
fi
./bin/test-runner --ext=.icry -r ./output --exe=$(which bash) -F -c -F "$cmd" -F -- ./tests
TARGETS_JSON=$(echo -n "$(ls -1 ./output/tests)" | jq -Rsc 'split("\n")')
Expand All @@ -158,7 +160,7 @@ jobs:
- if: runner.os == 'Windows'
run: .github/wix.ps1

- if: runner.os == 'Windows'
- if: runner.os == 'Windows' && github.event.pull_request.head.repo.fork == false
shell: bash
env:
SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }}
Expand All @@ -181,7 +183,8 @@ jobs:
env:
OS_TAG: ${{ matrix.os }}

- shell: bash
- if: github.event.pull_request.head.repo.fork == false
shell: bash
env:
SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }}
SIGNING_KEY: ${{ secrets.SIGNING_KEY }}
Expand Down Expand Up @@ -231,12 +234,12 @@ jobs:
matrix:
suite: [test-lib]
target: ${{ fromJson(needs.build.outputs.test-lib-json) }}
os: [ubuntu-20.04, macos-12, windows-2019]
os: [ubuntu-22.04, macos-12, windows-2019]
continue-on-error: [false]
include:
- suite: rpc
target: ''
os: ubuntu-20.04
os: ubuntu-22.04
continue-on-error: false
#- suite: rpc
# target: ''
Expand Down Expand Up @@ -311,7 +314,7 @@ jobs:
cryptol-remote-api/run_rpc_tests.sh

build-push-image:
runs-on: ubuntu-20.04
runs-on: ubuntu-22.04
needs: [config]
if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' || needs.config.outputs.release == 'true'
strategy:
Expand Down
27 changes: 21 additions & 6 deletions Dockerfile
Original file line number Diff line number Diff line change
@@ -1,21 +1,36 @@
FROM haskell:8.8.4 AS build
FROM ubuntu:22.04 AS build

RUN apt-get update && apt-get install -y libncurses-dev unzip
RUN apt-get update && \
apt-get install -y \
# ghcup requirements
build-essential curl libffi-dev libffi8 libgmp-dev libgmp10 libncurses-dev libncurses6 libtinfo6 \
# Cryptol dependencies
zlib1g-dev \
# Miscellaneous
unzip
RUN useradd -m cryptol
COPY --chown=cryptol:cryptol . /cryptol
USER cryptol
WORKDIR /cryptol
RUN mkdir -p rootfs/usr/local/bin
WORKDIR /cryptol/rootfs/usr/local/bin
RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220114/ubuntu-18.04-bin.zip"
RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220812/ubuntu-22.04-bin.zip"
RUN unzip solvers.zip && rm solvers.zip && chmod +x *
WORKDIR /cryptol
ENV PATH=/cryptol/rootfs/usr/local/bin:$PATH
ENV PATH=/cryptol/rootfs/usr/local/bin:/home/cryptol/.local/bin:/home/cryptol/.ghcup/bin:$PATH
RUN z3 --version
ARG CRYPTOLPATH="/cryptol/.cryptol"
ENV LANG=C.UTF-8 \
LC_ALL=C.UTF-8
COPY cabal.GHC-8.8.4.config cabal.project.freeze
RUN mkdir -p /home/cryptol/.local/bin && \
curl -L https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7 -o /home/cryptol/.local/bin/ghcup && \
chmod +x /home/cryptol/.local/bin/ghcup
RUN mkdir -p /home/cryptol/.ghcup && \
ghcup --version && \
ghcup install cabal 3.6.2.0 && \
ghcup install ghc 8.8.4 && \
ghcup set ghc 8.8.4
RUN cabal v2-update && \
cabal v2-build -j cryptol:exe:cryptol && \
cp $(cabal v2-exec which cryptol) rootfs/usr/local/bin && \
Expand All @@ -33,9 +48,9 @@ RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
USER root
RUN chown -R root:root /cryptol/rootfs

FROM debian:buster-20210511-slim
FROM ubuntu:22.04
RUN apt-get update \
&& apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 \
&& apt-get install -y libgmp10 libgomp1 libffi8 libncurses6 libtinfo6 libreadline8 \
&& apt-get clean && rm -rf /var/lib/apt/lists/*
RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol
COPY --from=build /cryptol/rootfs /
Expand Down
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ Cryptol currently uses Microsoft Research's [Z3 SMT
solver](https://github.com/Z3Prover/z3) by default to solve constraints
during type checking, and as the default solver for the `:sat` and
`:prove` commands. Cryptol generally requires the most recent version
of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20220721).
of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20220812).

You can download Z3 binaries for a variety of platforms from their
[releases page](https://github.com/Z3Prover/z3/releases). If you
Expand Down Expand Up @@ -75,15 +75,15 @@ Cryptol builds and runs on various flavors of Linux, Mac OS X, and
Windows. We regularly build and test it in the following environments:

- macOS 12, 64-bit
- Ubuntu 18.04, 64-bit
- Ubuntu 20.04, 64-bit
- Ubuntu 22.04, 64-bit
- Windows Server 2019, 64-bit

## Prerequisites

Cryptol is regularly built and tested with the three most recent
versions of GHC, which at the time of this writing are 8.10.7, 9.0.2, and
9.2.2. The easiest way to install an approporiate version of GHC is
9.2.4. The easiest way to install an approporiate version of GHC is
with [ghcup](https://www.haskell.org/ghcup/).

Some supporting non-Haskell libraries are required to build
Expand Down
Loading