Why do our binaries include ocamlopt and ocamlrun? Are they really needed? Are we legally allowed to redistribute them?

[catalin-hritcu]

The make package target from the Makefile in src/ocaml-output includes this:

    cp /usr/bin/ocamlopt fstar/bin/ocamlopt || true
    cp /usr/bin/ocamlrun fstar/bin/fsocamlrun || true

@ad-l Why are these OCaml binaries sometimes copied in (and sometimes not, since the hardcoded path seems very fragile)? Are they needed for anything?

If they are really needed we would need to think more seriously about licensing issues. OCaml is released under the rather non-standard Q Public License:
https://ocaml.org/docs/license.html
https://en.wikipedia.org/wiki/Q_Public_License

[avsm]

Note that it's possible to get OCaml under the BSD license by joining the Caml Consortium; http://caml.inria.fr/consortium/. (Microsoft is already a member)

[catalin-hritcu]

@avsm This is good to know, thanks a lot. My impression is that we don't need to bundle OCaml with our binaries anyway. In fact we just removed them from the latest release.

[avsm]

Nope, it shouldn't be necessary. I'm taking a look at adding an OPAM package for Fstar that'll make it even easier. Just needs Z3 first (ocaml/opam-repository#3298).

[catalin-hritcu]

Having an OPAM package for Fstar would be great, of course. Please let us know when there is something with which we can help.

[ad-l]

It is no longer necessary in the current setup.

[markulf]

OCaml on windows is still quite broken:
#294