# -*- 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

name                    fstar
categories              lang devel
maintainers             {landonf @landonf}

homepage                https://fstar-lang.org
platforms               darwin

if {${subport} eq "fstar" || ${subport} eq "karamel"} {
    PortGroup               ocaml 1.1

    depends_build           port:ocaml-ocamlbuild \
                            port:ocaml-dune \
                            port:gmake

    # Requires gmake 3.82+
    build.cmd               ${prefix}/bin/gmake

    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

    # Common configuration options that vary based on the subport (fstar vs karamel)
    foreach fname {fstar karamel} {
        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]}]
        default ${fname}.bin         [{*}$S {[set fname]}]
        default ${fname}.port        [{*}$S {[set fname]}]
        default ${fname}.select_name {${subport}}
    }

    # Provide generic alias options for the current subport
    foreach key {home doc_dirs bin port select_name} {
        set var "${subport}.${key}"
        default fstar.subport.${key}    [subst -nocommands {[set ${var}]}]
    }
}

subport fstar {
    github.setup            FStarLang FStar 2025.03.25 v
    epoch                   1

    license                 Apache-2
    description             Verification system for effectful programs
    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.

    checksums               rmd160  aa976d5d7e1836c932dedd0f719a509e4e5f3997 \
                            sha256  923488dff1927adfeb96b3ef2f9707fd9c5ec6589c41dd47d5ba8f01ae1aeac8 \
                            size    7598122
    github.tarball_from     archive

    depends_build-append    path:libexec/coreutils/libstdbuf.so:coreutils

    depends_lib-append      port:z3-fstar \
                            port:ocaml-sedlex \
                            port:ocaml-ppxlib \
                            port:ocaml-memtrace \
                            port:ocaml-mtime

    # Skip lib-fsharp: it requires dotnet and builds F# bindings we don't ship
    build.target            stage1 stage2
    build.args              ADMIT=1
    destroot.args           PREFIX=${destroot}${fstar.home}
    destroot.destdir        {}
    destroot.env-append     FSTAR_LINK_LIBDIRS=0

    post-patch {
        # Provide required links to z3 binaries
        xinstall -d ${worksrcpath}/bin
        ln -shf ${prefix}/libexec/z3-fstar/bin/z3-4.13.3 \
            ${worksrcpath}/bin/z3
        ln -shf ${prefix}/libexec/z3-fstar/bin/z3-4.8.5 \
            ${worksrcpath}/bin/z3-4.8.5
        ln -shf ${prefix}/libexec/z3-fstar/bin/z3-4.13.3 \
            ${worksrcpath}/bin/z3-4.13.3
    }

    # dune installs the binary as fstar.exe on all platforms
    fstar.bin               fstar.exe
    fstar.doc_dirs          examples

    post-destroot {
        # Provide links to z3 binaries (versioned names required by F* PATH discovery)
        ln -shf ../../z3-fstar/bin/z3-4.13.3 ${destroot}${fstar.home}/bin/z3
        ln -shf ../../z3-fstar/bin/z3-4.8.5 ${destroot}${fstar.home}/bin/z3-4.8.5
        ln -shf ../../z3-fstar/bin/z3-4.13.3 ${destroot}${fstar.home}/bin/z3-4.13.3

        # Provide compatibility symlinks for projects that expect F*'s
        # source layout
        set fstar_compat_home ${destroot}${fstar.home}/home
        xinstall -d -m 755 ${fstar_compat_home}
        foreach {fstar_src fstar_dest} {
            lib/fstar/ulib          ulib
            bin                     bin
        } {
            ln -shf \
                ../${fstar_src} \
                ${fstar_compat_home}/${fstar_dest}
        }
    }

    notes "
    F* requires z3-4.8.5 and z3-4.13.3 in your PATH.
    The z3-fstar port provides these.
    "
}

subport karamel {
    # KreMLin was renamed to KaRaMeL; sources are now at FStarLang/karamel
    github.setup            FStarLang karamel 86f99f08afa04ca792f9c4f64f24db4c0fdbc46c
    version                 2025.04.01
    epoch                   1

    license                 Apache-2
    description             A tool for extracting low-level F* programs to readable C code
    long_description        KaRaMeL (formerly KreMLin) is a tool that extracts an F* \
                            program to readable C code.

    checksums               rmd160  3bb15f59d3ea439ea52b27644d4dbe97bd166757 \
                            sha256  e80c43582f8b359fc218d34bbaeee2c9f9687094e0101dffad1b9e212f3921f8 \
                            size    498787
    github.tarball_from     archive

    compiler.c_standard     2011

    depends_lib-append      port:fstar \
                            path:libexec/coreutils/libstdbuf.so:coreutils \
                            port:ocaml-fix \
                            port:ocaml-wasm \
                            port:ocaml-visitors \
                            port:ocaml-uucp

    patchfiles-append       karamel/patch-lib-dune-add-str

    karamel.bin             krml
    karamel.doc_dirs        {}

    # PREFIX is baked into AutoConfig.ml at build time for hardcoded library paths
    build.args              PREFIX=${karamel.home} \
                            CC=${configure.cc} \
                            GIT_REV=${github.version}
    build.env-append        FSTAR_EXE=${prefix}/bin/fstar.exe \
                            OCAMLPATH=${fstar.home}/lib \
                            PATH=${prefix}/libexec/z3-fstar/bin:$env(PATH)

    test.run                no

    destroot.args           PREFIX=${destroot}${karamel.home}
    destroot.destdir        {}
    destroot.env-append     FSTAR_EXE=${prefix}/bin/fstar.exe \
                            OCAMLPATH=${fstar.home}/lib \
                            PATH=${prefix}/libexec/z3-fstar/bin:$env(PATH)

    post-destroot {
        # Provide a link to our fstar binary
        ln -shf ${fstar.home}/bin/${fstar.bin} ${destroot}${karamel.home}/bin/${fstar.bin}

        # Provide compatibility symlinks for projects that expect KaRaMeL's
        # source layout
        set karamel_compat_home ${destroot}${karamel.home}/home
        xinstall -d -m 755 ${karamel_compat_home}
        foreach {karamel_src karamel_dest} {
            lib/krml                kremlib
            lib/krml                krmllib
            lib/krml/runtime        runtime
            include                 include
            bin/krml                krml
            share/krml/misc         misc
        } {
            ln -shf \
                ../${karamel_src} \
                ${karamel_compat_home}/${karamel_dest}
        }
    }

    notes "
    To use this KaRaMeL toolchain with most standard Makefile-based F*/KaRaMeL\
    projects, pass KRML_HOME to the build as either an environment variable,\
    or make(1) parameter:

      KRML_HOME=\"${karamel.home}/home\"

    "
}

if {${subport} eq "kremlin" || ${subport} eq "fstar-devel" ||
    ${subport} eq "fstar_select" || ${subport} eq "kremlin_select"} {
    PortGroup           obsolete 1.0
}

subport kremlin {
    version             2022.06.08
    revision            1
    replaced_by         karamel
}

subport fstar-devel {
    version             20210824-b95d1ac
    revision            1
    replaced_by         fstar
}

subport fstar_select {
    version             1.3
    revision            1
}

subport kremlin_select {
    version             1.3
    revision            1
}

#
# Common destroot cleanup
#
if {${subport} eq "fstar" || ${subport} eq "karamel"} {
    post-destroot {
        # Clean up the installed files.
        fs-traverse {f} ${destroot}${fstar.subport.home} {
            switch -glob -- "[file tail $f] [file type $f]" {
                {*.checked file} {
                    # Bump the mtime of all *.checked files by 1 second.
                    #
                    # This ensures that fstar/karamel GNU make dependencies
                    # don't try to regenerate read-only *.checked files if they
                    # have an mtime identical to their corresponding fst/fsti
                    # input (yes, that happens)
                    set mtime [file mtime $f]
                    file mtime $f [expr {$mtime + 1}]
                }
                {.gitignore file} {
                    # Delete .gitignore files
                    delete $f
                }
            }
        }

        # Add versioned documentation symlinks to share/doc/
        xinstall -d -m 755 ${destroot}${prefix}/share/doc/${subport}
        foreach doc_dir ${fstar.subport.doc_dirs} {
            ln -sf \
                ${fstar.subport.home}/share/${subport}/${doc_dir} \
                ${destroot}${prefix}/share/doc/${subport}/${doc_dir}
        }

        # Add a versioned symlink to bin/
        ln -sf \
            ${fstar.subport.home}/bin/${fstar.subport.bin} \
            ${destroot}${prefix}/bin/${fstar.subport.bin}
    }
}
