mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-07-07 10:46:54 +03:00
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.
This commit is contained in:
Aaron Tomb
GitHub
parent
6e412ed32e
commit
2f4684c8af
|
|
@ -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
|
||||
43
.travis.yml
43
.travis.yml
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
||||
- <http://www.cryptol.net> (in the `cryptol2-web.git` repo)
|
||||
- <cryptol-team@lists.galois.com>
|
||||
- <cryptol-users@community.galois.com>
|
||||
- @galois on Twitter (for major releases)
|
||||
- TODO: more?
|
||||
|
|
|
|||
85
Dockerfile
85
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"]
|
||||
|
|
|
|||
2
LICENSE
2
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
|
||||
|
|
|
|||
|
|
@ -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\
|
||||
|
|
|
|||
287
Makefile
287
Makefile
|
|
@ -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
|
||||
118
README.md
118
README.md
|
|
@ -1,10 +1,10 @@
|
|||
[
|
||||
](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 <cryptol@galois.com>.
|
||||
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 <cryptol@galois.com>.
|
||||
|
||||
## 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 <cryptol@galois.com> 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!
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user