Package Details: fstar-bin 2023.09.03-2

Git Clone URL: https://aur.archlinux.org/fstar-bin.git (read-only, click to copy)
Package Base: fstar-bin
Description: A Higher-Order Effectful Language Designed for Program Verification
Upstream URL: https://fstar-lang.org/
Keywords: F* ML verification
Licenses: Apache
Conflicts: fstar, fstar-git
Provides: fstar
Submitter: soimort
Maintainer: soimort (hnns)
Last Packager: hnns
Votes: 4
Popularity: 0.000000
First Submitted: 2016-03-13 03:29 (UTC)
Last Updated: 2024-05-31 11:01 (UTC)

Latest Comments

mb64 commented on 2020-09-23 04:17 (UTC)

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.

NobbZ commented on 2018-07-11 12:31 (UTC)

What version of ocaml was this compiled with?

soimort commented on 2018-05-29 12:47 (UTC)

@Tyilo Updated. Thanks!

Tyilo commented on 2018-05-27 21:22 (UTC)

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 ?