FStar
FStar copied to clipboard
Difference in case sensitive for modules and filenames
$ cat AA.fst
module Aa
$ cat BB.fst
module BB
open AA
Trying to check BB gives:
$ ./bin/fstar.exe BB.fst
* Warning 241 at AA.fst(0,0-0,0):
- Unable to load AA.fst.checked since checked file AA.fst.checked does not
exist; will recheck AA.fst (suppressing this warning for further modules)
* Error 134 at BB.fst(3,5-3,7):
- Namespace AA cannot be found
1 error was reported (see above)
The first warning is expected. The second error does not mention a missing file, so it did find AA.fst and loaded it, but its name had a wrong case, so the AA namespace/module is not present, only Aa is.