Are the build instructions using docker out of date?

[dreemkiller]

I'm attempting to build mitls-fstar using the docker approach, but I've run into a lot of problems:

1. The "git submodile init", "git submodule update" don't do anything, the .fstar directory is not created. This can be worked around by calling "git submodule add" with the information from the .gitmodules file.
2. src/parsers/Makefile seems to be slightly off. It appears that the addsuffix in the gen dependencies is creating a $basename.rfc.gen string, which the recipe for %.gen farther down does not match. I think it should be changed to $(addsuffix .gen,$(basename $(wildcard *(.rfc)), which creates a $basename.gen string, which the recipe for %.gen does match.
3. There are a number of additional things that need to be included in the docker volumes, such as quackyducky (or everparse - they seem to be used interchangeably), kremlin, and hacl-star.

Are the instructions for building with docker out of date? Or am I missing something essential in the instructions?

[ad-l]

Good points, it seems they are indeed out of date. Can you try on the dev branch?

[dreemkiller]

Will attempt to do that today.

[ad-l]

Any update?

[dreemkiller]

Sorry, didn't get to it yesterday. Hopefully this afternoon. If not, then this weekend. Thanks for being responsive, and sorry for being lame.

[dreemkiller]

Just ran it on dev.

1. I'm not sure if it still has the git submodule problem because I didn't start fresh, but I don't see anything that changed that would make me think it didn't.
2. The src/parsers/Makefile problem seems to be fixed in dev.
3. The quackyducky/everparser problem is still there (I don't think it's omitted from the docker image - I think it's the same one from master, so that makes sense)

[ad-l]

Thanks, we are adding the missing repo in the docker image

[Varad0612]

Any update on the quackyducky parser problem? I am trying to build the miTLS-fstar dev branch but there doesn't seem to be a rule for '../../../quackyducky/qd', needed by 'parsers.gen' in the src/parsers MAKEFILE. This is what I get when I try to run "make -C src/tls all -k -j 2":

make: Entering directory '/home/mitls-fstar/src/tls'
rm -f cache/OCaml/.depend cache/Kremlin/.depend cache/Model/.depend
make -C ../parsers gen
make[1]: Entering directory '/home/mitls-fstar/src/parsers'
make[1]: *** No rule to make target '../../../quackyducky/qd', needed by 'parsers.gen'.
make[1]: Target 'gen' not remade because of errors.
make[1]: Leaving directory '/home/mitls-fstar/src/parsers'
Makefile:11: recipe for target 'refresh-depend' failed
make: *** [refresh-depend] Error 2
make: Target 'all' not remade because of errors.

Is there something that I am missing? Any help would be appreciated.