FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
This pushes the CI base image to the `ghcr.io` container registry instead of storing it locally on the build machine. The container registry is publicly accessible, so `make docker-ci` works...
This reduces the dependencies that clients take on just for mentioning the char type or a character literal. Currently this brings in a lot to just check a module with...
This PR changes the parser to require fewer parentheses: 1. When using lambdas as last function argument: `foo fun x -> x + 1` 2. Around `assume` and `assert` arguments:...
Some work in progress to make dependency graphs more useful. Mostly 1) distinguish between interface and implementation instead of just coallescing the modules, and 2) do not bring into the...
This tactic deprecates (in fact removes) the `mk_class` tactic in typeclasses and instead uses the MkProjectors tactic all classes too, by default. This tactic is meant to generate projectors that...
module ExceptionBadErrorMessage exception E1 exception E2 let f () = let n = (try 1 with E1 -> 2 | E2 -> 3 | _ -> 4) in n reports...
module ExceptionNamesBug /// It would be nice if it did not warn 331 here as names are documentation. exception One of (name: string) and turning it down may cause other...
I did try to export [F* source code](https://github.com/kant2002/fstarsample/blob/master/lens/Lens.fst) to F# and was shown following error messages in .NET 6 and up F* Code ``` let center : lens circle point...
This makes fstar try to find a file named `fstar.include` in every directory we are explicitly including (with `--include`). That file contains the names of more directories that F* should...