FStar

FStar copied to clipboard

The following actions failed │ λ build conf-python-2-7 1.2

6

Hello， when I run the following command，it occur some error， could you give me some suggests? $ opam pin add fstar --dev-repo [NOTE] Package fstar is already pinned to git://github.com/FStarLang/FStar...

Chaos-Crypto

Parsing error with record update

1

Hi all -- is the following undesired behavior? ``` module Test type t = { x : nat; y : nat} // Parses correctly let tst (f : t ->...

gancherj

I have noticed the following behavior with error messages: Construct an inductive type `t`, and have the constructors return `squash t` instead of `t`. (This is an easy thing to...

gancherj

Cannot match on negative integer literals

2

There doesn't seem to be a way to match on a negative integer. Here's a small reproduction: ``` module ExampleMatch let sign = (z:int{z = 0 \/ z = (-1)...

mgritter

Steel work items

1

Recapping here the list of Steel work items **Code Refactoring** - [x] Replace SteelAtomic unobservable and SteelAtomic observable by SteelGhost and SteelAtomic - [ ] Remove the quantification on invariant_names...

R1kM

F* seems to diverge on this example consuming a lot of memory

1

https://github.com/FStarLang/FStar/blob/master/ulib/experimental/Steel.FractionalAnchoredPreorder.fst#L485

nikswamy

This may be related to the unfolding behavior of vprops. Could it be remedied by using strict_on_arguments? ``` module AVP open FStar.Ghost open Steel.FractionalPermission open Steel.Memory open Steel.Effect.Atomic open Steel.Effect...

nikswamy

When writing Steel specifications in selector style, the specifications themselves need to be framed. Consider this: First some general scaffolding for a test case, defining an abstract indexed vprop `p...

nikswamy

It seems that defining actions directly in an `effect` or `layered_effect` results in an error message. Below is an example which works: ```fstar module MWE let wpost a = a...

TheoWinterhalter

I ran across some behavior that’s surprising to me. The example below fails with the message `(Error 54) (*?u47*) _ is not equal to the expected type log': logT{Seq.Base.length log'...

klinvill