search

FStarLang / FStar

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

`Executing F* code` not up-to-date for fstar-0.9.5? #1367

Closed WolframKahl closed 5 years ago

WolframKahl commented 6 years ago

Where that wiki page talks about lib/ml, I guess that this now should be ulib/ml.

However, make -C ulib/ml fails because there is no Makefile there --- as unpacked from fstar_0.9.5.0_Linux_x86_64.tar.gz, I only have a Makefile.include there.

mtzguido commented 6 years ago

I just edited the wiki to say ulib instead of lib, thanks!

The Linux tarball already has the compiler library fstarlib.cmxa, so that Makefile is not actually needed. The include will be useful if you plan to compile some F* file from a Makefile of your own. You can copy the one in example/hello/ (the relevant rule is ocaml).

But I just tried it out and got an OCaml linking error

OCAMLPATH="../../bin" ocamlfind opt -package fstarlib -linkpkg -g  out/Hello.ml -o hello.exe
File "out/Hello.ml", line 1:
Error: The files /usr/lib/ocaml/pervasives.cmi
       and ../../bin/fstarlib/prims.cmi make inconsistent assumptions
       over interface Pervasives
Makefile:19: recipe for target 'ocaml' failed
make: *** [ocaml] Error 2

which is likely due to the fact I'm on a different OCaml version than the library was compiled with (which is 4.02.3, I believe). I wasn't aware this was so brittle.

WolframKahl commented 6 years ago

I have seen this inconsistent assumptions for batteries when I tried to compile a modified version of examples/hello/testseq.fst (with an also-modified Makefile), and that although I opam switched to the OCaml version (4.05.0) indicated by fstar.exe --version. That's why I started this issue.

(It would be nice if testseq could be officially resurrected...)

mtzguido commented 6 years ago

I'm not sure about those batteries errors. I imagine it could be due to slight variations in OCaml setups, but I'm not very familiar with OCaml.

What will certainly work, though, is cloning our source tree and building F and its library yourself with your compiler. Building F is as simple as running make, and the library should compile when you try to use it in examples/hello, or by doing make -C ulib/ml/.

I've just restored testseq as well, and wired it to CI so it shouldn't break silently :)

catalin-hritcu commented 5 years ago

This works if compiling the master branch: https://fstar.zulipchat.com/#narrow/stream/184683-questions-and.20help/topic/Compiling.20to.20OCaml and is reasonable documented at: https://github.com/FStarLang/FStar/wiki/Executing-F%2A-code