Package Details: fstar 0.9.7.0-2

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

Latest Comments

1 2 Next › Last »

soimort commented on 2019-10-20 14:53

Patch applied. Should be fixed now.

catalin.hritcu commented on 2019-10-20 06:10

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

soimort commented on 2019-10-19 21:03

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

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

In FStar_Tactics_Load.ml ( https://github.com/FStarLang/FStar/blob/f3f7d15cfb2ca329ce2560d8190fdf2d84b683ab/src/tactics/ml/FStar_Tactics_Load.ml ) 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 https://github.com/ocaml/ocaml/commit/6526a0c3d9457705fa5403650f0810e7cc2a2965 ).

File "src/tactics/ml/FStar_Tactics_Load.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

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

soimort commented on 2019-10-18 23:05

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

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

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

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?

[1] https://wiki.archlinux.org/index.php/Arch_package_guidelines#Package_versioning

soimort commented on 2017-10-29 17:01

I noticed that one of the dependencies, ocaml-batteries, requires:
ocaml>=4.03

From my knowledge, (on Arch) the package `ocamlbuild` was split from ocaml since 4.03.0, so any PKGBUILD that requires it won't work for a rusty Arch system (since the dependency `ocamlbuild` simply doesn't exist prior to ocaml 4.03). I think forcing ocaml>=4.03 is probably a good way to ensure that the ocamlbuild package exists on users' Arch mirror so as to save them from potential troubles.