Beginner issue with executing fstar code.

[alex4482]

Hi. I wrote some code in Fstar, and i managed to make my local setup and to run one of the examples.

Now i tried to copy the Makefile from the examples/hello folder to change that one to match the files that i have.
But in that example there was only 1 .fst file and i have multiple .fst files.

Some of the modules use some of the other modules, and i have included them in the code, i seem to have created the .ml files for each module, but i dont know how to write in the makefile to get that 1 executable i need.
I tried random things as you can see in the photo and also tried looking at other examples but didnt find anything. Im just not familiar with this syntax or with what each command does.

Please help. I just want to get 1 executable from all of those .fst modules.

The main module is CDCL.fst, which uses all other 4, then ConflictFunctions.fst and DPLLPropagation.fst which include the remaining 2 modules, and then OtherFunctions which includes DataTypes.fst and then DataTypes.fst which includes nothing.

One more question.
To get a result from the executable, i need a 'main' function?

'let main = solveFormula [Disj (Lit (NotVar "a")) (Lit (Var "b")) ; Disj (Lit (NotVar "a")) (Lit (NotVar "c")) ]'

Like this?
'solveFormula' returns an array for me

[nikswamy]

Here's a sample multi-file project extracted and built in OCaml, with a main function

https://github.com/FStarLang/FStar/tree/nik_misc/examples/hello/multifile

[alex4482]

hi
thanks for the reply.
I tried using your makefile example
From what i unterstood, i only had to change the path to my fstar.exe and the name of my MAIN file.
then run
make -C .depend
make -C out/%.checked
make -C out/%.ml
make -C out/CDCL.exe (CDCL.fst is my MAIN file)

Not sure if i should write something at INCLUDE_PATHS.

this is the error i got when running make -C out/%.checked

Thanks for helping and reading!

[nikswamy]

you should just be able to run make. Can you first try to see if it works in the sample project that I provided. Once you are able to reproduce that, then you can try to adapt it to you project

[alex4482]

apparently i had to name my folders like you did ('output', also named my primary file 'Main') and it worked.

but i get and ocaml code error

in f* i dont get any errors, when the code is verified, but when i try to create the build i get this error.

maybe im not supposed to open certain FStar modules or maybe im supposed to exclude them somehow

[nikswamy]

Oh, that seems to be a bug in some handwritten code in FStar_List_Tot_Base.ml., which I'll fix now, but it will take some time for the fix to land in master and the next F* release.

Meanwhile, if you use FStar.List.Tot.mem lit literals instead of contains it should work.