Brian Milnes

module ExceptionNamesBug /// It would be nice if it did not warn 331 here as names are documentation. exception One of (name: string) and turning it down may cause other...

generated Makefile.basic exe target needs .o's

4

%.exe: *.o $(CC) $(CFLAGS) -o $@ $^ $(KRML_HOME)/krmllib/dist/generic/libkrmllib.a

tests/c-tests.exe: tests/c-tests.o dist/libbignum.a $(CC) $^ -o $@ for line 273 in karamel/book/tutorial/Makefile

Had to do a curl, sh thing to install rust. karamel/test/README.md should probably just point up to karamel/README.md

CompileError: WebAssembly.instantiate(): return count of 2 exceeds internal limit of 1 @+53 when making the WASM tests on Ubuntu 21. So WASM which test/README.md says is super experimental is not...

__FL__ added and tested

2

Two changes: 1) __FL__ lexeme in FStarC_Parser_LexFStar.ml 2) tests/validation-time with a Test.LexemeFL.fst that checks __FL__

Milnes strings

1

I have 'thickened' strings quite a bit. There are additions to the end of FStar.String.fst that define a partial string equality and string equality and provide a string difference (for...

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

If you foolishly add a decreases to an interface you get a 337 but in the language server it does not give you a line number. Perhaps a sweep of...

I bumped into this validating Sheera's DFS, so I wrote some small test files. * Error 98 at src/LetLemmaInFSTI.fst(1,7-1,21): - Some interface elements were not implemented by module LetLemmaInFSTI: val...