Skip to content
Permalink
Browse files

Revert "[CI] regenerate hints + ocaml snapshot"

This reverts commit 53fb86d.
  • Loading branch information
msprotz committed Jan 27, 2017
1 parent 53fb86d commit e35b8b42e9c6944deda3241c3a481bd9733ecddb
Showing 362 changed files with 141,143 additions and 146,377 deletions.
@@ -1,44 +1,44 @@
FROM ubuntu:xenial

MAINTAINER Benjamin Beurdouche <benjamin.beurdouche@inria.fr>; Daniel Fabian <daniel.fabian@integral-it.ch>

# Define versions of dependencies
ENV opamv 4.04.0
ENV z3v z3-4.5.0

# Install required packages and set versions
RUN apt-get -qq update
RUN apt-get install --yes sudo libssl-dev libsqlite3-dev g++-5 gcc-5 m4 make opam pkg-config python libgmp3-dev
RUN update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 200
RUN update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 200

# Create user
RUN useradd -ms /bin/bash FStar
RUN echo "FStar ALL=(ALL:ALL) NOPASSWD:ALL" >> /etc/sudoers
USER FStar
WORKDIR /home/FStar

# Prepare build (OCaml packages)
ENV OPAMYES true
RUN opam init
RUN echo ". /home/FStar/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true" >> .bashrc
RUN opam switch ${opamv}
RUN opam install ocamlfind batteries sqlite3 fileutils stdint zarith yojson pprint menhir

# Prepare and build Z3
RUN git clone -b ${z3v} https://github.com/Z3Prover/z3.git
WORKDIR z3
RUN python scripts/mk_make.py
WORKDIR build
RUN make
RUN sudo make install
WORKDIR /home/FStar


# Prepare and build F*
ADD update-fstar.sh .
RUN git clone https://github.com/FStarLang/FStar.git
ENV PATH "~/FStar/bin:$PATH"
RUN opam config exec -- make -C FStar/src/ocaml-output
RUN make ocaml -C FStar/src
RUN opam config exec -- make -C FStar/src/ocaml-output
FROM ubuntu:xenial

MAINTAINER Benjamin Beurdouche <benjamin.beurdouche@inria.fr>; Daniel Fabian <daniel.fabian@integral-it.ch>

# Define versions of dependencies
ENV opamv 4.04.0
ENV z3v z3-4.5.0

# Install required packages and set versions
RUN apt-get -qq update
RUN apt-get install --yes sudo libssl-dev libsqlite3-dev g++-5 gcc-5 m4 make opam pkg-config python libgmp3-dev
RUN update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 200
RUN update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 200

# Create user
RUN useradd -ms /bin/bash FStar
RUN echo "FStar ALL=(ALL:ALL) NOPASSWD:ALL" >> /etc/sudoers
USER FStar
WORKDIR /home/FStar

# Prepare build (OCaml packages)
ENV OPAMYES true
RUN opam init
RUN echo ". /home/FStar/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true" >> .bashrc
RUN opam switch ${opamv}
RUN opam install ocamlfind batteries sqlite3 fileutils stdint zarith yojson pprint menhir

# Prepare and build Z3
RUN git clone -b ${z3v} https://github.com/Z3Prover/z3.git
WORKDIR z3
RUN python scripts/mk_make.py
WORKDIR build
RUN make
RUN sudo make install
WORKDIR /home/FStar


# Prepare and build F*
ADD update-fstar.sh .
RUN git clone https://github.com/FStarLang/FStar.git
ENV PATH "~/FStar/bin:$PATH"
RUN opam config exec -- make -C FStar/src/ocaml-output
RUN make ocaml -C FStar/src
RUN opam config exec -- make -C FStar/src/ocaml-output
@@ -1,5 +1,5 @@
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
(package-initialize)
(set-default 'fstar-executable "~/FStar/bin/fstar.exe")
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
(package-initialize)
(set-default 'fstar-executable "~/FStar/bin/fstar.exe")
(global-flycheck-mode)
@@ -1,18 +1,18 @@
FROM fstarlang/fstar

MAINTAINER Daniel Fabian <daniel.fabian@integral-it.ch>; Benjamin Beurdouche <benjamin.beurdouche@inria.fr>

# Install required packages
RUN sudo apt-get install -y emacs-nox

ENV LANG C.UTF-8
RUN emacs --batch \
--eval "(require 'package)" \
--eval "(add-to-list 'package-archives '(\"melpa\" . \"http://melpa.org/packages/\") t)" \
--eval "(package-initialize)" \
--eval "(package-refresh-contents)" \
--eval "(package-install 'fstar-mode)" \
--eval "(package-install 'flycheck)"

ADD .emacs .emacs
RUN sudo chown FStar:FStar .emacs
FROM fstarlang/fstar

MAINTAINER Daniel Fabian <daniel.fabian@integral-it.ch>; Benjamin Beurdouche <benjamin.beurdouche@inria.fr>

# Install required packages
RUN sudo apt-get install -y emacs-nox

ENV LANG C.UTF-8
RUN emacs --batch \
--eval "(require 'package)" \
--eval "(add-to-list 'package-archives '(\"melpa\" . \"http://melpa.org/packages/\") t)" \
--eval "(package-initialize)" \
--eval "(package-refresh-contents)" \
--eval "(package-install 'fstar-mode)" \
--eval "(package-install 'flycheck)"

ADD .emacs .emacs
RUN sudo chown FStar:FStar .emacs
@@ -1,21 +1,21 @@
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
(package-initialize)
(set-default 'fstar-executable "~/FStar/bin/fstar.exe")
(global-flycheck-mode)
(set-face-font 'default "Terminus-14")



;;set fstar includes, these should work for most tutorial examples, except those using hyperheap
(setq fstar-subp-prover-args '("--include" "/home/FStar/FStar/ucontrib/Platform/fst" "--include" "/home/FStar/FStar/ucontrib/CoreCrypto/fst"))


;;this is what the above corresponds to on the command line:
;fstar --include /home/FStar/FStar/ucontrib/Platform/fst --include /home/FStar/FStar/ucontrib/CoreCrypto/fst

;;set fstar includes, these work for the the Encrypt-then-MAC example:
;(setq fstar-subp-prover-args '("--include" "/home/FStar/FStar/ulib/hyperheap" "--include" "/home/FStar/FStar/ucontrib/Platform/fst" "--include" "/home/FStar/FStar/ucontrib/CoreCrypto/fst"))

;;this is what the above corresponds to on the command line:
;fstar --include /home/FStar/FStar/ulib/hyperheap --include /home/FStar/FStar/ucontrib/Platform/fst --include /home/FStar/FStar/ucontrib/CoreCrypto/fst
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
(package-initialize)
(set-default 'fstar-executable "~/FStar/bin/fstar.exe")
(global-flycheck-mode)
(set-face-font 'default "Terminus-14")



;;set fstar includes, these should work for most tutorial examples, except those using hyperheap
(setq fstar-subp-prover-args '("--include" "/home/FStar/FStar/ucontrib/Platform/fst" "--include" "/home/FStar/FStar/ucontrib/CoreCrypto/fst"))


;;this is what the above corresponds to on the command line:
;fstar --include /home/FStar/FStar/ucontrib/Platform/fst --include /home/FStar/FStar/ucontrib/CoreCrypto/fst

;;set fstar includes, these work for the the Encrypt-then-MAC example:
;(setq fstar-subp-prover-args '("--include" "/home/FStar/FStar/ulib/hyperheap" "--include" "/home/FStar/FStar/ucontrib/Platform/fst" "--include" "/home/FStar/FStar/ucontrib/CoreCrypto/fst"))

;;this is what the above corresponds to on the command line:
;fstar --include /home/FStar/FStar/ulib/hyperheap --include /home/FStar/FStar/ucontrib/Platform/fst --include /home/FStar/FStar/ucontrib/CoreCrypto/fst
@@ -1,18 +1,18 @@
FROM fstarlang/fstar

MAINTAINER Daniel Fabian <daniel.fabian@integral-it.ch>; Benjamin Beurdouche <benjamin.beurdouche@inria.fr>

# Install required packages
RUN sudo apt-get install -y emacs libglu1-mesa xfonts-terminus fonts-symbola

ENV LANG C.UTF-8
RUN emacs --batch \
--eval "(require 'package)" \
--eval "(add-to-list 'package-archives '(\"melpa\" . \"http://melpa.org/packages/\") t)" \
--eval "(package-initialize)" \
--eval "(package-refresh-contents)" \
--eval "(package-install 'fstar-mode)" \
--eval "(package-install 'flycheck)"

ADD .emacs .emacs
RUN sudo chown FStar:FStar .emacs
FROM fstarlang/fstar

MAINTAINER Daniel Fabian <daniel.fabian@integral-it.ch>; Benjamin Beurdouche <benjamin.beurdouche@inria.fr>

# Install required packages
RUN sudo apt-get install -y emacs libglu1-mesa xfonts-terminus fonts-symbola

ENV LANG C.UTF-8
RUN emacs --batch \
--eval "(require 'package)" \
--eval "(add-to-list 'package-archives '(\"melpa\" . \"http://melpa.org/packages/\") t)" \
--eval "(package-initialize)" \
--eval "(package-refresh-contents)" \
--eval "(package-install 'fstar-mode)" \
--eval "(package-install 'flycheck)"

ADD .emacs .emacs
RUN sudo chown FStar:FStar .emacs
@@ -1,12 +1,12 @@
*.fst linguist-language=FStar
*.fsti linguist-language=FStar

*.fs* eol=lf
*.ml* eol=lf
Makefile eol=lf
*.sh eol=lf

/src/tools/* eol=lf

# Don't show diffs for generated ocaml-output files
/src/ocaml-output/*.ml -diff
*.fst linguist-language=FStar
*.fsti linguist-language=FStar

*.fs* eol=lf
*.ml* eol=lf
Makefile eol=lf
*.sh eol=lf

/src/tools/* eol=lf

# Don't show diffs for generated ocaml-output files
/src/ocaml-output/*.ml -diff
@@ -1,78 +1,78 @@
*~
.#*
\#*\#
*.vspx
*.psess
*.suo
*.smt2
*.sav
*.hints.fsval
*.hints.mlval
dump*
cache/
/VS/packages

/src/parser/parse.fs
/src/parser/lex.fs
/src/parser/parse.ml
/src/parser/parse.mli

/src/boot_fstis
/src/boot_fsts
/src/format/formatml.fsi

/lib/FStar.Util.fsti
/lib/FStar.GetOpt.fsti
/lib/FStar.Unionfind.fsti

/ulib/ml/extracted

/bin/*.dll
/bin/*.pdb
/bin/*.mdb
/bin/*.xml
/bin/*.config
/bin/fstar.exe
/bin/fstar.ocaml
/bin/tests.exe
/bin/z3.exe
/bin/z3-x86.exe
/bin/z3-x64.exe
/src/*/obj

examples/*/*.ml
examples/crypto/CntProtocol.exe
examples/wysteria/ocaml-output/*
examples/incl/*.neg/error.log

_build/

*.native
*.byte

queries*.smt2
transcript
dump

*.cmi
*.cmo
*.cmx
*.o

.depend
*.a
*.cmxa
*.so
*.annot
/VS/

tags

*~
*.swp

/.nubuild
/nucache/
/nuobj/
nubuild.log
nubuild.progress
*~
.#*
\#*\#
*.vspx
*.psess
*.suo
*.smt2
*.sav
*.hints.fsval
*.hints.mlval
dump*
cache/
/VS/packages

/src/parser/parse.fs
/src/parser/lex.fs
/src/parser/parse.ml
/src/parser/parse.mli

/src/boot_fstis
/src/boot_fsts
/src/format/formatml.fsi

/lib/FStar.Util.fsti
/lib/FStar.GetOpt.fsti
/lib/FStar.Unionfind.fsti

/ulib/ml/extracted

/bin/*.dll
/bin/*.pdb
/bin/*.mdb
/bin/*.xml
/bin/*.config
/bin/fstar.exe
/bin/fstar.ocaml
/bin/tests.exe
/bin/z3.exe
/bin/z3-x86.exe
/bin/z3-x64.exe
/src/*/obj

examples/*/*.ml
examples/crypto/CntProtocol.exe
examples/wysteria/ocaml-output/*
examples/incl/*.neg/error.log

_build/

*.native
*.byte

queries*.smt2
transcript
dump

*.cmi
*.cmo
*.cmx
*.o

.depend
*.a
*.cmxa
*.so
*.annot
/VS/

tags

*~
*.swp

/.nubuild
/nucache/
/nuobj/
nubuild.log
nubuild.progress

0 comments on commit e35b8b4

Please sign in to comment.
You can’t perform that action at this time.