Skip to content

Commit

Permalink
Merge branch 'fstar-master'
Browse files Browse the repository at this point in the history
  • Loading branch information
protz committed May 17, 2018
2 parents 4064311 + f0f1f0e commit 951e267
Show file tree
Hide file tree
Showing 410 changed files with 142,682 additions and 4,387 deletions.
24 changes: 16 additions & 8 deletions .ci/install.sh
Original file line number Diff line number Diff line change
Expand Up @@ -2,26 +2,34 @@

set -e

git config --global user.name "Dzomo, the Everest Yak"
git config --global user.email "[email protected]"

git clone https://github.com/fstarlang/fstar-mode.el
git clone https://dzomo:$DZOMO_TOKEN@github.com/fstarlang/fstarlang.github.io

if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
sudo apt-get install --yes libssl-dev opam libgmp-dev libsqlite3-dev g++-5 gcc-5 libc6-dev;
sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 200;
sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 200;
fi

sudo easy_install docutils sphinx sphinx-rtd-theme

export OPAMYES=true
opam init
export OPAMJOBS=4
opam init --comp=4.05.0
eval $(opam config env)
opam install batteries sqlite3 fileutils stdint zarith yojson pprint \
ppx_deriving_yojson menhir ulex process fix wasm

git clone https://github.com/project-everest/everest
./everest/everest --yes opam z3

if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
export Z3=z3-4.4.1-x64-ubuntu-14.04;
wget https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/$Z3.zip;
unzip $Z3.zip;
wget https://www.dropbox.com/s/r1uj2cqifhz50ri/d8.tar.bz2?dl=0 -O d8.tar.bz2
tar xjvf d8.tar.bz2
fi

git clone --branch stable --single-branch --depth 1 https://github.com/FStarLang/FStar.git fstar
git clone --branch master --single-branch --depth 1 https://github.com/mitls/hacl-star
git clone --branch master --single-branch --depth 1 https://github.com/FStarLang/FStar.git fstar
git clone --branch fstar-master --single-branch --depth 1 https://github.com/mitls/hacl-star
make -C fstar/src/ocaml-output
make -C fstar/ulib/ml -j 4
32 changes: 25 additions & 7 deletions .ci/script.sh
Original file line number Diff line number Diff line change
Expand Up @@ -3,26 +3,44 @@
set -e

eval $(opam config env)
export Z3=z3-4.4.1-x64-ubuntu-14.04;
export PATH=/home/travis/build/FStarLang/kremlin/$Z3/bin:$PATH;
export PATH=/home/travis/build/FStarLang/kremlin:$PATH;
export PATH=/home/travis/build/FStarLang/kremlin/d8:$PATH;
export PATH=/home/travis/build/FStarLang/kremlin/fstar/bin:$PATH;
export PATH=/home/travis/build/FStarLang/kremlin/everest/z3/bin:$PATH
export PATH=/home/travis/build/FStarLang/kremlin:$PATH
export PATH=/home/travis/build/FStarLang/kremlin/d8:$PATH
export PATH=/home/travis/build/FStarLang/kremlin/fstar/bin:$PATH
export FSTAR_HOME=/home/travis/build/FStarLang/kremlin/fstar
export HACL_HOME=/home/travis/build/FStarLang/kremlin/hacl-star
export KRML_HOME=/home/travis/build/FStarLang/kremlin
export KREMLIN_HOME=/home/travis/build/FStarLang/kremlin
export OCAMLRUNPARAM=b

echo "\"$Z3\": -traverse" >> _tags
echo "\"everest\": -traverse" >> _tags
echo "\"fstar\": -traverse" >> _tags
echo "\"hacl-star\": -traverse" >> _tags
echo "\"d8\": -traverse" >> _tags
echo "\"MLCrypto\": -traverse" >> _tags
echo "\"fstar-mode.el\": -traverse" >> _tags
echo "\"fstarlang.github.io\": -traverse" >> _tags

echo -e "\e[31m=== Some info about the environment ===\e[0m"
ocamlfind ocamlopt -config
gcc --version
fstar.exe --version
echo | $(which d8)

make && make -C test all wasm
make -C $FSTAR_HOME/ulib -j 4
make -j 4 && make -C test all wasm external -j 4

make -C book html
cd fstarlang.github.io
git pull
cp -R ../book/_build/* lowstar/
rm -rf lowstar/html/static
mv lowstar/html/_static lowstar/html/static
find lowstar/html -type f | xargs sed -i 's/_static/static/g'
git add -A lowstar/
if ! git diff --exit-code HEAD > /dev/null; then
git commit -am "[CI] Refresh Low* tutorial"
git push
else
echo No git diff for the tutorial, not generating a commit
fi
4 changes: 4 additions & 0 deletions .clang-format
Original file line number Diff line number Diff line change
@@ -1 +1,5 @@
IndentPPDirectives: AfterHash
AllowShortBlocksOnASingleLine: false
AllowShortFunctionsOnASingleLine: Empty
Cpp11BracedListStyle: false
AlignAfterOpenBracket: AlwaysBreak
3 changes: 3 additions & 0 deletions .gitattributes
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
*.ml* eol=lf
*.sh eol=lf
*.c eol=lf
*.h eol=lf
Makefile eol=lf
*.hints -diff
5 changes: 5 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -3,3 +3,8 @@
_build
krml
tags
*.checked
*.checked.lax
*~
book/_build
fstar-mode.el
1 change: 1 addition & 0 deletions .merlin
Original file line number Diff line number Diff line change
Expand Up @@ -2,3 +2,4 @@ S src
S lib
B _build/*
PKG ppx_deriving.std ppx_deriving_yojson zarith pprint unix wasm process ulex
PKG visitors.ppx visitors.runtime
Loading

0 comments on commit 951e267

Please sign in to comment.