Package Details: fstar-bin 2023.09.03-1

Git Clone URL: (read-only, click to copy)
Package Base: fstar-bin
Description: A Higher-Order Effectful Language Designed for Program Verification
Upstream URL:
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-30 08:08 (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 <>

pkgdesc='A Higher-Order Effectful Language Designed for Program Verification'
conflicts=('fstar' 'fstar-git')

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 ?