From 137af19a898a5357c5be58bd2457db5f404144fa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maciej=20Bar=C4=87?= <xgqt@gentoo.org>
Date: Thu, 9 Dec 2021 04:49:24 +0100
Subject: [PATCH] dev-lang/fstar: new package; add version 2021.11.27 and
 2021.11.30
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Package-Manager: Portage-3.0.28, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
---
 dev-lang/fstar/Manifest                |  1 +
 dev-lang/fstar/fstar-2021.11.27.ebuild | 48 ++++++++++++++++++++++++++
 dev-lang/fstar/metadata.xml            | 21 +++++++++++
 3 files changed, 70 insertions(+)
 create mode 100644 dev-lang/fstar/Manifest
 create mode 100644 dev-lang/fstar/fstar-2021.11.27.ebuild
 create mode 100644 dev-lang/fstar/metadata.xml

diff --git a/dev-lang/fstar/Manifest b/dev-lang/fstar/Manifest
new file mode 100644
index 0000000..2a8151c
--- /dev/null
+++ b/dev-lang/fstar/Manifest
@@ -0,0 +1 @@
+DIST fstar-2021.11.27.tar.gz 8227837 BLAKE2B 91bb487830ffbff0e0b90f66b05f22411f713094d00c05cf6bd27a55121149e71b9c1c6d798c16db2c52cf05fe46b85d5df597c0eb6d4b1c926f513f2bd59df2 SHA512 3d6e8f06cd7d4396224b51787b0850a32680e9bc7d195b0b8d0ef9f64171158743e69a175c91256ce8078eb88f11d12039e4fb9913e95ba02c68becd6633bc4c
diff --git a/dev-lang/fstar/fstar-2021.11.27.ebuild b/dev-lang/fstar/fstar-2021.11.27.ebuild
new file mode 100644
index 0000000..f43ef19
--- /dev/null
+++ b/dev-lang/fstar/fstar-2021.11.27.ebuild
@@ -0,0 +1,48 @@
+# Copyright 1999-2021 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+inherit findlib
+
+DESCRIPTION="Verification system for effectful programs"
+HOMEPAGE="https://www.fstar-lang.org"
+SRC_URI="https://github.com/FStarLang/FStar/archive/v${PV}.tar.gz -> ${P}.tar.gz"
+S="${WORKDIR}/FStar-${PV}"
+
+LICENSE="Apache-2.0"
+SLOT="0/${PV}"
+KEYWORDS="~amd64"
+IUSE="+ocamlopt"
+
+RDEPEND="
+	dev-ml/batteries:=
+	dev-ml/ocaml-fileutils:=
+	dev-ml/ocaml-process:=
+	dev-ml/ocaml-stdint:=
+	dev-ml/ppx_deriving:=
+	dev-ml/ppx_deriving_yojson:=
+	dev-ml/ppxlib:=
+	dev-ml/yojson:=
+	dev-ml/zarith:=
+
+	~sci-mathematics/z3-4.8.5
+	dev-libs/gmp:=
+"
+DEPEND="${RDEPEND}"
+BDEPEND="
+	dev-ml/menhir
+	dev-ml/ocamlbuild
+	dev-ml/pprint
+	dev-ml/sedlex
+"
+
+src_install() {
+	findlib_src_preinst
+
+	emake PREFIX="${D}/usr" install
+
+	dosym ${PN}.exe /usr/bin/${PN}
+
+	dodoc *.md
+}
diff --git a/dev-lang/fstar/metadata.xml b/dev-lang/fstar/metadata.xml
new file mode 100644
index 0000000..187b639
--- /dev/null
+++ b/dev-lang/fstar/metadata.xml
@@ -0,0 +1,21 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <longdescription>
+    F* (pronounced F star) is a general-purpose functional programming language
+    with effects aimed at program verification. It puts together the automation
+    of an SMT-backed deductive verification tool with the expressive power of a
+    proof assistant based on dependent types. After verification, F* programs
+    can be extracted to efficient OCaml, F#, C, WASM, or ASM code. This enables
+    verifying the functional correctness and security of realistic
+    applications. The main ongoing use case of F* is building a verified,
+    drop-in replacement for the whole HTTPS stack in Project Everest. This
+    includes verified implementations of TLS 1.2 and 1.3 and of the underlying
+    cryptographic primitives.
+  </longdescription>
+  <upstream>
+    <bugs-to>https://github.com/FStarLang/FStar/issues</bugs-to>
+    <remote-id type="github">FStarLang/FStar</remote-id>
+  </upstream>
+</pkgmetadata>