# -*- 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                everparse
github.setup        project-everest everparse 69d6c064ea34d0f5458db94ba1204795db9496dc
github.tarball_from archive
version             2025.01.25
epoch               1
revision            1

categories          devel
maintainers         {landonf @landonf} openmaintainer
license             Apache-2
description         A verified secure parser framework for F*.
long_description    EverParse provides LowParse, verified-secure F*/Low* parser combinator library, and \
                    QuackyDucky, an untrusted compiler for generating verified secure parsers from a \
                    message format specification.

checksums           rmd160  a3dee7f6566f6f2927d8a4330f9c4fcfed9d0600 \
                    sha256  51042c4e4f78204acefb1ecf226077a25700ae6d490dd5f725d3ec639e1a9d39 \
                    size    18977419

depends_lib         port:fstar \
                    port:karamel

depends_build       port:ocaml \
                    port:ocaml-batteries \
                    port:ocaml-dune \
                    port:ocaml-hex \
                    port:ocaml-menhir \
                    port:ocaml-ppx_deriving_yojson \
                    port:ocaml-process \
                    port:ocaml-re \
                    port:ocaml-sexplib \
                    port:ocaml-sha \
                    port:ocaml-yojson

options             fstar.home \
                    karamel.home

default fstar.home      {${prefix}/libexec/fstar}
default karamel.home    {${prefix}/libexec/karamel}

use_configure       no

# src/3d/ocaml/Makefile uses CRLF line endings.
post-extract {
    reinplace "s|\r||g" src/3d/ocaml/Makefile
}

build.type          gnu
build.env-append    FSTAR_EXE=${prefix}/bin/fstar.exe \
                    OCAMLPATH=${fstar.home}/lib \
                    OTHERFLAGS=--admit_smt_queries\ true
build.args          FSTAR_EXE=${prefix}/bin/fstar.exe \
                    KRML_HOME=${karamel.home}/home
build.target        3d quackyducky

test.run            no

destroot {
    # Create EVERPARSE_HOME layout compatible with src/package/package.sh
    set everparse_root      ${prefix}/libexec/everparse
    set everparse_bin       ${everparse_root}/bin
    set everparse_lib       ${everparse_root}/lib
    set everparse_lib_3d    ${everparse_root}/lib/3d
    set everparse_src       ${everparse_root}/src

    xinstall -d \
        ${destroot}${everparse_lib}    \
        ${destroot}${everparse_lib_3d} \
        ${destroot}${everparse_bin}

    xinstall \
        ${worksrcpath}/bin/qd.exe \
        ${destroot}${everparse_bin}/qd.exe

    xinstall \
        ${worksrcpath}/bin/3d.exe \
        ${destroot}${everparse_bin}/3d.exe

    foreach {ep_src ep_dst} [list \
        lowparse                    ${everparse_lib}    \
        3d/prelude                  ${everparse_lib_3d} \
        3d/EverParseEndianness.h    ${everparse_lib_3d} \
        3d/noheader.txt             ${everparse_lib_3d} \
        3d/copyright.txt            ${everparse_lib_3d} \
    ] {
        if {[file exists ${worksrcpath}/src/${ep_src}]} {
            copy ${worksrcpath}/src/${ep_src} ${destroot}${ep_dst}
        }
    }

    fs-traverse {f} ${destroot}${everparse_lib} {
        switch -glob -- "[file tail $f] [file type $f]" {
            {.hints link}       -
            {.gitignore file}   -
            {.depend file}      -
            {Makefile file}     { delete $f }
        }
    }

    # src/package/package.sh expects a 'src' directory
    ln -sf lib                  ${destroot}/${everparse_src}

    # Symlink the binaries into ${prefix}/bin
    ln -sf ${everparse_bin}/qd.exe  ${destroot}${prefix}/bin/quackyducky
    ln -sf quackyducky              ${destroot}${prefix}/bin/qd
    ln -sf ${everparse_bin}/3d.exe  ${destroot}${prefix}/bin/quackyducky-3d
    ln -sf quackyducky-3d           ${destroot}${prefix}/bin/qd-3d
}

notes "
EverParse 3D is invoked through the quackyducky-3d wrapper and requires
F* and KaRaMeL to be in PATH at runtime:

  PATH=${fstar.home}/bin:${karamel.home}/home/bin:\$PATH quackyducky-3d ...

"
