Downloads of v 0.9.4.0
F*: An ML-like language aimed at program verification
This package will install F* language with compatable version of z3.
It is recommended that you remove your z3 package and then install F*
More information on F* can be found at www.fstar-lang.org
The F* tutorial provides a first taste of verified programming in
F*, explaining things by example.
The F* wiki contains additional, usually more in-depth, technical
documentation on F*.
Editing F* code
You can edit F* code using your favourite text editor, but Emacs,
Atom, and Vim have extensions that add special support for F*,
including syntax highlighting and interactive development. More
details on editor support on the F* wiki .
Executing F* code
By default F* only verifies the input code, it does not compile or execute it.
To execute F* code one needs to translate it to either OCaml or F#, using
F*'s code extraction facility---this is invoked using the command line
--codegen OCaml or
--codegen FSharp. More details on
executing F* code on the F* wiki .
Community mailing list
The fstar-club mailing list is dedicated to F* users. Here is where
all F* announcements are made to the general public (e.g. for
releases, new papers, etc) and where users can ask questions, ask for
help, discuss, provide feedback, announce jobs requiring at least 10
years of F* experience, etc.
Users can also ask questions on the
#fstar Slack channel at
< http://fpchat.com/ >
Please report issues using the F* issue tracker on GitHub.
Before filing please use search to make sure the issue doesn't already exist.
We don't maintain old releases, so if possible please use the
online F* editor or directly the GitHub sources to check
that your problem still exists on the
The F* for the masses blog is also expected to become an important
source of information and news on the F* project.
This new variant of F* is released under the Apache 2.0 license;
LICENSE for more details.
To install F* language, run the following command from the command line or from PowerShell:
C:\> choco install fstar
To upgrade F* language, run the following command from the command line or from PowerShell:
C:\> choco upgrade fstar
$ErrorActionPreference = 'Stop'; # stop on all errors Install-ChocolateyZipPackage -packageName 'fstar' -UnzipLocation $(Split-Path -Parent $MyInvocation.MyCommand.Definition) -Url64 'https://github.com/FStarLang/FStar/releases/download/V0.9.4.0/fstar_0.9.4.0_Windows_x64.zip' -checksum64 '3F5EFB7F99F371C5A842C9D7F2F42C741AC786F788B00F77A6DB606E4AE51189' -checksumType64 'sha256'
Virus Scan Results
- msvcp100.dll (5bb420fbe283) - ## / 61 - Log in or click on link to see number of positives
- msvcr100.dll (1d1a1ae540ba) - ## / 67 - Log in or click on link to see number of positives
- FStar.0.9.4.0.nupkg (fc2a52480e1e) - ## / 57 - Log in or click on link to see number of positives
- FSharp.PowerPack.Compatibility.dll (c8c79989f8b6) - ## / 55 - Log in or click on link to see number of positives
- FSharp.PowerPack.dll (21c1e14535c4) - ## / 56 - Log in or click on link to see number of positives
- fstar.exe (3a78ead053f8) - ## / 62 - Log in or click on link to see number of positives
- libgmp-10.dll (e4f8b81ea927) - ## / 62 - Log in or click on link to see number of positives
- z3.exe (9307083bfcd0) - ## / 57 - Log in or click on link to see number of positives
- fstar_0.9.4.0_Windows_x64.zip (3f5efb7f99f3) - ## / 55 - Log in or click on link to see number of positives
This package has no dependencies.
This is a big release with lots of important changes compared to v0.9.2.0 exactly a year ago:
- Predicative hierarchy of universes with universe polymorphism
- Uniform syntax between expressions and types allowing rich type-level computation
- Dijkstra Monads for Free (https://www.fstar-lang.org/papers/dm4free/)
- Extraction to C via KreMLin (https://github.com/FStarLang/kremlin)
- New parser based on Menhir
- New pretty printer for surface syntax and
- Changed default effect to Tot
- Strict positivity check for inductives
- New synatax for inductive type projectors and discriminators
- Better semantics for module open and support for local opens
- Better dependency analysis
- Better error locations for Z3 failures
- Replaced Z3 timeouts with machine independent resource limits
- Cleaned up libraries and examples (a bit)
- Improvements to interactive mode
- Docker builds
- Fixed a ton of bugs (262 closed GitHub issues)
|F* language 0.9.6.001||73||Wednesday, October 17, 2018||approved|
|F* language 0.9.6.0||40||Tuesday, August 28, 2018||approved|
|F* language 0.9.5.0||274||Tuesday, September 5, 2017||approved|
|F* language 0.9.4.0||222||Wednesday, May 3, 2017||approved|
Discussion for the F* language Package
- This discussion is only about F* language and the F* language package. If you have feedback for Chocolatey, please contact the google group.
- This discussion will carry over multiple versions. If you have a comment about a particular version, please note that in your comments.
- The maintainers of this Chocolatey Package will be notified about new comments that are posted to this Disqus thread, however, it is NOT a guarantee that you will get a response. If you do not hear back from the maintainers after posting a message below, please follow up by using the link on the left side of this page or follow this link to contact maintainers. If you still hear nothing back, please follow the package triage process.
- Tell us what you love about the package or F* language, or tell us what needs improvement.
- Share your experiences with the package, or extra configuration or gotchas that you've found.
- If you use a url, the comment will be flagged for moderation until you've been whitelisted. Disqus moderated comments are approved on a weekly schedule if not sooner. It could take between 1-5 days for your comment to show up.