Errors when running test files on Linux

[mohitWrangler]

I tested Vale with F* in Linux with the following command:

mono $HOME/vale-release-0.3.19/bin/vale.exe -fstarText -in common.vaf -out common.fst -outi common.fsti
fstar.exe --query_stats common.fst

I'm able to run it for common.vaf and forall.vaf but most of the instruction-specific files which include files like

include "../../../fstar/code/arch/x64/X64.Vale.InsBasic.vaf"
include{:fstar}{:open} "TestFStar"
include{:fstar}{:open} "FStar.Seq.Base"

are giving the following errors:

error at line 21 column 9 of file $HOME/hacl-star/vale/code/test/Vale.Test.X64.Memcpy.vaf:
cannot find id 'locs_disjoint'

error at line 18 column 14 of file $HOME/vale-0.3.19/tools/Vale/test/test.vaf:
cannot find type 'nat64'

error at line 41 column 5 of file $HOME/vale/tools/Vale/test/FTypeVale.vaf:
cannot find type 'byte'

I'm assuming these types have been defined in F* and somehow the compilation is not able to fetch these into the code.

Any help would be helpful.

[Chris-Hawblitzel]

Vale cannot read F* files directly, so the types have to be declared as Vale types in a Vale file. To help with this, we use the tool bin/importFStarTypes.exe to read in F* "dump" files and extract the F* types into Vale .vaf files. The SConstruct file contains examples of how to use this. It runs importFStarTypes.exe as follows: Command(types_vaf, dumps, f'{mono} {import_fstar_types_exe} {dumps_string} -out {types_vaf}'), where types_vaf is defined as types_vaf = f'{source_base}.types.vaf'. This puts the types into a new .vaf file with the suffix .types.vaf. Later, the SConstruct file adds these as extra include files using the -include {target}.types.vaf option to Vale.

[mohitWrangler]

After a long effort, I was able to run the SConstruct using scons. However, I had to copy the Fstar-master repo into the Vale/tools folder. Then running scons --FSTAR --FSTAR-MY-VERSION helped me see what you meant by import FStar types. Thank you for help.