Merge branch 'fstar-master'

.ci/install.sh

@@ -2,26 +2,34 @@
 
 set -e
 
+git config --global user.name "Dzomo, the Everest Yak"
+git config --global user.email "everbld@microsoft.com"
+
+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

.ci/script.sh

@@ -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

.clang-format

@@ -1 +1,5 @@
 IndentPPDirectives: AfterHash
+AllowShortBlocksOnASingleLine: false
+AllowShortFunctionsOnASingleLine: Empty
+Cpp11BracedListStyle: false
+AlignAfterOpenBracket: AlwaysBreak

.gitattributes

@@ -1,3 +1,6 @@
 *.ml* eol=lf
 *.sh eol=lf
+*.c eol=lf
+*.h eol=lf
 Makefile eol=lf
+*.hints -diff

.gitignore

@@ -3,3 +3,8 @@
 _build
 krml
 tags
+*.checked
+*.checked.lax
+*~
+book/_build
+fstar-mode.el

.merlin

@@ -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