ulib doesn't make with F# build of F*

[catalin-hritcu]

[Update]: added progress tracking:

• UInt/Int/Normalization assertion failed - FStar.UInt discrepancy #872
• Not yet implemented - Removing format rm format #876
• Too many open files -- see below, maybe related to Too many open files? #1027
• The value could not be parsed -- see below
• F# build of F* rejects 0ul as out of range (F# build of F* rejects 0ul as out of range #1053)

We're making some progress towards being able to check our code even with the F# build of F*. Currently we're failing in ulib for two different reasons. First reason seems more about verification:

[hritcu@resurrected ulib]$ make                                                                                        (git)-[master] 
...
/home/hritcu/Projects/fstar/pub/bin/fstar.exe  --use_hints FStar.UInt.fst
./FStar.UInt.fst(22,0-33,13): (Error) assertion failed(Also see: ././prims.fst(193,30-193,42))
Verified module: FStar.UInt (41284 milliseconds)
1 error was reported (see above)
make: *** [Makefile:28: FStar.UInt.fst-ver] Error 1

While the second one seems more about printing and extraction:

[hritcu@resurrected ulib]$ make mgen                                                                                   (git)-[master] 
mkdir -p ml/extracted
/home/hritcu/Projects/fstar/pub/bin/fstar.exe  --use_hints --lax --codegen OCaml --odir ml/extracted --no_extract FStar.List.Tot --no_extract FStar.List.Tot.Base --no_extract FStar.Heap --no_extract FStar.List.Tot.Properties FStar.Set.fst FStar.TSet.fst FStar.Map.fst FStar.HyperHeap.fst FStar.HyperStack.fst
Extracted module Classical
Extracted module FunctionalExtensionality
Extracted module StrongExcludedMiddle
Extracted module PropositionalExtensionality
Extracted module PredicateExtensionality
Extracted module TSet
Extracted module Set
Extracted module Map
Extracted module HyperHeap
Extracted module HyperStack
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Not yet implemented
make: *** [Makefile:87: mgen] Error 1

[hritcu@resurrected ulib]$ /home/hritcu/Projects/fstar/pub/bin/fstar.exe  --use_hints --lax --codegen OCaml --odir ml/extracted --no_extract FStar.List.Tot --no_extract FStar.List.Tot.Base --no_extract FStar.Heap --no_extract FStar.List.Tot.Properties FStar.Set.fst FStar.TSet.fst FStar.Map.fst FStar.HyperHeap.fst FStar.HyperStack.fst --trace_error

Extracted module Classical
Extracted module FunctionalExtensionality
Extracted module StrongExcludedMiddle
Extracted module PropositionalExtensionality
Extracted module PredicateExtensionality
Extracted module TSet
Extracted module Set
Extracted module Map
Extracted module HyperHeap
Extracted module HyperStack
Unexpected error
Not yet implemented
  at FStar.Extraction.ML.PrintML+print@9.Invoke (System.Tuple`2[T1,T2] tupledArg) [0x00020] in <590c2b58cb5b3d61a7450383582b0c59>:0 
  at Microsoft.FSharp.Primitives.Basics.List.iter[T] (Microsoft.FSharp.Core.FSharpFunc`2[T,TResult] f, Microsoft.FSharp.Collections.FSharpList`1[T] x) [0x00019] in <589718b7dff9fae1a7450383b7189758>:0 
  at Microsoft.FSharp.Collections.ListModule.Iterate[T] (Microsoft.FSharp.Core.FSharpFunc`2[T,TResult] action, Microsoft.FSharp.Collections.FSharpList`1[T] list) [0x00001] in <589718b7dff9fae1a7450383b7189758>:0 
  at FStar.Extraction.ML.PrintML.print (Microsoft.FSharp.Core.FSharpOption`1[T] _arg1, System.String ext, FStar.Extraction.ML.Syntax+mllib l) [0x0000d] in <590c2b58cb5b3d61a7450383582b0c59>:0 
  at FStar.Main+codegen@79.Invoke (FStar.Extraction.ML.Syntax+mllib arg20@) [0x00001] in <590c2b65ce2aad61a7450383652b0c59>:0 
  at FStar.List.iter[a] (Microsoft.FSharp.Core.FSharpFunc`2[T,TResult] f, Microsoft.FSharp.Collections.FSharpList`1[T] x) [0x00019] in <590c2b34864a5396a7450383342b0c59>:0 
  at FStar.Main.codegen$cont@64 (Microsoft.FSharp.Collections.FSharpList`1[T] umods, FStar.TypeChecker.Env+env env, Microsoft.FSharp.Core.FSharpOption`1[T] opt, Microsoft.FSharp.Core.Unit unitVar) [0x000ac] in <590c2b65ce2aad61a7450383652b0c59>:0 
  at FStar.Main.codegen (Microsoft.FSharp.Collections.FSharpList`1[T] umods, FStar.TypeChecker.Env+env env) [0x00015] in <590c2b65ce2aad61a7450383652b0c59>:0 
  at FStar.Main.go$cont@120 (Microsoft.FSharp.Collections.FSharpList`1[T] filenames, Microsoft.FSharp.Core.Unit unitVar) [0x000de] in <590c2b65ce2aad61a7450383652b0c59>:0 
  at FStar.Main.go[a] (a _arg1) [0x00127] in <590c2b65ce2aad61a7450383652b0c59>:0 
  at FStar.Main.main[a] () [0x00002] in <590c2b65ce2aad61a7450383652b0c59>:0 

[kyoDralliam]

The second failure comes from src/format/format.fs ; It seems to be related to the new printer and PPrint but I don't understand why we still have both format and prettyprint.

[sishtiaq]

Removing format is a workitem already #876 .

[catalin-hritcu]

Just realized that the first issue has also already been filed (#872).

Here is the last error I get for ulib:

[hritcu@resurrected ulib]$ /home/hritcu/Projects/fstar/pub/bin/fstar.exe  --use_hints FStar.Map.fst FStar.HyperStack.fst hyperstack/FStar.ST.fst FStar.Buffer.fst FStar.Buffer.Quantifiers.fst --trace_error
Unexpected error
Too many open files
  at System.Diagnostics.Process.CreatePipe (System.IntPtr& read, System.IntPtr& write, System.Boolean writeDirection) [0x00014] in <f8255d9ef0594d18ae2c0d97286b9a80>:0 
  at System.Diagnostics.Process.StartWithCreateProcess (System.Diagnostics.ProcessStartInfo startInfo) [0x0012c] in <f8255d9ef0594d18ae2c0d97286b9a80>:0 

[catalin-hritcu]

Not sure why, but for the last problem it seems that mono runs out of file descriptors. Increasing the maximum number of file descriptors (from 1024 to 2048) makes this work:

[hritcu@resurrected ulib]$ ulimit -n 2048
[hritcu@resurrected ulib]$ /home/hritcu/Projects/fstar/pub/bin/fstar.exe  --use_hints FStar.Map.fst FStar.HyperStack.fst hyperstack/FStar.ST.fst FStar.Buffer.fst FStar.Buffer.Quantifiers.fst              
[1]  + done       emacs FStar.Int.fst
Verified module: FStar.Map (6845 milliseconds)
Verified module: FStar.HyperStack (24178 milliseconds)
Verified module: FStar.ST (18307 milliseconds)
Verified module: FStar.Buffer (159235 milliseconds)
Verified module: FStar.Buffer.Quantifiers (6678 milliseconds)
All verification conditions discharged successfully

[cpitclaudel]

That last error seems related to what I'm seeing in #1027

[catalin-hritcu]

@cpitclaudel Could well be. Please try to reproduce this by running

[ulib]$ fstar.exe  --use_hints FStar.Map.fst FStar.HyperStack.fst hyperstack/FStar.ST.fst FStar.Buffer.fst FStar.Buffer.Quantifiers.fst

[catalin-hritcu]

@cpitclaudel Any news on the repro above?

[cpitclaudel]

I see this:

$ ../bin/fstar.exe  --use_hints FStar.Map.fst FStar.HyperStack.fst hyperstack/FStar.ST.fst FStar.Buffer.fst FStar.Buffer.Quantifiers.fst
./FStar.Buffer.fst(745,31-745,34): (Error) 0 is not in the expected range for FStar.UInt32
1 error was reported (see above)

[catalin-hritcu]

@cpitclaudel Ouch, this is a new problem with the F# build I can also reproduce. The error seems bogus, does not appear with the OCaml build, and appears in code recently committed by @nikswamy
a8c1fbc#diff-0b9e97904ace9e5e55b6cdcd8e842211R642

[catalin-hritcu]

Will need to retry these things again, since I suspect that some of them are already fixed. Have been using the F# version successfully to bootstrap F* on the c_prop-dev branch, thus my optimism :)

[catalin-hritcu]

The first problems I got reproducing this were

1. Too many open files for FStar.Pointer.Base.fst

/home/hritcu/Projects/fstar/pub/bin/fstar.exe --use_two_phase_tc true --use_extracted_interfaces --use_hints --use_hint_hashes --cache_checked_modules --odir _output FStar.Pointer.Base.fst
FStar.Pointer.Base.fst(0,0-0,0): (Warning 241) Absent cache file FStar.Pointer.Base.fst.checked; will recheck FStar.Pointer.Base.fst and all subsequent files
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Too many open files

Doing ulimit -n unlimited does make this go away though.

2. A new The value could not be parsed error in FStar.UInt128.fst

[hritcu@resurrected ulib]$ /home/hritcu/Projects/fstar/pub/bin/fstar.exe --use_two_phase_tc true --use_extracted_interfaces --use_hints --use_hint_hashes --cache_checked_modules --odir _output FStar.UInt128.fst

FStar.UInt128.fst(0,0-0,0): (Warning 241) Absent cache file FStar.UInt128.fst.checked; will recheck FStar.UInt128.fst and all subsequent files
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
The value could not be parsed.

No clue what could be causing this.

Anyway, issue re-confirmed.

[valera-rozuvan]

I just ran into the same error message The value could not be parsed in UnifyRefs.uver. This happens when running the full suite of benchmarks:

$ make -C examples/micro-benchmarks
...
/home/user/dev/FStar/bin/fstar.exe  --use_hints --use_hint_hashes --use_extracted_interfaces true UnifyMatch.fst
Verified module: UnifyMatch (31910 milliseconds)
All verification conditions discharged successfully
/home/user/dev/FStar/bin/fstar.exe  --use_hints --use_hint_hashes --use_extracted_interfaces true UnifyRefs.fst
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
The value could not be parsed.
../Makefile.include:18: recipe for target 'UnifyRefs.uver' failed
make: *** [UnifyRefs.uver] Error 1
make: Leaving directory '/home/user/dev/FStar/examples/micro-benchmarks'

This is on a Debian machine:

Linux debian 4.9.0-8-amd64 #1 SMP Debian 4.9.110-3+deb9u5 (2018-09-30) x86_64 GNU/Linux
"Debian GNU/Linux 9 (stretch)"

How can I debug the source of the problem? Adding --debug_level Extreme does not produce any more information. @aseemr , @catalin-hritcu ?

[catalin-hritcu]

@valera-rozuvan If you have Visual Studio you can try running this in the F# debugger to get more details.

[valera-rozuvan]

long forgotten - should close issue
@catalin-hritcu ping

[mtzguido]

We do not have an F# build any more.