# -*- 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 "kremlin"} {
    PortGroup               ocaml 1.1

    depends_build           port:ocaml-ocamlbuild \
                            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 kremlin)
    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]}]
        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 34320b047539629c53debda640c50b97d6e556fd
    version                 2022.06.08
    epoch                   1

    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.

    checksums               rmd160  d2d10d63648d67da5f25c13a1893c6519cd6f3cb \
                            sha256  cd3ce5281fe6f1dcf155ee0e83417c9a52c406039b7ebf801ed7f5abf2ed1252 \
                            size    8159524
    github.tarball_from     archive

    # destroot requires ginstall from coreutils
    depends_build-append    path:libexec/coreutils/libstdbuf.so:coreutils

    depends_lib-append      port:z3-fstar \
                            port:gmp \
                            port:realpath \
                            port:ocaml-sedlex \
                            port:ocaml-ppxlib

    patchfiles              fstar/patch-z3-path \
                            fstar/patch-fix-get_exec_dir \
                            fstar/patch-tests_machine__integers_Makefile

    fstar.doc_dirs          examples \
                            contrib \
                            tutorial

    ocaml.package_dir   ${fstar.home}/bin

    post-patch {
        # Fix-up paths to MacPorts' binaries
        reinplace -E "s|@PREFIX@|${prefix}|g" \
            src/basic/ml/FStar_Compiler_Util.ml

        # Fix invalid use of (now-removed) `FSTAR_ALWAYS`
        reinplace {s|\$(FSTAR_ALWAYS)|$(FSTAR)|g} \
            examples/crypto/Makefile

        # Don't try to use `git` to fetch the commit
        reinplace "s|^COMMIT =.*|COMMIT = ${git.branch}|g" \
            src/ocaml-output/Makefile

        # Fix up the z3 path in the generated code, too.
        #
        # A patch file would be more of a headache here, as the autogenerated variable names
        # result in the patches not applying cleanly across updates.
        reinplace {s|FStar_Platform.exe "z3"|FStar_String.op_Hat fstar_bin_directory (FStar_Platform.exe "/z3")|g} \
            src/ocaml-output/FStar_Options.ml

        # Provide required link to z3 binary
        ln -shf ${prefix}/libexec/z3-fstar/bin/z3 \
            ${worksrcpath}/bin/z3
    }

    # XXX TODO:
    #
    # A number of F* test cases actually depend on KreMLin (while KreMLin depends
    # on F*).
    #
    # We need to find a way to break this circular dependency, either by disabling
    # the given tests (and running them in KreMLin's test target?), or actually
    # building KreMLin as part of F*, or ... (?).
    #
    # Current (as of this writing) list of examples in fstar-devel that depend on KreMLin:
    #   - csl
    #   - kv_parsing
    #   - low-level
    #   - miniparse
    #   - tactics
    #   - typeclasses
    depends_test        port:${kremlin.port}
    test.run            yes
    test.env            FSTAR_HOME=${worksrcpath} \
                        KREMLIN_HOME=${kremlin.home}/home \
                        KRML_HOME=${kremlin.home}/home
    test.dir            ${worksrcpath}
    test.target         all
    test.args           -C examples \
                        -j ${build.jobs}

    destroot.args       PREFIX=${destroot}${fstar.home}
    post-destroot {
        # Remove intermediate build directories
        foreach dir {ml tactics_ml} {
            delete ${destroot}${fstar.home}/lib/fstar/${dir}/_build
        }

        # Drop the '.exe' file extension inserted by the build system
        move \
            ${destroot}${fstar.home}/bin/${fstar.bin}.exe \
            ${destroot}${fstar.home}/bin/${fstar.bin}

        # Provide an fstar.exe -> fstar compatibility symlink
        ln -shf fstar ${destroot}${fstar.home}/bin/${fstar.bin}.exe

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

        # 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
            bin                     bin
            share/fstar/examples    examples
            share/fstar/contrib     ucontrib
        } {
            ln -shf \
                ../${fstar_src} \
                ${fstar_compat_home}/${fstar_dest}
        }
    }

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

      FSTAR_HOME=\"${fstar.home}/home\"

    "
}

subport kremlin {
    github.setup            FStarLang kremlin 28a9d4a64fbbdcd1fe12c07e65d4b82e63bb5106
    version                 2022.06.08
    epoch                   1

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

    checksums               rmd160  6316b264b4aec908e452ccec8377a7148d753961 \
                            sha256  63d1444da6361dfe2f2ca7a555eab3265f06eede4d1b718bcd032d7054cb1667 \
                            size    902280
    github.tarball_from     archive

    compiler.c_standard     2011

    depends_build-append    port:gsed

    depends_lib-append      port:${fstar.port} \
                            path:libexec/coreutils/libstdbuf.so:coreutils \
                            port:ocaml-fix \
                            port:ocaml-wasm \
                            port:ocaml-visitors \
                            port:ocaml-sedlex

    depends_test-append     port:ocaml-ctypes

    patchfiles              kremlin/patch-clang-driver-options \
                            kremlin/patch-fstar-discover-path \
                            kremlin/patch-fstar-driver-no-lax \
                            kremlin/patch-test_system_system.h

    kremlin.bin             krml
    kremlin.doc_dirs        examples

    options                 kremlin.cc \
                            kremlin.ccpath

    kremlin.ccpath          {${configure.compiler}}

    # XXX TODO: We really need a ${configure.compiler.family}
    if {[string match *clang* ${configure.compiler}]} {
        kremlin.cc clang
    } elseif {[string match *gcc* ${configure.compiler}]} {
        kremlin.cc gcc
    } else {
        # Assume GCC-like behavior
        kremlin.cc gcc
    }

    # If we specify PREFIX=${kremlin.home} in our build.args, a fixed path to
    # kremlin.home is hard-coded by kremlin's build system in AutoConfig.ml.
    #
    # If we exclude it, we can rely on auto-detection of kremlin.home, which
    # allows us to run krml in-place (e.g. for tests)
    build.args              CC=${configure.cc} \
                            FSTAR_HOME=${fstar.home}/home \
                            KRML_HOME=${worksrcpath}

    build.env-append        PATH=${workpath}/compiler-bin:$env(PATH) \
                            "KRML_ARGS=-cc ${kremlin.cc}"

    post-patch {
        file mkdir "${workpath}/compiler-bin"

        set krml_cc ${workpath}/compiler-bin/${kremlin.cc}
        xinstall -m 755 ${filespath}/krml-cc.in ${krml_cc}
        reinplace "s|@CONFIGURE_CC@|${configure.cc}|g" ${krml_cc}

        # XXX: Must be kept in-sync with Driver.detect_gnu()
        foreach {cc_major} {5 6 7 8 9 10} {
            ln -shf ${krml_cc} ${krml_cc}-${cc_major}
        }
    }

    test.run                yes
    test.args               {*}${build.args} \
                            -j ${build.jobs}
    test.env-append         PATH=${workpath}/compiler-bin:$env(PATH) \
                            "KOPTS=-cc ${kremlin.cc}"

    destroot.args           PREFIX=${destroot}${kremlin.home} \
                            FSTAR_HOME=${fstar.home}/home \
                            KRML_HOME=${worksrcpath}

    post-destroot {
        # KreMLin-specific cleanup up the installed files.
        fs-traverse {f} ${destroot}${fstar.subport.home} {
            switch -glob -- "[file tail $f] [file type $f]" {
                {*.d file} {
                    # Delete KreMLin's GCC dependency (-MD) files; these contain the build's
                    # worksrcpath, and even with the correct paths, would not be useful to
                    # library consumers
                    delete $f
                }
            }
        }

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

        # Provide compatibility symlinks for projects that expect KreMLin's
        # source layout
        set kremlin_compat_home ${destroot}${kremlin.home}/home
        xinstall -d -m 755 ${kremlin_compat_home}
        foreach {kremlin_src kremlin_dest} {
            lib/krml                kremlib
            lib/krml                krmllib
            lib/krml/runtime        runtime
            include                 include
            bin/krml                krml
            share/krml/misc         misc
        } {
            ln -shf \
                ../${kremlin_src} \
                ${kremlin_compat_home}/${kremlin_dest}
        }
    }

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

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

    "
}

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

subport kremlin-devel {
    PortGroup           obsolete 1.0
    version             20210824-b95d1ac
    revision            1
    replaced_by         fstar
}

subport fstar_select {
    PortGroup           obsolete 1.0
    version             1.3
    revision            1
}

subport kremlin_select {
    PortGroup           obsolete 1.0
    version             1.3
    revision            1
}

#
# Common destroot cleanup
#
if {${subport} eq "fstar" || ${subport} eq "kremlin"} {
    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/kremlin 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}
    }
}