FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Difference in case sensitive for modules and filenames

Open mtzguido opened this issue 1 year ago • 0 comments

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

mtzguido avatar Feb 06 '24 23:02 mtzguido