Moving F* .{fst,fsti} into a dune library

Ecosystem
1

I am creating a new set of makefiles for F* which translates to OCaml and compiles using dune. The ml
builds and opam installs nicely but I can’t find a simple recipe to copy src/.{fst,fsti} F files into the package.

Whats a way to get dune to build a package that it, and OPam, will install in my Opam package’s lib directory?
The F* compiler needs the sources to compile, the binaries are just fine.

1 Like
2

If you just need the files when building, shouldn’t dune’s copy_files work?
https://dune.readthedocs.io/en/stable/reference/dune/copy_files.html

If you need the files themselves to be installed, you can use the install stanza, something like:

(install
  (section lib)
  (files <whatever>.fst <whatever>.fsti))

I’m pretty new to dune myself so apologies if I got anything wrong.

3

(files …) wants a rule I can’t get right and copy_files only really allows renames, it complains about moving directories.

4

Could you paste the dune file you’re trying to use?

5

If you don’t mind adding a dependency, you can use https://github.com/diskuv/diskuvbox?tab=readme-ov-file#using-in-dune-rules and choose the copy-dir command.

(Are you trying to copy one of the fstar directories like ulib/ that contains a zillion files?)

6

I am trying to copy out just .fst and .fsti (F* files) but not Main.fst. Does that still work?

7

Not today. I never put in exclude flags. If time-sensitive you can just do a (deps (subtree .../ulib)) (progn (run (diskuvbox copy-dir .../ulib %{whatever})) (system (rm %{whatever}/Main.fst))) … please edit and use correct syntax. If you can wait until midweek I can add exclude flags.

8

J,
I think I could start with some more basic help.
/home/milnes/.opam/default/lib/fstar/
has all of the F* sources (*{.fst,.fsti})
and under it lib has all of the compiled ML files.

I’m not even getting that with a basic dune setup.
Is the compiled ML really supposed to be in a lib/lib?
How do I move my sources (including Main to start) into the /lib (not the double?)

9

Okay. Let’s clear up the ambiguity first.

  1. When you say “compiled ML” you are talking about the output of fstar --extract, right? (Which are.ml files)
  2. You (I think) also want a pure OCaml library that can be linked into an OCaml executable, right? (Which means .cma and related files)

If yes there are two compilers you are trying to coordinate.

Can you confirm / clarify the above?