project-everest / vale

Verified Assembly Language for Everest
Apache License 2.0
270 stars 20 forks source link

fstar.exe missing from Docker image #38

Closed thomasveje closed 5 years ago

thomasveje commented 5 years ago

Hi. As far as I can see, a change in the projecteverest/fstar-linux docker image has removed home/everest/FStar/bin/fstar.exe from the vale docker build as well.

msprotz commented 5 years ago

@gugavaro would know what happened with that image -- maybe it was renamed?

gugavaro commented 5 years ago

No changes were made. I will take a look

gugavaro commented 5 years ago

@protz @thomasveje what is the commit id you are seeing this issue? I just tried with projecteverest/fstar-linux:6743ab33adc1 this is the latest commit id and I cannot repro the issue.

everest@fc3e61349967:~$ ls /home/everest/FStar/bin -la total 86356 drwxr-xr-x 1 everest everest 4096 Mar 14 17:45 . drwxr-xr-x 1 everest everest 4096 Mar 14 17:54 .. -rw-r--r-- 1 everest everest 118 Jan 9 08:22 .gitignore -rw-r--r-- 1 everest everest 392192 Mar 14 17:43 FSharp.Compatibility.OCaml.dll -rw-r--r-- 1 everest everest 2611376 Mar 14 17:43 FSharp.Core.dll -rw-r--r-- 1 everest everest 53248 Mar 14 17:43 FSharp.PPrint.dll -rw-r--r-- 1 everest everest 71168 Mar 14 17:43 FsLexYacc.Runtime.dll -rw-r--r-- 1 everest everest 630784 Mar 14 17:44 basic.dll -rw-r--r-- 1 everest everest 527360 Mar 14 17:44 extraction.dll -rw-r--r-- 1 everest everest 414 Jan 9 08:22 extraction.dll.config -rw-r--r-- 1 everest everest 10240 Mar 14 17:44 format.dll -rw-r--r-- 1 everest everest 20992 Mar 14 17:44 fsdoc.dll -rw-r--r-- 1 everest everest 187 Sep 25 18:06 fsdoc.dll.config -rwxr-xr-x 1 everest everest 368 Sep 25 18:06 fstar-any.sh drwxr-xr-x 1 everest everest 12288 Mar 14 17:45 fstar-compiler-lib drwxr-xr-x 1 everest everest 16384 Mar 14 17:47 fstar-tactics-lib -rwxr-xr-x 1 everest everest 27294520 Mar 14 17:45 fstar.exe -rw-r--r-- 1 everest everest 190 Jan 9 08:22 fstar.exe.config -rwxr-xr-x 1 everest everest 306176 Mar 14 17:44 fstar.fsharp -rwxr-xr-x 1 everest everest 27294520 Mar 14 17:45 fstar.ocaml drwxr-xr-x 1 everest everest 12288 Mar 14 17:47 fstarlib -rw-r--r-- 1 everest everest 1080832 Mar 14 17:44 parser.dll -rw-r--r-- 1 everest everest 26112 Mar 14 17:44 prettyprint.dll -rw-r--r-- 1 everest everest 207360 Mar 14 17:44 reflection.dll -rw-r--r-- 1 everest everest 466432 Mar 14 17:44 smtencoding.dll -rw-r--r-- 1 everest everest 681984 Mar 14 17:44 syntax.dll -rw-r--r-- 1 everest everest 382976 Mar 14 17:44 tactics.dll -rwxr-xr-x 1 everest everest 78 Sep 25 18:06 tests-mono.sh -rwxr-xr-x 1 everest everest 24886208 Mar 14 17:45 tests.exe -rw-r--r-- 1 everest everest 187392 Mar 14 17:44 tosyntax.dll -rw-r--r-- 1 everest everest 1192448 Mar 14 17:44 typechecker.dll

thomasveje commented 5 years ago

Hmm. I get a different result for the newest image compared to an older one I had.

➜  ~ docker run projecteverest/fstar-linux:4e59328f4ad4 find . -name "fstar.exe"
./FStar/src/fstar/obj/Release/fstar.exe
./FStar/bin/fstar.exe
➜  ~ docker run projecteverest/fstar-linux:6743ab33adc1 find . -name "fstar.exe" 
➜  ~ docker run -it projecteverest/fstar-linux:6743ab33adc1 bash         
everest@f2ed22ebca19:~$ ls /home/everest/FStar/bin -la
total 32
drwxr-xr-x 5 everest everest 4096 Jan 22 05:18 .
drwxr-xr-x 1 everest everest 4096 Mar 14 06:00 ..
-rw-r--r-- 1 everest everest  118 Jan 22 05:18 .gitignore
-rwxr-xr-x 1 everest everest  368 Sep 24 23:17 fstar-any.sh
drwxr-xr-x 2 everest everest 4096 Sep 24 23:17 fstar-compiler-lib
drwxr-xr-x 2 everest everest 4096 Sep 24 23:17 fstar-tactics-lib
drwxr-xr-x 2 everest everest 4096 Sep 24 23:17 fstarlib
-rwxr-xr-x 1 everest everest   78 Sep 24 23:17 tests-mono.sh
gugavaro commented 5 years ago

it seems the issue is now resolved. let us know if you hit it again. thanks!