FStar

FStar copied to clipboard

Invalid --warn_error setting: cannot change the error level of fatal error 152 In order to support compilation in a directory hierarchy and particularly in emacs, one wants to put in...

briangmilnes

F* can't find one enum constructor after it found an isomorphic one

4

/// BUG F* can't find Three either as WrapOCaml.Three or Three !! /// This works above for enum One which is only trivially different. /// It works in language server...

briangmilnes

Warning for shadowing format needs to be more like warning for emacs

1

* Warning 274: - Implicitly opening namespace 'test.fstar.final.' shadows module 'testmain' in file "/home/milnes/Tuff/FinalFlog/test/src/fstar/fst/TestMain.fst". - Rename "/home/milnes/Tuff/FinalFlog/test/src/fstar/fst/TestMain.fst" to avoid conflicts. is not like Warning N: at and the emacs regexps...

briangmilnes

Sealed: mark seal/unseal as coercions

3

Draft, should test across projects.

mtzguido

Unexpected error when missing all files

3

F* 2024.08.14~dev platform=Linux_x86_64 compiler=OCaml 4.14.2 date=2024-09-02 15:23:16 -0700 commit=445f713ad8b276864ba7e205e028813e19324b66 I was goofing around with fstar arguments (in Forge makefiles) and darn Make did not evaluate things at the expected time,...

briangmilnes

OCaml comments on function applications with too many arguments "Did you miss a ;?" we should too to ease new users experience.

briangmilnes

While Z3 4.8.5 builds on aarch64 linux, it segfaults already on the VCs from prims.fst: ``` CHECK prims.fst Unexpected error; please file a bug report, ideally with a minimized version...

gebner

master, last three releases all build but can't compile FStar.Common.fst* from emacs or command line

3

/home/milnes/contrib/multicache/FStar/src/basic/FStar.Common.fst(54,27-57,27): - Computed type [Prims.int](http://prims.int/) & 'b and effect FStar.Compiler.Effect.ALL is not compatible with the annotated type [Prims.int](http://prims.int/) & 'b and effect Tot So we have the issue that this...

briangmilnes

Refinement subtypes being discarded

6

Hi, I came across a bug which allowed me to use integer division in a context that required a function of type `int -> int -> int`. This should be...

amosr

This should *not* work. It finishes correctly in either Dv or Tot. ```fstar assume val loop () : Dv unit let _ = assert True by begin loop (); ()...

mtzguido