FStar

FStar copied to clipboard

Huge verification freeze (performance regression)

2

[Here's an example](https://gist.github.com/hacklex/07821bf0a294e2e2810146d1510eedeb) extracted from my algebra library FStar freezes for minutes before finally accepting the fraction field definition.

hacklex

The automatic introduction of `exists_` and `pure` mechanism in Steel relies on the Steel tactic identifying lemmas by their attributes: 1. It finds all lemmas tagged `solve_can_be_split_lookup`. 2. Among them,...

tahina-pro

Hi, This PR adds reflection for quotations, allowing for static or dynamic quotations and anti-quotations to be inspected and constructed from the reflection API. This feature is particularly useful for...

W95Psp

Publishing F* as nuget

17

### IDEA With weekly binary packages fixed (https://github.com/FStarLang/FStar/pull/2275), it should be quite simple to extend the build process to also publish a nuget package. I have some bespoke powershell script...

mateuszbujalski

QuasiQuotes for F*

2

Hi, This (draft) PR adds some support for quasi-quotes in F*, with a syntax similar to [Haskell's quasi-quotes](https://wiki.haskell.org/Quasiquotation). It's quite experimental for now, and I wanted to have some feedback...

W95Psp

Without `open FStar.Mul` complete novice would struggle to understand why perfectly valid example does not work in sandbox.

kant2002

Expose term parsing in tactics via `string_to_term`

6

Hello, Here is a PR that brings term parsing to tactics, via a primitive `string_to_term`, that takes a string and an environement. I hope to write a sort of REPL...

W95Psp

Hi, This PR makes the following record expression and type declaration valid: ```fstar type foo = { ( ^ ): int } let _: foo = { ( ^ )...

W95Psp

Improvements over let operators

1

Hi, Following the conversation in #1868, this PR improves the implementations of let operators in the following ways: - simplify the parser by letting `let` and `and` be treated as...

W95Psp

Parser: accept `f {field = ...}` (no need for `f ({field = ...})` anymore)

2

Hi, This PR changes a bit the parser rules related to function application so that the expression `f {foo = 123}` is now allowed. Previously, `f {foo = 123}` was...

W95Psp