OPAM package for F* (package is there, but can't run the tests)

[catalin-hritcu]

On Wed, Aug 5, 2015 at 9:24 PM, Nikhil Swamy [email protected] wrote:

Hey guys,

Just re-thinking the timing of a fresh release via OPAM.

Catalin and I are doing tutorial at ICFP at the end of August. It would be
great to have a nicely packaged, stable release available in advance of
that. I don’t mind doing a dry run of the current bits almost immediately,
but I think a stable release, including the new extraction features, to
coincide with the end of Abhishek’s internship would be very nice.

-Nik

This was brought up before (#234 (comment)), and while this would of course be nice, it depends on having a working Z3 package for OPAM. I've just checked (ocaml/opam-repository#3298) and there seems to be no working Z3 package for OPAM at this point. Given the imminence of the F* release, I think this will have to wait until after.

[markulf]

See also #294.

[msprotz]

I've fixed a couple things in Makefiles / search directories, so now all that's needed is a new release of F* with my fixes in, and then I'll send a pull request to opam-repository and we'll be all good.

[markulf]

I gave it a try under windows, and it worked fine. I noticed however that the Makefile in ~/.opam/system/share/fstar/examples assumes that fstar is located at ../../bin/fstar.exe.

[catalin-hritcu]

F* doesn't really support the Unix layout the OPAM package uses. If I remember right, another problem is that the binary itself assumes that the standard library is in ../lib.

[msprotz]

I fixed the binary so that it also finds the library in a standard unix-like layout (i.e. in ../lib/fstar). This should make things easier if we decide, one day, to have a debian / redhat / whatever package.

For the makefiles in examples, I think they should use whatever fstar is in the path.

[catalin-hritcu]

Someone should indeed try to fix the Makefile to work with the opam package. Last time I tried it was a lot of pain and I eventually gave up.

[beurdouche]

@msprotz, @catalin-hritcu : Is it still the case ?

[msprotz]

yes

[mtzguido]

We now have a working OPAM package. @tahina-pro notes that it is not under daily CI, but that should be coming soon.