From 2f4684c8afa5a82c9f3028690e285e009d221b46 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 14 Jul 2020 10:58:38 -0700 Subject: [PATCH] Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807. --- .appveyor.yml | 26 ----- .travis.yml | 43 -------- CONTRIBUTING.md | 73 +++--------- Dockerfile | 85 +++++++------- LICENSE | 2 +- LICENSE.rtf | 2 +- Makefile | 287 ------------------------------------------------ README.md | 118 ++++++++++---------- cry | 3 +- 9 files changed, 119 insertions(+), 520 deletions(-) delete mode 100644 .appveyor.yml delete mode 100644 .travis.yml delete mode 100644 Makefile diff --git a/.appveyor.yml b/.appveyor.yml deleted file mode 100644 index e6efb303..00000000 --- a/.appveyor.yml +++ /dev/null @@ -1,26 +0,0 @@ -environment: - matrix: - - GHC_VERSION: 8.4.4 - - GHC_VERSION: 8.6.5 - - GHC_VERSION: 8.8.3 - -install: - # Using '-y' and 'refreshenv' as a workaround to: - # https://github.com/haskell/cabal/issues/3687 - - choco install -y ghc --version %GHC_VERSION% - - refreshenv - # See http://help.appveyor.com/discussions/problems/6312-curl-command-not-found#comment_42195491 - # NB: Do this after refreshenv, otherwise it will be clobbered! - - set PATH=C:\Program Files\Git\mingw64\bin;%PATH%;C:\msys64\usr\bin;%APPVEYOR_BUILD_FOLDER%\bin - - curl -o z3.zip -L https://github.com/Z3Prover/z3/releases/download/z3-4.7.1/z3-4.7.1-x64-win.zip - - 7z x -bd z3.zip - - mkdir %APPVEYOR_BUILD_FOLDER%\bin - - cp z3-4.7.1-x64-win/bin/z3.exe %APPVEYOR_BUILD_FOLDER%\bin - -build_script: - - git submodule update --init - #- cp cabal.GHC-%GHC_VERSION%.config cabal.project.freeze - - cabal v2-update - - cabal v2-configure --allow-newer - - bash cry build - - bash cry test diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index 6517ba9b..00000000 --- a/.travis.yml +++ /dev/null @@ -1,43 +0,0 @@ -dist: trusty -sudo: false - -language: c - -cache: - directories: - - $HOME/.ghc - - $HOME/.cabal - -matrix: - include: - - env: CABALVER="3.0" GHCVER="8.4.4" - compiler: ": #GHC 8.4.4" - addons: {apt: {packages: [cabal-install-3.0,ghc-8.4.4], sources: [hvr-ghc]}} - - env: CABALVER="3.0" GHCVER="8.6.5" - compiler: ": #GHC 8.6.5" - addons: {apt: {packages: [cabal-install-3.0,ghc-8.6.5], sources: [hvr-ghc]}} - - env: CABALVER="3.0" GHCVER="8.8.3" - compiler: ": #GHC 8.8.3" - addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.3], sources: [hvr-ghc]}} - -before_install: - - if [[ $TRAVIS_OS_NAME == 'linux' ]]; - then - mkdir -p $HOME/bin; - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$HOME/bin:$HOME/.cabal/bin:$PATH; - curl https://saw.galois.com/builds/z3/z3 > z3; - chmod +x z3; - mv z3 $HOME/bin/z3; - z3 --version; - fi - - env - -script: - - cp cabal.GHC-${GHCVER}.config cabal.project.freeze - - cabal update - - cabal v2-configure --allow-newer - - bash cry build - - bash cry test - -notifications: - email: false diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 622932c5..37974454 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -28,39 +28,20 @@ check the output against an expected output file. We make at least one test for each new issue, and keep the accumulated tests in our suite as regression tests. The test suite itself is written using the `test-framework` library, so it can readily output XML for consumption -by Jenkins and other CI systems. - -## Stackage - -On the Jenkins machines, we `cp cabal.GHCNNN.config cabal.config` -before building in order to build against a Stackage LTS snapshot -(updated periodically). This is to ensure compatibility with -downstream dependencies that rely on Stackage for their stability. We -do not have `cabal.config` in place by default, though, so developers -can use different versions of the compiler. +by CI systems. ## Running tests -To run the test suite, run `make test` from the root of the +To run the test suite, run `./cry test` from the root of the repository. By default, you'll get output on the console for each test that fails, either with an explanation for why it failed, or a command line you can paste in order to compare the test results against the expected output. -The `make test` target invokes the `cryptol-test-runner` executable, +The `./cry test` command invokes the `cryptol-test-runner` executable, which is defined in the `/tests/` directory. It is invoked with the location of the `cryptol` executable, an output directory, and -standard `test-framework` command line arguments. The `test` target in -the `Makefile` provides a template for how to invoke it if you need to -use advanced parameters. - -## Running benchmarks - -To run the benchmark suite, run `make bench` from the root of the -repository. By default, you'll get Criterion output on the console -from the benchmarking executable in `/bench`. The easiest way to pass -custom arguments to this executable is to run the suite subsequently -with `cabal bench --benchmark-options="..."`. +standard `test-framework` command line arguments. ## Creaing a new test @@ -149,11 +130,11 @@ look as expected, and then save those results as the new `.icry.stdout`: # start with a fresh build - % make + % ./cry build ... # tests are run from within the directory of the .icry file % cd tests/issues - % ../../.cabal-sandbox/bin/cryptol -b issue006.icry + % ../../bin/cryptol -b issue006.icry Loading module Cryptol Loading module Cryptol Loading module Main @@ -169,7 +150,7 @@ script. Since the results looked correct, we piped the same command into the matching `.icry.stdout` file and removed the `.icry.fails` file: - % ../../.cabal-sandbox/bin/cryptol -b issue006.icry.stdout + % ../../bin/cryptol -b issue006.icry.stdout % rm issue006.icry.fails Now the test case `issue006` passes, and will (hopefully!) break if @@ -182,9 +163,6 @@ The top-level repository directories are: - `/bench`: Benchmarking executable and suite - `/cryptol`: Haskell sources for the front-end `cryptol` executable and read-eval-print loop -- `/cryptol-server`: Experimental Cryptol JSON-over-ZeroMQ server, - currently built to support - [pycryptol](http://pycryptol.readthedocs.org/en/latest/) - `/docs`: LaTeX and Markdown sources for the Cryptol documentation - `/examples`: Cryptol sources implementing several interesting algorithms @@ -217,15 +195,15 @@ for branches and merging. Our version has two notable differences: In short: - Any substantial new features should be developed on a branch - prefixed with `feature/`, and then merged into `master` when + prefixed with `feature-`, and then merged into `master` when completed. - When we reach a feature freeze for a release, we create a new branch - prefixed with `release/`, for example `release/2.1.0`. When the + prefixed with `release-`, for example `release-2.1.0`. When the release is made, we merge those changes back into `master` and make a snapshot commit on the `release` branch. - If a critical bug emerges in already-released software, we create a branch off of the relevant `release` branch commit prefixed with - `hotfix/2.1.1`. When the hotfix is complete, we merge those changes + `hotfix-`. When the hotfix is complete, we merge those changes back into `master` and make a snapshot commit on the `release` branch. @@ -257,37 +235,20 @@ with a [GPG key](http://www.cryptol.net/files/Galois.asc). ## Cutting releases -**TODO**: make this relevant to folks outside Galois; right now the - build farm exists within the Galois network only, and Galois also - controls the release signing key. - The release process is: -1. Make sure the `release/n.n.n` branch is in a release/ready state, +1. Make sure the `release-n.n.n` branch is in a release/ready state, with successful build artifacts across all platforms on the - relevant Jenkins job. **TODO**: get a Jenkins job running per - release branch, rather than just `master`. -1. Merge the `release/n.n.n` branch into the pristine `release` branch + relevant GitHub Action. +1. Merge the `release-n.n.n` branch into the pristine `release` branch and add a git tag. -1. Merge the `release/n.n.n` branch back into `master` for future - development, and delete the `release/n.n.n` branch. -1. Run the `cryptol-release` Jenkins job to create a draft - release. Specify the build number with the successful artifacts, - the textual version tag (e.g., "2.1.0"), whether it's a prerelease - (e.g., an alpha), and keep the `DRAFT` option checked. -1. On the Github page for the draft release and add a changelog - (**TODO**: automate changelogs?). -1. (**TODO**: this part of the process needs to be better and - automated) Download the successfully-built artifacts _from - Jenkins_, and in the same directory run the script - `/release-infrastructure/sign.sh` from the `cryptol-internal.git` - repository. You must have the correct GPG key (D3103D7E) for this - to work. +1. Merge the `release-n.n.n` branch back into `master` for future + development. +1. Upload the build archives to the draft release on Github. 1. Upload the `.sig` files to the draft release on Github. -1. Publish the release and announce it (**TODO**: compile mailing lists) +1. Publish the release and announce it - (in the `cryptol2-web.git` repo) - - - @galois on Twitter (for major releases) - - TODO: more? diff --git a/Dockerfile b/Dockerfile index 51a579b6..7217225d 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,45 +1,20 @@ -FROM haskell:8.6 AS build -RUN apt-get update \ - && apt-get install -y wget libncurses-dev unzip \ - && wget https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-debian-8.11.zip \ - && unzip z3*.zip \ - && mv z3-*/bin/z3 /usr/local/bin -RUN useradd -m cryptol \ - && su -c '/opt/cabal/bin/cabal v2-update' cryptol -COPY --chown=cryptol:cryptol . /cryptol -USER cryptol -WORKDIR /cryptol -ARG CRYPTOLPATH="/home/cryptol/.cryptol" -ARG TESTS="modsys parser issues regression renamer mono-binds" -ARG DIFF="diff" -ARG IGNORE_EXPECTED="--ignore-expected" -ARG CABAL_BUILD_FLAGS="-j" -ARG CABAL_INSTALL_FLAGS="${CABAL_BUILD_FLAGS}" -RUN ./cry build -ARG TIME="" -RUN ./cry test -RUN mkdir -p rootfs/"${CRYPTOLPATH}" \ - && cp -r lib/* rootfs/"${CRYPTOLPATH}" \ - && mkdir -p rootfs/usr/local \ - && rm -r cryptol-*-Linux-*_unknown/share/doc \ - && mv cryptol-*-Linux-*_unknown/* rootfs/usr/local \ - && cp /usr/local/bin/z3 rootfs/usr/local/bin/z3 -USER root -RUN chown -R root:root /cryptol/rootfs - - -from debian:stretch AS solvers +from debian:buster AS solvers # Install needed packages for building RUN apt-get update \ - && apt-get install -y curl cmake gcc g++ git libreadline-dev + && apt-get install -y curl cmake gcc g++ git libreadline-dev unzip RUN useradd -m user RUN install -d -o user -g user /solvers USER user WORKDIR /solvers RUN mkdir -p rootfs/usr/local/bin -# Build abc from Github. (Latest version.) +# Get Z3 4.8.8 from GitHub +RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip --output z3.zip +RUN unzip z3.zip +RUN mv z3-*/bin/z3 rootfs/usr/local/bin + +# Build abc from GitHub. (Latest version.) RUN git clone https://github.com/berkeley-abc/abc.git RUN cd abc && make -j$(nproc) RUN cp abc/abc rootfs/usr/local/bin @@ -49,35 +24,59 @@ RUN curl -L https://github.com/Boolector/boolector/archive/3.2.1.tar.gz | tar xz RUN cd boolector* && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh && cd build && make -j$(nproc) RUN cp boolector*/build/bin/boolector rootfs/usr/local/bin -# Install yices 2.6.2 +# Install Yices 2.6.2 RUN curl -L https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz | tar xz -RUN cp yices*/bin/yices-smt2 rootfs/usr/local/bin +RUN cp yices*/bin/yices-smt2 rootfs/usr/local/bin \ + && cp yices*/bin/yices rootfs/usr/local/bin -# Install cvc4 1.8 +# Install CVC4 1.8 RUN curl -L https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt --output rootfs/usr/local/bin/cvc4 -# Install Mathsat 5.6.3 - Uncomment if you are in compliance with Mathsat's license. +# Install MathSAT 5.6.3 - Uncomment if you are in compliance with MathSAT's license. # RUN curl -L https://mathsat.fbk.eu/download.php?file=mathsat-5.6.3-linux-x86_64.tar.gz | tar xz # RUN cp mathsat-5.6.3-linux-x86_64/bin/mathsat rootfs/usr/local/bin # Set executable and run tests RUN chmod +x rootfs/usr/local/bin/* -COPY --from=build /cryptol/rootfs / -ENV PATH=/solvers/rootfs/usr/local/bin:$PATH + +FROM haskell:8.8 AS build + +RUN apt-get update && apt-get install -y libncurses-dev +COPY --from=solvers /solvers/rootfs / +RUN useradd -m cryptol \ + && su -c '/opt/cabal/bin/cabal v2-update' cryptol +COPY --chown=cryptol:cryptol . /cryptol +USER cryptol +WORKDIR /cryptol +ENV PATH=/cryptol/rootfs/usr/local/bin:$PATH +ARG CRYPTOLPATH="/cryptol/.cryptol" +ENV LANG=C.UTF-8 \ + LC_ALL=C.UTF-8 +COPY cabal.GHC-8.8.3.config cabal.project.freeze +RUN mkdir -p rootfs/usr/local/bin +RUN cabal v2-install --install-method=copy --installdir=rootfs/usr/local/bin exe:cryptol +RUN cabal v2-install --install-method=copy --installdir=bin test-lib +RUN ./bin/test-runner --ext=.icry --exe=./rootfs/usr/local/bin/cryptol -F -b tests +ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH RUN ! $(cryptol -c ":s prover=abc" | tail -n +2 | grep -q .) \ # && ! $(cryptol -c ":s prover=mathsat" | tail -n +2 | grep -q .) \ && ! $(cryptol -c ":s prover=cvc4" | tail -n +2 | grep -q .) \ && ! $(cryptol -c ":s prover=yices" | tail -n +2 | grep -q .) \ && ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \ && ! $(cryptol -c ":s prover=z3" | tail -n +2 | grep -q .) +RUN mkdir -p rootfs/"${CRYPTOLPATH}" \ + && cp -r lib/* rootfs/"${CRYPTOLPATH}" +USER root +RUN chown -R root:root /cryptol/rootfs - -FROM debian:stretch-slim +FROM debian:buster-slim RUN apt-get update \ - && apt-get install -y libgmp10 libgomp1 libffi6 wget libncurses5 unzip \ + && apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 \ && apt-get clean && rm -rf /var/lib/apt/lists/* +RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol COPY --from=build /cryptol/rootfs / COPY --from=solvers /solvers/rootfs / -RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol USER cryptol +ENV LANG=C.UTF-8 \ + LC_ALL=C.UTF-8 ENTRYPOINT ["/usr/local/bin/cryptol"] diff --git a/LICENSE b/LICENSE index 6295754e..c879d828 100644 --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2013-2019 Galois Inc. +Copyright (c) 2013-2020 Galois Inc. All rights reserved. Redistribution and use in source and binary forms, with or without diff --git a/LICENSE.rtf b/LICENSE.rtf index 94bba994..11fc6721 100644 --- a/LICENSE.rtf +++ b/LICENSE.rtf @@ -4,7 +4,7 @@ \margl1440\margr1440\vieww12600\viewh7800\viewkind0 \pard\tx720\tx1440\tx2160\tx2880\tx3600\tx4320\tx5040\tx5760\tx6480\tx7200\tx7920\tx8640\pardirnatural -\f0\fs24 \cf0 Copyright (c) 2013-2019 Galois Inc.\ +\f0\fs24 \cf0 Copyright (c) 2013-2020 Galois Inc.\ All rights reserved.\ \ Redistribution and use in source and binary forms, with or without\ diff --git a/Makefile b/Makefile deleted file mode 100644 index 44e45db5..00000000 --- a/Makefile +++ /dev/null @@ -1,287 +0,0 @@ -HERE := $(realpath $(dir $(lastword $(MAKEFILE_LIST)))) - -UNAME := $(shell uname -s) -ARCH := $(shell uname -m) - -TESTS ?= modsys parser issues regression renamer mono-binds -DIFF ?= meld -TIME ?= time - -IGNORE_EXPECTED ?= --ignore-expected - -CABAL_BUILD_FLAGS ?= -j -CABAL_INSTALL_FLAGS ?= $(CABAL_BUILD_FLAGS) - -CABAL := cabal -CABAL_BUILD := $(CABAL) build $(CABAL_BUILD_FLAGS) -CABAL_INSTALL := $(CABAL) install $(CABAL_INSTALL_FLAGS) -CS := $(HERE)/.cabal-sandbox -CS_BIN := $(CS)/bin - -# Used only for windows, to find the right Program Files. -PROGRAM_FILES = Program\ Files\ \(x86\) -# Windows installer tools; assumes running on Cygwin and using WiX 3.10 -WiX := /cygdrive/c/${PROGRAM_FILES}/WiX\ Toolset\ v3.10 -CANDLE := ${WiX}/bin/candle.exe -HEAT := ${WiX}/bin/heat.exe -LIGHT := ${WiX}/bin/light.exe - -REV ?= $(shell git rev-parse --short=7 HEAD || echo "unknown") -VERSION := $(shell grep -i ^Version cryptol.cabal | awk '{ print $$2}') -SYSTEM_DESC ?= ${UNAME}-${ARCH}_${REV} -PKG := cryptol-${VERSION}-${SYSTEM_DESC} - -# Windows-specific stuff -ifneq (,$(findstring _NT,${UNAME})) - DIST := ${PKG}.msi - EXE_EXT := .exe - adjust-path = '$(shell /usr/bin/cygpath -w $1)' - PREFIX ?= - # For a systemwide distribution .msi, use: - # PREFIX ?= ${PROGRAM_FILES}/Galois/Cryptol\ ${VERSION} - # split this up because `cabal copy` strips drive letters - PREFIX_ABS := /cygdrive/c/${PREFIX} - # since Windows installs aren't overlapping like /usr/local, we - # don't need this extra prefix - PREFIX_SHARE := - # goes under the share prefix - PREFIX_DOC := /doc - PKG_PREFIX := ${PKG}/${PREFIX} - ROOT_PATH := /cygdrive/c -else - DIST := ${PKG}.tar.gz ${PKG}.zip - EXE_EXT := - adjust-path = '$1' - PREFIX ?= - # For a systemwide distribution like an .rpm or .pkg, use something like: - # PREFIX ?= /usr/local - PREFIX_ABS := ${PREFIX} - PREFIX_SHARE := /share - # goes under the share prefix - PREFIX_DOC := /doc/cryptol - PKG_PREFIX := ${PKG}${PREFIX} - ROOT_PATH := / -endif - -CRYPTOL_EXE := ./dist/build/cryptol/cryptol${EXE_EXT} - -.PHONY: all -all: ${CRYPTOL_EXE} - -.PHONY: run -run: ${CRYPTOL_EXE} - CRYPTOLPATH=$(call adjust-path,$(CURDIR)/lib) ${CRYPTOL_EXE} - -.PHONY: docs -docs: - (cd docs; make) - -.PHONY: dist -dist: ${DIST} - -.PHONY: tarball -tarball: ${PKG}.tar.gz - -.PHONY: zip -zip: ${PKG}.zip - -.PHONY: msi -msi: ${PKG}.msi - -# TODO: piece this apart a bit more; if right now if something fails -# during initial setup, you have to invoke this target again manually -${CS}: - $(CABAL) sandbox init - -${CS_BIN}/alex: | ${CS} - $(CABAL_INSTALL) alex - -${CS_BIN}/happy: | ${CS} ${CS_BIN}/alex - $(CABAL_INSTALL) happy - -GIT_INFO_FILES := -ifneq ("$(wildcard .git/index)","") -GIT_INFO_FILES := ${GIT_INFO_FILES} .git/index -endif -ifneq ("$(wildcard .git/HEAD)","") -GIT_INFO_FILES := ${GIT_INFO_FILES} .git/HEAD -endif -ifneq ("$(wildcard .git/packed-refs)","") -GIT_INFO_FILES := ${GIT_INFO_FILES} .git/packed-refs -endif - -CRYPTOL_SRC := \ - $(shell find src cryptol bench \ - \( -name \*.hs -or -name \*.lhs -or -name \*.x -or -name \*.y \) \ - -and \( -not -name \*\#\* \) -print) \ - $(shell find lib -name \*.cry) \ - ${GIT_INFO_FILES} - -print-%: - @echo $* = $($*) - -# If CRYPTOL_SERVER is nonempty, build the cryptol-server executable -ifneq (,${CRYPTOL_SERVER}) - SERVER_FLAG := -fserver -endif - -# We do things differently based on whether we have a PREFIX set by -# the user. If we do, then we know the eventual path it'll wind up in -# (useful for stuff like RPMs or Homebrew). If not, we try to be as -# relocatable as possible. -ifneq (,${PREFIX}) - PREFIX_ARG := --prefix=$(call adjust-path,${PREFIX_ABS}) - DESTDIR_ARG := --destdir=${PKG} - CONFIGURE_ARGS := -f-relocatable \ - --docdir=$(call adjust-path,${PREFIX}/${PREFIX_SHARE}/${PREFIX_DOC}) \ - ${SERVER_FLAG} -else - # This is kind of weird: 1. Prefix argument must be absolute; Cabal - # doesn't yet fully support relocatable packages. 2. We have to - # provide *some* prefix here even if we're not using it, otherwise - # `cabal copy` will make a mess in the PKG directory. - PREFIX_ARG := --prefix=$(call adjust-path,${ROOT_PATH}) - DESTDIR_ARG := --destdir=${PKG} - CONFIGURE_ARGS := --docdir=$(call adjust-path,${PREFIX_SHARE}/${PREFIX_DOC}) \ - ${SERVER_FLAG} -endif - -dist/setup-config: cryptol.cabal Makefile | ${CS_BIN}/alex ${CS_BIN}/happy - $(CABAL_INSTALL) --only-dependencies ${SERVER_FLAG} - $(CABAL) configure ${PREFIX_ARG} --datasubdir=cryptol \ - ${CONFIGURE_ARGS} - -${CRYPTOL_EXE}: $(CRYPTOL_SRC) dist/setup-config - $(CABAL_BUILD) - - -PKG_BIN := ${PKG_PREFIX}/bin -PKG_SHARE := ${PKG_PREFIX}${PREFIX_SHARE} -PKG_CRY := ${PKG_SHARE}/cryptol -PKG_DOC := ${PKG_SHARE}${PREFIX_DOC} -PKG_EXAMPLES := ${PKG_DOC}/examples -PKG_EXCONTRIB := ${PKG_EXAMPLES}/contrib -PKG_EXFUNSTUFF := ${PKG_EXAMPLES}/funstuff - -PKG_EXAMPLE_FILES := docs/ProgrammingCryptol/aes/AES.cry \ - docs/ProgrammingCryptol/enigma/Enigma.cry \ - examples/ChaChaPolyCryptolIETF.md \ - examples/Cipher.cry \ - examples/DES.cry \ - examples/DEStest.cry \ - examples/Test.cry \ - -PKG_EXCONTRIB_FILES := examples/contrib/EvenMansour.cry \ - examples/contrib/RC4.cry \ - examples/contrib/README.md \ - examples/contrib/mkrand.cry \ - -PKG_EXFUNSTUFF_FILES := examples/funstuff/Coins.cry \ - examples/funstuff/FoxChickenCorn.cry \ - examples/funstuff/NQueens.cry \ - examples/funstuff/marble.cry \ - -PKG_MINILOCK_FILES := $(shell find examples/MiniLock) - -${PKG}: ${CRYPTOL_EXE} \ - docs/*.md docs/*.pdf LICENSE LICENSE.rtf \ - ${PKG_EXAMPLE_FILES} ${PKG_EXCONTRIB_FILES} ${PKG_EXFUNSTUFF_FILES} \ - ${PKG_MINILOCK_FILES} - $(CABAL) copy ${DESTDIR_ARG} - mkdir -p ${PKG_CRY} - mkdir -p ${PKG_DOC} - mkdir -p ${PKG_EXAMPLES} - mkdir -p ${PKG_EXCONTRIB} - cp docs/*.md ${PKG_DOC} - cp docs/*.pdf ${PKG_DOC} - for EXAMPLE in ${PKG_EXAMPLE_FILES}; do \ - cp $$EXAMPLE ${PKG_EXAMPLES}; done - for EXAMPLE in ${PKG_EXCONTRIB_FILES}; do \ - cp $$EXAMPLE ${PKG_EXCONTRIB}; done - for EXAMPLE in ${PKG_EXFUNSTUFF_FILES}; do \ - cp $$EXAMPLE ${PKG_EXFUNSTUFF}; done - cp -r examples/MiniLock ${PKG_EXAMPLES} - -# cleanup unwanted files -# don't want to bundle the cryptol library in the binary distribution - rm -rf ${PKG_PREFIX}/lib; rm -rf ${PKG_PREFIX}/*windows-ghc* -# don't ship haddock - rm -rf ${PKG_DOC}/html - -.PHONY: install -install: ${PKG} - [ -n "${PREFIX}" ] \ - || (echo "[error] Can't install without PREFIX set"; false) - (cd ${PKG_PREFIX}; \ - find . -type d -exec install -d ${PREFIX}/{} \; ; \ - find bin -not -type d -exec install -m 755 {} ${PREFIX}/{} \; ; \ - find share -not -type d -exec install -m 644 {} ${PREFIX}/{} \;) - -${PKG}.tar.gz: ${PKG} - tar -czvf $@ $< - -${PKG}.zip: ${PKG} - zip -r $@ $< - -${PKG}.msi: ${PKG} win32/cryptol.wxs - ${HEAT} dir ${PKG_PREFIX} -o allfiles.wxs -nologo -var var.pkg \ - -ag -wixvar -cg ALLFILES -srd -dr INSTALLDIR -sfrag - ${CANDLE} -ext WixUIExtension -ext WixUtilExtension \ - -dversion=${VERSION} -dpkg=${PKG_PREFIX} win32/cryptol.wxs - ${CANDLE} -ext WixUIExtension -ext WixUtilExtension \ - -dversion=${VERSION} -dpkg=${PKG_PREFIX} allfiles.wxs - ${LIGHT} -ext WixUIExtension -ext WixUtilExtension \ - -sval -o $@ cryptol.wixobj allfiles.wixobj - rm -f allfiles.wxs - rm -f *.wixobj - rm -f *.wixpdb - -${CS_BIN}/cryptol-test-runner: \ - ${PKG} \ - $(CURDIR)/tests/Main.hs \ - $(CURDIR)/tests/cryptol-test-runner.cabal - $(CABAL_INSTALL) ./tests - -.PHONY: test -test: ${CS_BIN}/cryptol-test-runner - ( cd tests && \ - echo "Testing on $(UNAME)-$(ARCH)" && \ - ${TIME} $(realpath $(CS_BIN)/cryptol-test-runner) \ - $(TESTS) \ - --exe $(call adjust-path,${CURDIR}/${PKG_BIN}/cryptol${EXE_EXT}) \ - -r output \ - -T --hide-successes \ - -T --jxml=$(call adjust-path,$(CURDIR)/results.xml) \ - $(IGNORE_EXPECTED) \ - $(if $(DIFF),-p $(DIFF),) \ - ) - -# Since this is meant for development rather than end-user builds, -# this tries to stay out of the way of the other targets by -# reconfiguring, then removing dist/setup-config so that other targets -# aren't left in a weird state -.PHONY: bench -bench: cryptol.cabal Makefile | ${CS_BIN}/alex ${CS_BIN}/happy - $(CABAL_INSTALL) --only-dependencies --enable-benchmarks - $(CABAL) configure --enable-benchmarks - $(CABAL) bench --benchmark-option=--junit --benchmark-option=$(call adjust-path,$(CURDIR)/bench-parser.xml) --benchmark-option='parser/' - $(CABAL) bench --benchmark-option=--junit --benchmark-option=$(call adjust-path,$(CURDIR)/bench-typechecker.xml) --benchmark-option='typechecker/' - $(CABAL) bench --benchmark-option=--junit --benchmark-option=$(call adjust-path,$(CURDIR)/bench-conc_eval.xml) --benchmark-option='conc_eval/' - $(CABAL) bench --benchmark-option=--junit --benchmark-option=$(call adjust-path,$(CURDIR)/bench-sym_eval.xml) --benchmark-option='sym_eval/' - rm -rf dist/setup-config - -.PHONY: clean -clean: - cabal clean - rm -f $(CS_BIN)/cryptol-test-suite - rm -rf cryptol-${VERSION}*/ - rm -rf cryptol-${VERSION}*.tar.gz - rm -rf cryptol-${VERSION}*.zip - rm -rf cryptol-${VERSION}*.msi - -.PHONY: squeaky -squeaky: clean - -$(CABAL) sandbox delete - (cd docs; make clean) - rm -rf dist - rm -rf tests/dist diff --git a/README.md b/README.md index 913c3669..b554a3d6 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,10 @@ [![Build Status](https://github.com/GaloisInc/cryptol/workflows/Cryptol/badge.svg?branch=master) -](https://github.com/GaloisInc/cryptol/actions?query=workflow%3ACryptol) +](https://github.com/GaloisInc/cryptol/actions?query=workflow%3A%22Cryptol+Nightly+Builds%22) # Cryptol, version 2 - This version of Cryptol is (C) 2013-2017 Galois, Inc., and + This version of Cryptol is (C) 2013-2020 Galois, Inc., and distributed under a standard, three-clause BSD license. Please see the file LICENSE, distributed with this software, for specific terms and conditions. @@ -29,13 +29,12 @@ Yices, Z3, or CVC4, to prove predicates for all possible inputs. # Getting Cryptol Binaries -Cryptol binaries for Mac OS X, Linux, and Windows are available from -the GitHub -[releases page](https://github.com/GaloisInc/cryptol/releases). Mac OS -X and Linux binaries are distributed as a tarball which you can +Cryptol binaries for Mac OS X, Linux, and Windows are available from the +GitHub [releases page](https://github.com/GaloisInc/cryptol/releases). +Mac OS X and Linux binaries are distributed as a tarball which you can extract to a location of your choice. Windows binaries are distributed -as an `.msi` installer package which places a shortcut to the Cryptol -interpreter in the Start menu. +both as tarballs and as `.msi` installer packages which place a shortcut +to the Cryptol interpreter in the Start menu. On Mac OS X, Cryptol is also available via [Homebrew](http://brew.sh/). Simply run `brew update && brew install cryptol` @@ -46,13 +45,15 @@ to get the latest stable version. 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. You can download Z3 binaries for a variety of -platforms from their [releases page](https://github.com/Z3Prover/z3/releases). +`:prove` commands. Cryptol generally requires the most recent version +of Z3, which at the time of writing this file is 4.8.8. -Cryptol generally requires the most recent version of Z3, which at the -time of writing this file is 4.5.0. Note that if you install Cryptol -using Homebrew, the appropriate version of Z3 will be installed -automatically. +You can download Z3 binaries for a variety of platforms from their +[releases page](https://github.com/Z3Prover/z3/releases). If you +install Cryptol using Homebrew, the appropriate version of Z3 will be +installed automatically. If you're using Linux, the package manager for +your distribution may include Z3, as well, though sometimes the +available versions are somewhat old. After installation, make sure that `z3` (or `z3.exe` on Windows) is on your PATH. @@ -60,9 +61,10 @@ is on your PATH. ### Note for 64-bit Linux Users On some 64-bit Linux configurations, 32-bit binaries do not work. This -can lead to unhelpful error messages like `z3: no such file or directory`, even when `z3` is clearly present. To fix this, either -install 32-bit compatibility packages for your distribution, or -download the `x64` version of Z3. +can lead to unhelpful error messages like `z3: no such file or +directory`, even when `z3` is clearly present. To fix this, either +install 32-bit compatibility packages for your distribution, or download +the `x64` version of Z3. # Building Cryptol From Source @@ -72,16 +74,16 @@ on [GitHub](https://github.com/GaloisInc/cryptol). Cryptol builds and runs on various flavors of Linux, Mac OS X, and Windows. We regularly build and test it in the following environments: -- Mac OS X 10.10 64-bit -- CentOS 6 32/64-bit -- Windows 7 32-bit +- macOS 10.15, 64-bit +- Ubuntu 18.04, 64-bit +- Windows Server 2019, 64-bit ## Prerequisites -Cryptol is developed using GHC 7.10.2 and cabal-install 1.22, though -it is still tested with the previous major version of GHC. The easiest -way to get the correct versions is to follow the instructions on the -[haskell.org downloads page](https://www.haskell.org/downloads). +Cryptol is regularly built and tested with the three most recent +versions of GHC, which at the time of this writing are 8.6.5, 8.8.3, and +8.10.1. 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 Cryptol. Most should already be present for your operating system, but @@ -96,42 +98,30 @@ You'll also need [Z3](#getting-z3) installed when running Cryptol. From the Cryptol source directory, run: - make + ./cry build This will build Cryptol in place. From there, there are additional targets: -- `make run`: run Cryptol in the current directory -- `make test`: run the regression test suite (note: 4 failures is expected) -- `make docs`: build the Cryptol documentation (requires - [pandoc](http://johnmacfarlane.net/pandoc/) and - [TeX Live](https://www.tug.org/texlive/)) -- `make tarball`: build a tarball with a relocatable Cryptol binary and documentation -- `make dist`: build a platform-specific distribution. On all - platforms except Windows, this is currently equivalent to `make tarball`. On Windows, this will build an `.msi` package using - [WiX Toolset 3.8](http://wixtoolset.org/), which must be installed - separately. +- `./cry run`: run Cryptol in the current directory +- `./cry test`: run the regression test suite ## Installing Cryptol -If you run `cabal install` in your source directory after running one -of these `make` targets, you will end up with a binary in -`.cabal-sandbox/bin/cryptol`. You can either use that binary directly, -or use the results of `tarball` or `dist` to install Cryptol in a -location of your choice. +If you run `cabal v2-install --installdir=DIR` in your source directory +after running one of the above `./cry` command, you will end up with a +binary in `DIR`. ## Configuring Cryptol -Cryptol depends on several external files for complete operation. These -files are contained in the `lib` directory of the Cryptol repository. If -you install with `cabal install`, these files will be automaticall -copied into a directory that the `cryptol` executable can find. If you -install in other ways, you will have to do more manual configuration. -There are two options: +Cryptol can use several external files to control its operation. +Normally, the build process embeds these files into the executable. +However, these embedded files can be overwritten with local copies in +two ways: - Copy the contents of the `lib` directory into `$HOME/.cryptol`. - Set the `CRYPTOLPATH` environment variable to name some other - directory that contains those files. + directory that contains the files from the `lib` directory. # Contributing @@ -145,22 +135,23 @@ If you write Cryptol programs that you think would benefit the community, fork the GitHub repository, and add them to the `examples/contrib` directory and submit a pull request. -We host a Cryptol mailing list, which -you can [join here](https://groups.google.com/a/galois.com/forum/#!forum/cryptol-users). +We host a Cryptol mailing list, which you can [join +here](https://groups.google.com/a/galois.com/forum/#!forum/cryptol-users). -If you run into a bug in Cryptol, if something doesn't make sense in -the documentation, if you think something could be better, or if you -just have a cool use of Cryptol that you'd like to share with us, use -the issues page on [GitHub](https://github.com/GaloisInc/cryptol), or -send email to . +If you run into a bug in Cryptol, if something doesn't make sense in the +documentation, if you think something could be better, or if you just +have a cool use of Cryptol that you'd like to share with us, use the +issues page on [GitHub](https://github.com/GaloisInc/cryptol), or send +email to . ## Developers If you'd like to get involved with Cryptol development, see the list of -[low-hanging fruit](https://github.com/GaloisInc/cryptol/labels/low-hanging%20fruit). These -are tasks which should be straightforward to implement. Make a -fork of this GitHub repository, send along pull requests and we'll -be happy to incorporate your changes. +[low-hanging +fruit](https://github.com/GaloisInc/cryptol/labels/low-hanging%20fruit). +These are tasks which should be straightforward to implement. Make a +fork of this GitHub repository, send along pull requests and we'll be +happy to incorporate your changes. ### Repository Structure @@ -185,12 +176,15 @@ algorithms specified in Cryptol. If you are familiar with version 1 of Cryptol, you should read the `Version2Changes` document in the `docs` directory. +For a large collection of Cryptol examples, see the [cryptol-specs +repository](https://github.com/galoisinc/cryptol-specs). + Cryptol is still under active development at Galois. We are also building tools that consume both Cryptol specifications and -implementations in (for example) C or Java, and can (with some amount -of work) allow you to verify that an implementation meets its -specification. Email us at if you're interested -in these capabilities. +implementations in (for example) C or Java, and can (with some amount of +work) allow you to verify that an implementation meets its +specification. See more information on the [SAW +website](https://saw.galois.com). # Thanks! diff --git a/cry b/cry index 9bad94d7..6a71098b 100755 --- a/cry +++ b/cry @@ -43,7 +43,8 @@ case $COMMAND in cabal v2-build exe:cryptol - sed -i "/^$dirty_string/d" src/GitRev.hs + sed -i.bak "/^$dirty_string/d" src/GitRev.hs + rm -f src/GitRev.hs.bak ;; haddock) echo Building Haddock documentation && cabal v2-haddock ;;