search

project-everest / mitls-fstar

Verified implementation of TLS 1.3 in F*
https://www.mitls.org
Other
173 stars 16 forks source link

Test is not run in the MSVC configuration #212

Open msprotz opened 6 years ago

msprotz commented 6 years ago

https://github.com/project-everest/mitls-fstar/blob/master/src/windows/quiccrypto/makefile.vs#L22

this line doesn't work; I don't know how to do this in a visual studio makefile, short of calling into a .bat script; would anyone know how to make this work? @wintersteiger perhaps?

wintersteiger commented 6 years ago

Use & instead of ;?

E.g. compare set PATH=..\kremlib;%PATH% ; echo %PATH% with set PATH=..\kremlib;%PATH% & echo %PATH%

msprotz commented 6 years ago 
D:\cygwin\home\protz\Code\mitls-fstar\src\windows\quiccrypto>nmake -f makefile.vs

Microsoft (R) Program Maintenance Utility Version 14.10.25017.0
Copyright (C) Microsoft Corporation.  All rights reserved.

        set PATH=..\kremlib;..\evercrypt;%PATH% & .\test.exe

D:\cygwin\home\protz\Code\mitls-fstar\src\windows\quiccrypto>

nothing seems to run... any clue how to diagnose this?

wintersteiger commented 6 years ago

Does it pop up any dialogs in the background saying that it didn't find DLL so and so?

msprotz commented 6 years ago

On my machine, when I copy/paste that line, it displays some output then fails with an illegal instruction error. Nothing shows up when this is executed via the Makefile...

wintersteiger commented 6 years ago

Right, it probably suppresses that for some reason. Maybe wrap it in cmd /c "..."?

wintersteiger commented 6 years ago

I can't run that makefile, it complains that it doesn't know how to produce .obj files... I assume that's expected?

wintersteiger commented 6 years ago

Aha! Yes, the set doesn't work properly when used like that, the call to test.exe will see the old path.

wintersteiger commented 6 years ago

Try this:

test: test.exe libquiccrypto.dll
    set PATH=..\kremlib;%PATH%
    echo PATH=%%PATH%%
    .\test.exe