casa-mp-base

# -*- coding: utf-8; mode: tcl; tab-width: 4; indent-tabs-mode: nil; c-basic-offset: 4 -*- vim:fenc=utf-8:ft=tcl:et:sw=4:ts=4:sts=4

​

PortSystem              1.0

PortGroup               github  1.0

PortGroup               ocaml   1.1

PortGroup               select  1.0

​

name                    fstar

categories              lang devel

maintainers             {landonf @landonf}

​

homepage                https://fstar-lang.org

platforms               darwin

​

github.author           FStarLang

​

depends_build           port:ocaml-ocamlbuild

​

depends_lib             port:ocaml-batteries \

                        port:ocaml-stdint \

                        port:ocaml-zarith \

                        port:ocaml-ppx_deriving \

                        port:ocaml-ppx_deriving_yojson \

                        port:ocaml-process \

                        port:ocaml-yojson \

                        port:ocaml-fileutils \

                        port:ocaml-menhir \

                        port:ocaml-pprint

​

use_configure           no

​

ocaml.use_findlib       yes

​

# Basic configuration options that vary based on the subport (fstar vs kremlin)

# and its release type (stable vs devel).

default fstar.stable        {[expr {![string match {*-devel} $subport]}]}

default fstar.project       {[regsub {(.*?)(-devel)?$} ${subport} {\1}]}

default fstar.port_suffix   {[expr {${fstar.stable} ? "" : "-devel"}]}

​

options fstar.release \

        fstar.version

​

if {${fstar.stable}} {

    fstar.version       0.9.7.0-alpha1

    # Strip everything but <major>.<minor>

    fstar.release       [regsub {^([^\.]+\.[^\.]+).*} ${fstar.version} {\1}]

} else {

    fstar.version       20191129

    fstar.release       devel

}

​

foreach fname {fstar kremlin} {

    set S [list subst -novariables]

​

    options ${fname}.home \

            ${fname}.bin \

            ${fname}.port \

            ${fname}.select_name \

            ${fname}.doc_dirs

​

    default ${fname}.home        [{*}$S {${prefix}/libexec/[set fname]-${fstar.release}}]

    default ${fname}.bin         [{*}$S {[set fname]}]

    default ${fname}.port        [{*}$S {[set fname]${fstar.port_suffix}}]

    default ${fname}.select_name {${fstar.project}-${fstar.release}}

}

​

# Provide generic alias options for the current subport

foreach key {home doc_dirs bin port select_name} {

    set var "${fstar.project}.${key}"

    default fstar.subport.${key}    [subst -nocommands {[set ${var}]}]

}

​

# Common fstar/fstar-devel configuration

if {${fstar.project} eq "fstar"} {

    github.project          FStar

    license                 MIT

    description             General-purpose functional language aimed at program verification

    long_description        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.

​

    patchfiles              patch-z3-path \

                            patch-fix-get_exec_dir

​

    post-patch {

        # Fix up the z3 path in the generated code, too.