Consider adding this build step:
build() {
cd fstar
PATH=$PWD/bin:$PATH make -C ulib
}
Without it, Fstar shows this warning:
/opt/fstar/ulib/prims.fst(0,0-0,0): (Warning 241) Unable to load /opt/fstar/ulib/prims.fst.checked since checked file /opt/fstar/ulib/prims.fst.checked does not exist; will recheck /opt/fstar/ulib/prims.fst (suppressing this warning for further modules)
However, it takes a lot of time and RAM to pre-compile the standard library, as well as an extra ~150 MB of disk space, so it may not be worth it.
What version of ocaml was this compiled with?
To make sure that fstar actually uses the bundled z3 (and to not get the warning about using the wrong z3 version), use the following PKGBUILD:
# Maintainer: Mort Yao <soi@mort.ninja>
pkgname=fstar-bin
pkgver=0.9.6.0
pkgrel=2
pkgdesc='A Higher-Order Effectful Language Designed for Program Verification'
url='<https://fstar-lang.org/>'
license=('Apache')
arch=('x86_64')
depends=()
provides=('fstar')
conflicts=('fstar' 'fstar-git')
source=("<https://github.com/FStarLang/FStar/releases/download/v>${pkgver}/fstar_${pkgver}_Linux_x86_64.tar.gz")
md5sums=('789116db65f7fde743702ec641f7ccee')
package() {
cd "fstar"
install -d -m755 $pkgdir/opt/fstar $pkgdir/usr/bin
cp -r * $pkgdir/opt/fstar
# Instead of symlinking, create a wrapper script
# ln -s /opt/fstar/bin/fstar.exe $pkgdir/usr/bin/fstar
echo '#!/bin/bash' > $pkgdir/usr/bin/fstar
echo '/opt/fstar/bin/fstar.exe --smt /opt/fstar/bin/z3 "$@"' >> $pkgdir/usr/bin/fstar
chmod +x $pkgdir/usr/bin/fstar
}
Could you release this fix @soimort ?
