Package Details: fstar

Git Clone URL: (read-only, click to copy)
Package Base: fstar
Description: A Higher-Order Effectful Language Designed for Program Verification
Upstream URL:
Keywords: F* ML verification
Licenses: Apache
Conflicts: fstar-bin, fstar-git
Provides: fstar
Submitter: soimort
Maintainer: soimort
Last Packager: soimort
Votes: 3
Popularity: 0.000000
First Submitted: 2016-03-13 03:04 (UTC)
Last Updated: 2019-10-20 14:49 (UTC)

Dependencies (16)

Required by (1)

Sources (2)

Latest Comments

1 2 Next › Last »

Poscat commented on 2020-02-10 14:27 (UTC)

Are there any reasons to use z3-git instead of z3?

soimort commented on 2019-10-20 14:53 (UTC)

Patch applied. Should be fixed now.

catalin.hritcu commented on 2019-10-20 06:10 (UTC)

Cherry picking this commit should fix it even on 4.08: 8afbc109bd3d5d490b0f628e9f4645595d3a62d8 Can you try?

soimort commented on 2019-10-19 21:03 (UTC)

It seems to be fixed in fstar's master branch though. So for now it's only possible to use fstar-git (until another stable release comes out)

soimort commented on 2019-10-19 21:01 (UTC)

It turns out that the release tarball of v0.9.7.0-alpha1 won't build under ocaml >=4.08.

In ( ) there's a pattern match case for File_not_found on Dynlink.error, but this File_not_found has been removed since OCaml 4.08 (commit ).

File "src/tactics/ml/", line 18, characters 6-20: 18 | | File_not_found _ -> "File_not_found" ^^^^^^^^^^^^^^ Error: This variant pattern is expected to have type Dynlink.error The constructor File_not_found does not belong to type Dynlink.error

catalin.hritcu commented on 2019-10-19 07:04 (UTC)

Packing it as v0.9.7.0 would be great, thank you.

soimort commented on 2019-10-18 23:05 (UTC)

Thanks for the clarification. If there will be no more releases before 1.0, then I can at least try to pack it as v0.9.7.0 (omitting the alpha).

catalin.hritcu commented on 2019-10-13 12:07 (UTC)

Since otherwise no, there is no plan for another release until the 1.0 release in spring.

catalin.hritcu commented on 2019-10-13 11:57 (UTC)

We messed up the naming on this one. It's not less stable than any of our other F* releases. Can we pack it despite the alpha name?

soimort commented on 2019-10-13 11:27 (UTC)

Arch package guidelines [1] do not encourage the use of non-stable releases (e.g., alpha) in general, so I can't make a package for v0.9.7.0-alpha1 at the moment.

@catalin.hritcu Any chance to get a new stable release (v0.9.7.0) at upstream?