search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

ulib fails to build (linux) #1653

Closed A-Manning closed 5 years ago

A-Manning commented 5 years ago 
$ make -C ulib
make: Entering directory 'FStar/ulib'
make FSTAR_HOME=.. -f Makefile.verify verify-core
make[1]: Entering directory 'FStar/ulib'
.depend:1: *** target pattern contains no '%'.  Stop.
make[1]: Leaving directory 'FStar/ulib'
Makefile:10: recipe for target 'all' failed
make: *** [all] Error 2
make: Leaving directory 'FStar/ulib'
aseemr commented 5 years ago

Our CI build happens on a Linux machine and it is working fine. Could someone with a Linux machine confirm please? @catalin-hritcu?

catalin-hritcu commented 5 years ago

I just tried ulib and it worked no problem. What version of make do you have? I'm on 4.2.1.

A-Manning commented 5 years ago

Make 4.1, on Ubuntu 18.04.2 LTS x86_64

catalin-hritcu commented 5 years ago

@A-Manning Can you try this again in a completely clean repo?

A-Manning commented 5 years ago

Can you try this again in a completely clean repo?

If I do make -C src first, then I get a very long output composed of errors like

Failed to load file because: System.IO.FileNotFoundException: Could not find file "FStar/ulib/FStar.Reflection.Data.fst.checked"
File name: 'FStar/ulib/FStar.Reflection.Data.fst.checked'
  at System.IO.FileStream..ctor (System.String path, System.IO.FileMode mode, System.IO.FileAccess access, System.IO.FileShare share, System.Int32 bufferSize, System.Boolean anonymous, System.IO.FileOptions options) <0x7fabe65fe740 + 0x003b8> in <61d5ec988156494684532710ebf1643d>:0 
  at System.IO.FileStream..ctor (System.String path, System.IO.FileMode mode, System.IO.FileAccess access, System.IO.FileShare share) <0x7fabe65fe590 + 0x0001d> in <61d5ec988156494684532710ebf1643d>:0 
  at (wrapper remoting-invoke-with-check) System.IO.FileStream..ctor(string,System.IO.FileMode,System.IO.FileAccess,System.IO.FileShare)
  at FStar.Util.load_value_from_file[a] (System.String fname) [0x00000] in <5c800082005fa6fda74503838200805c>:0

That seems ok though.

Closing the issue now. Not sure what happened here since my failing branch is even with master, but a fresh clone seems to work.