dev-lang/fstar/Manifest

@@ -1 +0,0 @@
-DIST fstar-2021.11.27.tar.gz 8227837 BLAKE2B 91bb487830ffbff0e0b90f66b05f22411f713094d00c05cf6bd27a55121149e71b9c1c6d798c16db2c52cf05fe46b85d5df597c0eb6d4b1c926f513f2bd59df2 SHA512 3d6e8f06cd7d4396224b51787b0850a32680e9bc7d195b0b8d0ef9f64171158743e69a175c91256ce8078eb88f11d12039e4fb9913e95ba02c68becd6633bc4c

dev-lang/fstar/fstar-2021.11.27.ebuild

@@ -1,48 +0,0 @@
-# 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
-}

dev-lang/fstar/metadata.xml

@@ -1,21 +0,0 @@
-<?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>

sci-mathematics/z3/Manifest

@@ -1 +0,0 @@
-DIST Z3-4.8.5.tar.gz 4177051 BLAKE2B f8c4be9dbab2d5cf6fdb0bd8e9e1648f8ac29bc8ca9241b3ef29699400b383f09601149d50899d6ca828abadacb71161af1524df6d1ed45d7fd95c4a49c0d3df SHA512 ca36e1a0332bd473a64f41dfdb31656fb3486178473e4fd4934dccce109a84c9686c08f94998df74bacb588eb12ea5db25dc17a564ee76f82fd2559349697309

sci-mathematics/z3/metadata.xml

@@ -1,14 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
-
-<pkgmetadata>
-  <use>
-    <flag name="isabelle">
-      Add integration support for the Isabelle/HOL theorem prover
-    </flag>
-  </use>
-  <upstream>
-    <bugs-to>https://github.com/Z3Prover/z3</bugs-to>
-    <remote-id type="github">Z3Prover/z3</remote-id>
-  </upstream>
-</pkgmetadata>

sci-mathematics/z3/z3-4.8.5.ebuild

@@ -1,116 +0,0 @@
-# Copyright 1999-2021 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-CMAKE_ECLASS=cmake
-PYTHON_COMPAT=( python3_{8..10} )
-
-inherit cmake-multilib java-pkg-opt-2 python-single-r1 toolchain-funcs
-
-DESCRIPTION="An efficient theorem prover"
-HOMEPAGE="https://github.com/Z3Prover/z3/"
-SRC_URI="https://github.com/Z3Prover/z3/archive/${P^}.tar.gz"
-S="${WORKDIR}/${PN}-${P^}"
-
-SLOT="0/4.8"
-LICENSE="MIT"
-KEYWORDS="~amd64 ~arm ~arm64 ~ppc64 ~x86"
-IUSE="doc examples gmp isabelle java openmp python"
-REQUIRED_USE="${PYTHON_REQUIRED_USE}"
-
-RDEPEND="
-	${PYTHON_DEPS}
-	gmp? ( dev-libs/gmp:0=[${MULTILIB_USEDEP}] )
-"
-DEPEND="
-	${RDEPEND}
-	java? ( >=virtual/jdk-1.8 )
-"
-BDEPEND="doc? ( app-doc/doxygen )"
-
-CMAKE_BUILD_TYPE=RelWithDebInfo
-
-pkg_setup() {
-	python_setup
-
-	if [[ ${MERGE_TYPE} != binary ]]; then
-		if use openmp && ! tc-has-openmp; then
-			ewarn "Please use an openmp compatible compiler"
-			ewarn "like >gcc-4.2 with USE=openmp"
-			die "Openmp support missing in compiler"
-		fi
-	fi
-}
-
-src_prepare() {
-	cmake_src_prepare
-	java-pkg-opt-2_src_prepare
-}
-
-multilib_src_configure() {
-	local mycmakeargs=(
-		-DCMAKE_INSTALL_DOCDIR="${EPREFIX}/usr/share/doc/${P}"
-		-DENABLE_EXAMPLE_TARGETS=OFF
-		-DBUILD_DOCUMENTATION=$(multilib_native_usex doc)
-		-DBUILD_JAVA_BINDINGS=$(multilib_native_usex java)
-		-DBUILD_PYTHON_BINDINGS=$(multilib_native_usex python)
-		-DUSE_LIB_GMP=$(usex gmp)
-		-DUSE_OPENMP=$(usex openmp)
-	)
-	multilib_is_native_abi && use java &&
-		mycmakeargs+=( -DJAVA_HOME="$(java-config -g JAVA_HOME )" )
-	cmake_src_configure
-}
-
-multilib_src_test() {
-	cmake-utils_src_make test-z3
-	set -- "${BUILD_DIR}"/test-z3 /a
-	echo "${@}" >&2
-	"${@}" || die
-}
-
-multilib_src_install_all() {
-	dodoc README.md RELEASE_NOTES
-	use examples && dodoc -r examples
-	use python && python_optimize
-
-	if use isabelle; then
-		insinto /usr/share/Isabelle/contrib/${P}/etc
-		newins - settings <<-EOF
-			Z3_COMPONENT="\$COMPONENT"
-			Z3_HOME="${EPREFIX}/usr/bin"
-			Z3_SOLVER="${EPREFIX}/usr/bin/z3"
-			Z3_REMOTE_SOLVER="z3"
-			Z3_VERSION="${PV}"
-			Z3_INSTALLED="yes"
-			Z3_NON_COMMERCIAL="yes"
-		EOF
-	fi
-}
-
-pkg_postinst() {
-	if use isabelle; then
-		if [[ -f ${ROOT%/}/etc/isabelle/components ]]; then
-			sed -e "/contrib\/${PN}-[0-9.]*/d" \
-				-i "${ROOT%/}/etc/isabelle/components" || die
-			cat <<-EOF >> "${ROOT%/}/etc/isabelle/components" || die
-				contrib/${P}
-			EOF
-		fi
-	fi
-}
-
-pkg_postrm() {
-	if use isabelle; then
-		if [[ ! ${REPLACING_VERSIONS} ]]; then
-			if [[ -f "${ROOT%/}/etc/isabelle/components" ]]; then
-				# Note: this sed should only match the version of this ebuild
-				# Which is what we want as we do not want to remove the line
-				# of a new Isabelle component being installed during an upgrade.
-				sed -e "/contrib\/${P}/d" \
-					-i "${ROOT%/}/etc/isabelle/components" || die
-			fi
-		fi
-	fi
-}