# -*- 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 2026.03.21 v
github.tarball_from archive
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  ce5d9b8c41691a0f64fe2f7614b48805b014c1dc \
                    sha256  02e13310c1c7e7289663b67e79fab60ee7c3eb67dabd12c240828681740ef61e \
                    size    19639572

depends_lib         port:fstar \
                    port:karamel \
                    port:z3-fstar

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 \
                    PATH=${prefix}/libexec/z3-fstar/bin:$env(PATH)
# - EVERPARSE_USE_FSTAR_EXE / KRML_HOME: use the port-installed fstar and
#   karamel rather than the bundled opt/FStar and opt/karamel sources.
# - NO_PULSE: skip the optional Pulse-based components (we have no Pulse port).
# - z3_exe: short-circuit deps.Makefile's `which z3-4.13.3` lookup so it
#   doesn't try to download z3 and pass the download dir as a Make $<
#   prerequisite to fstar.exe.
build.args          FSTAR_EXE=${prefix}/bin/fstar.exe \
                    KRML_HOME=${karamel.home}/home \
                    EVERPARSE_USE_FSTAR_EXE=1 \
                    EVERPARSE_USE_KRML_HOME=1 \
                    NO_PULSE=1 \
                    z3_exe=${prefix}/libexec/z3-fstar/bin/z3-4.13.3
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 ...

"
