Brian Milnes

Multiple --cache_dir s for multi-directory compilations

3

Building a make system (before Fake) when I process a test subdirectory I get appropriate 241 and 247 errors due to having a single --cache_dir to work with. I checked...

FStar.IO could do with a flush

1

For testing, I write log files then read them and do a string compare to the expected. Useful for things like running external but small tests. It would be good...

* Error 118 at src/fstar/fst/FStar.Flog.fst(23,5-23,11): - Field 'startS' is redundant for type FStar.Flog.flog_config Should say something clearer, such as no such field startS in type.

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...

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...

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...

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,...

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

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...

I've run into multiple Sys_error no such file bugs. Ideally for a user, it would not ask for a bug report when a file is missing. And it print just...