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: None
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 (0)

Sources (2)

Latest Comments

« First ‹ Previous 1 2

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

soimort commented on 2017-10-29 17:01 (UTC)

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.

catalin.hritcu commented on 2017-10-29 13:00 (UTC)

@soimort One more comment is related to the minimum OCaml version that could be 4.02.3. That's what most F* developers use (don't ask, windows related issues).

catalin.hritcu commented on 2017-10-24 20:40 (UTC)

@soimort Thank you for the fixes. ulex seems to be only used for Steps 1 and 2 (generating a lexer) so if you now do only Step 3 it's not needed. In fact, some of the other dependencies are not needed either if you only do Step 3, like ocaml-menhir. The dependencies for only Step 3 and runtime are listed earlier in INSTALL.md https://github.com/FStarLang/FStar/blob/master/INSTALL.md#testing-a-binary-package $ opam install ocamlfind batteries stdint zarith

soimort commented on 2017-10-24 18:58 (UTC)

@catalin.hritcu Thank you for your comments. 0. I have added the missing dependencies (except ulex since v0.9.5.0 seems to compile without it, could that be problematic?) 1. Now PKGBUILD will use the OCaml snapshot directly. 2. As suggested, I've turned the runtime dependency into z3-git (instead of z3). Just as a side note, currently the `fstar-git` package doesn't build with Arch's OCaml 4.05 due to this: https://github.com/FStarLang/FStar/pull/1302 which needs to get patched in the upstream anyways.

catalin.hritcu commented on 2017-10-23 05:55 (UTC)

@soimort After installing `ocaml-menhir` the next missing dependency is `stdint`, and there doesn't seem to be any Arch package for this? + ocamlfind ocamldep -package stdint -package batteries -package zarith -modules ulib/ml/FStar_Int16.ml > ulib/ml/FStar_Int16.ml.depends ocamlfind: Package `stdint' not found For a complete list of dependencies please check out INSTALL.md: https://github.com/FStarLang/FStar/blob/master/INSTALL.md#instructions-for-all-oses More precisely this is the list currently: $ opam install ocamlbuild ocamlfind batteries stdint zarith yojson fileutils pprint menhir ulex So I expect next missing package problems I get to be fileutils and ulex

catalin.hritcu commented on 2017-10-22 21:31 (UTC)

@soimort Thanks a lot for the package. We generally encourage people to use OPAM, but it's always good to have other alternatives. A couple of comments about the package: 0. The build failed for me after a lot of time spent installing dependencies and compiling F* (Steps 1 and 2 for now). The culprit seems to be a missing dependency on `ocaml-menhir`. Without this `src/ocaml-output/Makefile` fails with `Correct version of menhir not found (needs a version newer than 20161115)` 1. You are doing a full bootstrapping round via F#, but that's not strictly necessary, since you could build directly from the OCaml snapshot in `src/ocaml-ocaml-output` (only Step 3). This would be faster and would remove the `fsharp` dependency. 2. You could consider to turn the Z3 dependency into just `z3-git`, since the last official Z3 release 4.5.0 is 1 year old and has many known problems and for some examples we need more recent Z3 versions. (The versions we use are usually here: https://github.com/FStarLang/binaries/tree/master/z3-tested) On the other hand, `z3-git` increases the build time.

soimort commented on 2017-02-22 03:16 (UTC)

I've added the package ocaml-pprint to AUR. Hope this helps.

farao commented on 2017-02-21 00:05 (UTC)

I have problems installing the package, it shows as error: + ocamlfind ocamldep -package batteries -package zarith -package yojson -package pprint -modules src/fstar/ml/main.ml > src/fstar/ml/main.ml.depends ocamlfind: Package `pprint' not found I already installed the two packages before (zarith and yojson) manually with other aur-packages (I'm wondering why they are not in the dependencies?) but I can't find an aur package for the pprint ocaml library. I installed it via opam, but the error remains (I guess because opam just installes it for my user, not globally for the whole system?). How can I solve this?

« First ‹ Previous 1 2