Lower case filenames cause everparse.cmd to fail with "(Error 168) Syntax error: expected a module name"

[Alan-Jowett]

Working:

type Test.3d
entrypoint typedef struct _point {
  UINT16 x;
  UINT16 y;
} point;
everparse.cmd Test.3d

Broken:

type test1.3d
entrypoint typedef struct _point {
  UINT16 x;
  UINT16 y;
} point;
everparse.cmd test1.3d
Processing files:  .\test1.3d
Writing file ./test1.Types.fst
Writing file ./test1.fst
Writing file ./test1.fsti
Writing file ./test1Wrapper.c
Writing file ./test1Wrapper.h
Running: c:\tools\everparse\bin\fstar.exe --print_in_place --odir . --cache_dir . --include . --load_cmxs WeakenTac --already_cached Prims,LowStar,FStar,LowParse,C,Prelude,Actions,ResultOps,Spec --include c:\tools\everparse\src\lowparse --include c:\tools\everparse\kremlib --include c:\tools\everparse\kremlib\obj --include c:\tools\everparse\src\3d\prelude --cmi --warn_error +241 .\test1.Types.fst
.\test1.Types.fst(1,7-1,12): (Error 168) Syntax error: expected a module name
1 error was reported (see above)

exit 1

[tahina-pro]

Thank you Alan for submitting this issue. Right now EverParse uses the .3d filename as is to generate the corresponding F* module name. Thus, as of now .3d filenames must start with a capital letter. I agree this is currently not documented anywhere. We could just do that.

If we were to introduce more flexibility and make your example work, then we would need to generate a F* module name with a case differing from that of the filename without user advice. There might be some consequences on 3d module names also (if data types from test1.3d are used in another .3d file), but I'm not sure. @nikswamy @aseemr What do you think?

[nikswamy]

How about we just detect the lower-case filename in 3d and immediately print an error requesting an upper-case filename?

Part of the annoyance with this issue is that the failure comes from the F* in the middle of the pipeline, which makes the error look obscure.