Extraction examples eg. examples/hello failing with F# · Issue #1087 · FStarLang/FStar (original) (raw)

building examples/hello with make -C examples/hello fs is failing to build with F#, with the error

Cannot open assembly './out/hello.exe': No such file or directory.
Makefile:47: recipe for target 'fs' failed
make: *** [fs] Error 2

This is due to compilation being commented out in the makefile:

#$(FSC) --nowarn:0086 -o out/hello.exe <span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mo stretchy="false">(</mo><mi>L</mi><mi>I</mi><mi>B</mi><mo stretchy="false">)</mo><mi mathvariant="normal">/</mi><mi>f</mi><mi>s</mi><mi mathvariant="normal">/</mi><mi>p</mi><mi>r</mi><mi>i</mi><mi>m</mi><mi>s</mi><mi mathvariant="normal">.</mi><mi>f</mi><mi>s</mi></mrow><annotation encoding="application/x-tex">(LIB)/fs/prims.fs </annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mopen">(</span><span class="mord mathnormal">L</span><span class="mord mathnormal" style="margin-right:0.07847em;">I</span><span class="mord mathnormal" style="margin-right:0.05017em;">B</span><span class="mclose">)</span><span class="mord">/</span><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="mord mathnormal">s</span><span class="mord">/</span><span class="mord mathnormal">p</span><span class="mord mathnormal" style="margin-right:0.02778em;">r</span><span class="mord mathnormal">im</span><span class="mord mathnormal">s</span><span class="mord">.</span><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="mord mathnormal">s</span></span></span></span>(LIB)/fs/io.fs out/Hello.fs

uncommenting gives another error - seemingly related to the removal of Powerpack

error FS0078: Unable to find the file '../../bin/FSharp.PowerPack.dll' in any of
 /usr/lib/mono/4.5
 /FStar/examples/hello
 /usr/lib/cli/fsharp

Placing FSharp.PowerPack.dll in /bin/ then gives a different error:

/FStar/examples/hello/out/Hello.fs(4,12): error FS0039: The namespace 'Pervasives' is not defined

/FStar/examples/hello/out/Hello.fs(9,51): error FS0039: The type 'Pervasives' is not defined

/FStar/examples/hello/out/Hello.fs(9,140): error FS0039: The type 'Pervasives' is not defined

/FStar/examples/hello/out/Hello.fs(10,9): error FS0039: The constructor, module or namespace 'Pervasives' is not defined