vale icon indicating copy to clipboard operation
vale copied to clipboard

Errors when running test files on Linux

Open mohitWrangler opened this issue 1 year ago • 2 comments

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.

mohitWrangler avatar Apr 08 '23 16:04 mohitWrangler