You've already forked macports-ports
mirror of
https://github.com/macports/macports-ports.git
synced 2026-07-12 18:20:25 -07:00
Paul Guyot
a776172ef6
Version updates required for 5.5: - ocaml-merlin to 5.8-505 - ocaml-camlp4 to 5.5+1 - ocaml-js_of_ocaml to 6.4.0 - ocaml-batteries to 3.11.0 Removed ocaml-ppx_tools which is dead upstream and superseded by ppxlib. Signed-off-by: Paul Guyot <pguyot@kallisys.net>
283 lines
10 KiB
Tcl
283 lines
10 KiB
Tcl
# -*- 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 2026.03.24 v
|
|
epoch 1
|
|
revision 2
|
|
|
|
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 bb8fb959aa41176cc3a21955568aa5cf8629a1b3 \
|
|
sha256 64a898ae1d0089315f607c47d9d708895748f86a009ee0d65eed9d8d433cf518 \
|
|
size 7548587
|
|
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 c96d44beee92853a4cc8d9c4bc84e8eb452379f4
|
|
version 2026.03.25
|
|
epoch 1
|
|
revision 2
|
|
|
|
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 10280a530b0540b48f818d3ef6b50ebd3aad0235 \
|
|
sha256 0740ee6d6179a99d46d59002f59a545a7c8811bae7d2e203153b71d7db3e306c \
|
|
size 516532
|
|
github.tarball_from archive
|
|
|
|
compiler.c_standard 2011
|
|
|
|
depends_build-append port:gtime
|
|
|
|
depends_lib-append port:fstar \
|
|
path:libexec/coreutils/libstdbuf.so:coreutils \
|
|
port:ocaml-fix \
|
|
port:ocaml-wasm \
|
|
port:ocaml-visitors \
|
|
port:ocaml-uucp
|
|
|
|
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 3
|
|
replaced_by karamel
|
|
}
|
|
|
|
subport fstar-devel {
|
|
version 20210824-b95d1ac
|
|
revision 3
|
|
replaced_by fstar
|
|
}
|
|
|
|
subport fstar_select {
|
|
version 1.3
|
|
revision 2
|
|
}
|
|
|
|
subport kremlin_select {
|
|
version 1.3
|
|
revision 2
|
|
}
|
|
|
|
#
|
|
# 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}
|
|
}
|
|
}
|