Search Criteria
Package Details: fstar 0.9.7.0-2
| Git Clone URL: | https://aur.archlinux.org/fstar.git (read-only, click to copy) |
|---|---|
| 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.000000 |
| First Submitted: | 2016-03-13 03:04 (UTC) |
| Last Updated: | 2019-10-20 14:49 (UTC) |
Dependencies (16)
- z3-gitAUR
- ocaml (make)
- ocaml-batteriesAUR (ocaml-batteries-gitAUR) (make)
- ocaml-fileutilsAUR (make)
- ocaml-findlib (make)
- ocaml-menhirAUR (make)
- ocaml-migrate-parsetreeAUR (ocaml-migrate-parsetree-gitAUR) (make)
- ocaml-num (make)
- ocaml-pprintAUR (make)
- ocaml-ppx_derivingAUR (ocaml-ppx_deriving-gitAUR) (make)
- ocaml-ppx_deriving_yojson (ocaml-ppx_deriving_yojson-gitAUR) (make)
- ocaml-process (ocaml-process-gitAUR) (make)
- ocaml-stdint (ocaml-stdint-gitAUR) (make)
- ocaml-yojsonAUR (ocaml-yojson-gitAUR, ocaml-yojsonAUR) (make)
- ulex-gitAUR (make)
- zarith (ocaml-zarith) (make)
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 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 (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?
[1] https://wiki.archlinux.org/index.php/Arch_package_guidelines#Package_versioning
1 2 Next › Last »