From 5ef5fce567175adcc2ba7a629b91608f525581bb Mon Sep 17 00:00:00 2001
From: Julian Ospald <hasufell@posteo.de>
Date: Thu, 20 Oct 2016 22:34:39 +0200
Subject: [PATCH] dev-lang/fstar: initial import

Change-Id: I0496b405f97e16623e2640443a99231d6282eaab
---
 metadata/repository_mask.conf               |  1 +
 packages/dev-lang/fstar/fstar-scm.exheres-0 | 60 +++++++++++++++++++++
 2 files changed, 61 insertions(+)
 create mode 100644 packages/dev-lang/fstar/fstar-scm.exheres-0

diff --git a/metadata/repository_mask.conf b/metadata/repository_mask.conf
index 78bd65be..d4c4ee3d 100644
--- a/metadata/repository_mask.conf
+++ b/metadata/repository_mask.conf
@@ -1,5 +1,6 @@
 (
     dev-lang/fsharp[~scm]
+    dev-lang/fstar[~scm]
     games-emulation/gambatte[~scm]
     games-engines/OpenJK[~scm]
     games-fps/eduke32[~scm]
diff --git a/packages/dev-lang/fstar/fstar-scm.exheres-0 b/packages/dev-lang/fstar/fstar-scm.exheres-0
new file mode 100644
index 00000000..738bdda0
--- /dev/null
+++ b/packages/dev-lang/fstar/fstar-scm.exheres-0
@@ -0,0 +1,60 @@
+# Copyright 2016 Julian Ospald <hasufell@posteo.de>
+# Distributed under the terms of the GNU General Public License v2
+
+require github [ user="FStarLang" project="FStar" ]
+
+SUMMARY="An ML-like language with a type system for program verification"
+DESCRIPTION="
+F* (pronounced F star) is an ML-like functional programming language aimed at
+program verification. Its type system includes polymorphism, dependent types,
+monadic effects, refinement types, and a weakest precondition calculus.
+Together, these features allow expressing precise and compact specifications for
+programs, including functional correctness and security properties. The F* type-
+checker aims to prove that programs meet their specifications using a
+combination of SMT solving and manual proofs. Programs written in F* can be
+translated to OCaml or F# for execution.
+"
+HOMEPAGE="https://www.fstar-lang.org ${HOMEPAGE}"
+
+LICENCES="Apache-2.0"
+SLOT="0"
+PLATFORMS="~amd64"
+MYOPTIONS=""
+
+DEPENDENCIES="
+    build:
+        dev-lang/fsharp
+        dev-lang/ocaml[>=4.02.2]
+        dev-ocaml/batteries
+        dev-ocaml/findlib
+        dev-ocaml/yojson
+        dev-ocaml/zarith
+    build+run:
+        dev-libs/gmp:=
+    run:
+        sci-apps/z3
+"
+
+BUGS_TO="hasufell@posteo.de"
+
+src_compile() {
+    # Step 1. Building F* from sources using the F# compiler
+    esandbox disable_net
+    emake -C src
+    esandbox enable_net
+    # Step 2. Extracting the sources of F* itself to OCaml
+    emake ocaml -C src
+    # Step 3. Building F* from the OCaml snapshot
+    emake -C src/ocaml-output
+}
+
+src_install() {
+    insinto /usr/$(exhost --target)/lib/fstar
+    doins -r lib contrib bin
+    edo chmod +x "${IMAGE%/}"/usr/$(exhost --target)/lib/fstar/bin/{fstar.exe,fstar-any.sh,tests.exe,tests-mono.sh}
+    dodoc -r doc/*
+
+    dodir /usr/$(exhost --target)/bin
+    dosym ../lib/fstar/bin/fstar.exe /usr/$(exhost --target)/bin/fstar
+}
+