Package management

[nikswamy]

The topic of structuring the library into several packages, with the possibility of separate user-provided package repositories etc. comes up regularly.

@karthikbhargavan mentions it here: #2474 (comment)
@R1kM has brought it up at recent F* meetings
@W95Psp has also mentioned it

Let's discuss it here, please. Wishes, requirements, problems that we're hoping to solve, etc. most welcome.

[hacklex]

I think what I was doing was best placed in the core lib. It's the most basic stuff after all, the general algebraic structures and lemmas about them. If on the other hand we consider very special stuff like concrete applications (cryptography? number theory? graph theory?) then external packages sound reasonable.

But then again, for example .NET framework is way bigger and has even more stuff we would probably have considered good candidates for external modules.

So even though I like the idea of packages in F*, I also like the idea of a rich framework that is readily available to users out-of-the-box.

We will probably need a mechanism for verifying the package against the latest f* release.

Also we should carefully think about the versioning issues, i.e. when different packages A and B reference different versions of the same package X, and my project uses both A and B. This might turn out to be a really big problem.

[TheoWinterhalter]

Other projects like Coq, Haskell and Ocaml solve this by having a platform which includes a lot of regularly used packages that are tested to be compatible version-wise at each release.

[kant2002]

Also we should carefully think about the versioning issues, i.e. when different packages A and B reference different versions of the same package X, and my project uses both A and B. This might turn out to be a really big problem.

I think this is mostly of cultural problem where developers in "stable ecosystems" decide that supporting old code and not removing it worth it. Where "unstable platforms" decide that new features worth breaking changes.

I personally in the camp where you should have "stable platform" and try to move fast and innovate, but that's provably hard to do and a lot of work.

[kant2002]

F* seems to be not compiler, but rather pre-processor (or interpreter) for the OCaml and F# and other languages. That's raise the question about what kind of system can be done.

Let's pretend that we have packaging and versioning system which works.

Questions:

1. Let's say I create library in F* and package it as .NET DLL. How I can consume that library from F* ?
2. Let's say I create library in F* and package it as Ocaml package. How I can consume that library from F* ?
3. I create library in F*. If I use it, do I need to re-compile it again in the new project? Or cache should come with package
4. I have OCaml library, I would like to supply additional type annotations to the library to use it in F*, how?
5. I have F# library which I want to use in F*, with additional annotations probably, how?
6. I create library in F*, how can I create consumable package for Ocaml and .NET?

We have other backends, but F# and Ocaml has definitely opionated packaging frameworks and if you use that language. JavaScript + NPM is approximately the same.

Source code distribution for F* libraries with current compilation times I think is out of question now.

Let's say, I want to get rid of F# altogether, and create ulib which will target .NET runtime, but on much lower level. Is this in principle doable with current status? (that's probably separate question)

[andricicezar]

For me, even opening/including modules can be better. I am talking about opening/including modules from different folders, which is not possible to my knowledge without using a flag.

I would like to open/include modules like this:

• open "./../someFile.fst" as SomeFile
• open "./somePackage/someFile.fst" as SomeFile

My problem is that I have to edit emacs' init file everytime I add/change/remove a subfolder (to change the args of the --include flag). I don't find this intuitive either because in my use case I have different modules with the same name in different folders. It is not clear just from open SomeModule which module is opened from what folder.

Also, I am not sure what solutions do you use, but right now we don't have a way of sharing what config is needed for emacs. In theory, a config file should be in the base folder of the project/package and emacs should take the configs from there.

In my personal opinion, NodeJS has the best and simple to understand package management system, npm, compared to OCaml, Ruby, Python, PHP and TeX.

[nikswamy]

FYI, for the include path configuration, most F* developers customize their .emacs to pull the include path from a Makefile. See here

https://github.com/project-everest/mitls-fstar#configuring-emacs-mode

[W95Psp]

I think there are two topics here; as @kant2002 says, F* is not actually a compiler, more like a type-checker with multiple extraction facilities.
Thus, the package manager should be about:

• a package format, describing:
  • F* libraries (that are sets of (1) F* modules –possibly with native plugins, and (2) dependencies to other F* libraries), and
  • F* extractions (i.e. OCaml, C...), possibly describing as well further executable targets from such extractions.
• and about building those differents targets of F* packages, into:
  • pre-verified caches such as checked and hints files;
  • pre-compiled native plugins;
  • development environments (with precomputed include paths, plugin paths, caching paths, so that the user has nothing to worry about);
  • OCaml/C/WASM/JS/F#/… modules (or/and –resusable– OCaml/… libraries);
  • executables (i.e. binaries);
  • documentation, tag files…

Also, F* being about proof-oriented programming and thus about robust software, I really think reproducibility should be a goal.
If we want reproducibility, packages should specify which F* they use, and thus, the package manager should manage & build F* versions and binaries.
I'm personally quite a big fan of reproducibility: I implemented already a very drafty F* package manager that leverages Nix to get nice reproducibility guarantees. I really think Nix could help us get a nice package manager (or at least builder) without reinventing the wheel.

And as mentioned above, version resolution is hard and I think should be a non-goal; as @TheoWinterhalter suggests, stackage-like package snapshots seem to be a healthier approach.

Now that the F* compiler dropped F# support, the compiler could really just be a bunch of F* packages and be extracted without needing makefiles, just leveraging the package manager. That would be quite nice.

[R1kM]

We discussed this at yesterday's F* developers meeting, here is a summary of the discussion.

As the F* community grows, we want to make it easier to find contributions and libraries from different people and to use them in different projects. Currently, new contributions are mostly added to ulib/, which provides a centralized place to look for libraries. This has several advantages: all these libraries are ensured to be working
with the same version of F* (i.e., F* master), and to interoperate with each other. But this also comes with several problems, especially related to maintenance, to difficulties to specify different versions/releases of packages, and also to a high overhead when users update F*: there is currently no way for an F* user that, say, is not interested in stateful verification to omit Low* and Steel when building ulib/. The result is a quite time-consuming F* update process, where all changed files in ulib/ need to be reverified instead of the few that might be needed for a specific project.

The main goal for an F* package manager should thus be to provide a unified framework to provide different libraries as F* files, which can be usable directly in projects. The question of whether extracted files should also be included is left for later. The inspiration is from package managers like opam, or what Coq does with the coq-archive.
A library using this package manager should provide several features:

• It should come with checked files, that avoid reverifying it when "installing" it
• It should indicate which F* version it works with
• It should clearly state the libraries it depends on, and provide a convenient way to build against these libraries

There are several interesting technical challenges to solve here. The first one is related to packages requiring different F* versions, or changes upstream requiring to reverify the libraries. The current proposal is to let F*'s checked files system handle this issue. If a library X depends on a file A.fst that changed since checked files were created, F* already invalidates checked files from X, and will require a new verification of library X. In other cases, checked files will be usable as is, and the library can be directly imported in new projects.
Major changes to the F* compiler that might impact verification will be reflected as a bump to the internal "cache_version" of checked files; bumping this value will invalidate all existing checked files and also require reverification.

Several questions related to, for instance, tooling for this package manager, or how to keep track of all existing F* packages were left open and little discussed. Again, a design inspired from other similar ecosystems (i.e., Coq and/or OCaml) might be valuable here.

To start making progress in this direction, the current proposal is to start experimenting with splitting ulib/ into the current ulib/ and ulib/experimental. This choice is mostly based on different folders already existing, but will also separate F* ulib/ from Steel. Technical challenges here relate to the handling of fstarlib and fstartaclib: we want to make sure that, when only building ulib/, parts from ulib/experimental are not packaged into fstarlib and fstartaclib, but that they can be added a posteriori.

Please do not hesitate to provide feedback and to comment on this proposal.

[kant2002]

From what I understand plan is approximately like this

Package manager fstpack (fictional name)

Distribution unit is package.
Package is folder (probably compressed) with

• source files
• metadata file
• binary files (?)
• OCaml files (?)
• validated cache.

Metadata file describe following information about package

• name
• version
• license information
• authors
• description
• list of dependencies and their version requirements.
• some additional metadata which would be discussed in the details.

Packages would be stored in the repository.
Repository is either some folder structure, or some simple web app which respond to queries.

• Search for package names
• Get list of version for specific package
• Download specific version
• login as maintainer (?)
• upload package (?)
• downloading package from Github (?)

Package manager commands

• Restore packages from project metadata
• Restore packages from project lock file with tightly locked versions (?)
• Verify package
• Extract source code (?)
• Produce executable (??)

Questions

1. Why cached version should be stored on the server and not, for example in the global cache on the user PC? Shouln't this eliminate need to care about F* version in the package.
   What if fstpack compile package locally during package restore for now. Is validation time a concern here? Shoulld then each cache file to be digitally signed.
2. How Ocaml source can be used inside packages. Or it would be explicitly prohibited to have untrusted code in the package?
3. Does native Windows experience encouraged? Cygwin/MSYS and WSL is not native Windows experience. I willing to contribute, test, fix that area.
4. Do I correctly understand that Low* and Steel would come as separate packages?
5. Related to 1. Does format for F* cache files are stable enough to be distributed inside package?

Again, a design inspired from other similar ecosystems (i.e., Coq and/or OCaml) might be valuable here.

C++ has similar issues too. VCpkg seems to be solving this okayish. Maybe worth looking at.

[kant2002]

Based on the #2544 (comment) there should be at least one more thing to consider in package. Flags to FStar compiler, which may or may not be part of package. I think that affects outcome design of package management quite a lot.

[hacklex]

Not to mention there are flags that would force fstar to accept any statement.

Perhaps a system of "badges" would do good to most potential ponsuming endpoints. Examples of package badges:

• Honest. No axioms, no toggles that disable proof checking for any definitions, no anything that could potentially create a situation where a false statement is provable using this lib
• Up-to-date. This lib is successfully verified against the latest FStar release
• Valid thru (range of releases) -- lib is successfully verified against all releases from d1.m1.y1 to d2.m2.y2