FStar

FStar copied to clipboard

cc @nikswamy , this may be related to the weirdness you noticed with context pruning? This file is in bug-reports as a negative test, we should fail to prove this...

mtzguido

docker dev container: explicit platform, install pkg-config

2

Hi, The docker dev container wasn't working for me on an M1 Mac. I fixed it by specifying AMD64 emulation. I believe this change should not affect other x86 users....

amosr

Errors: Introducing '--message_format github', for github actions

2

Inspired by @W95Psp 's PR #3491, I thought this could be a nice addition. By setting this flag the warnings and errors look like this: ``` ::warning file=/home/guido/r/fstar/github/ulib/FStar.UInt.fsti,line=435,endLine=435::(271) Pattern uses...

mtzguido

``` $ git describe schoolNancy17-26894-g64e5bc6b00 ``` This should be based on the latest release instead. Using `--tags` forces that, but many tools don't look at non-annotated tags.

mtzguido

Extraction: reduce krml output unless -d/--debug

3

Hi @msprotz , wondering if you think this makes sense. I usually see a lot of output from extraction runs that are all benign. This would prevent them unless you...

mtzguido

module ParseBug open FStar.String let aneq s1 s2 (pos: nat{pos

briangmilnes

Proving `int =!= (int -> Dv int)`

2

```fstar let _ = assert (int =!= (int -> int)) let _ = assert (int =!= (int -> Dv int)) ``` The second assertion here fails, probably due to SMT...

mtzguido

```fstar module Bug open FStar.Tactics.Typeclasses [@@fundeps [1]] class pts_to (a b : Type) = { foo : a -> b -> bool; } type box a = | B of...

mtzguido

Cannot match implicit arg using constructor

1

The second match fails with 'syntax error', but the fact that the argument is implicit should not make a difference. ```fstar noeq type t2 = | Mk2 : _:int ->...

mtzguido

Take following list of bytes ```fstar module Qalqan open Prims type byte = UInt8.t //[@@extract_as (`(fun (x: nat) -> "not a number"))] let sb : list byte = [ //UInt8.uint_to_t...

kant2002