nix: init #264
nix: init #264
Conversation
|
Thanks! Much appreciated. Just a heads up that most of us maintainers are on holiday until Monday. So, please expect that it'll take us until then to give you some proper feedback. |
|
So, I got pulse to compile using the Makefile in 381c5e6. Luckily, no ugly hacks were involved! While doing this, I also created the dune package, which I am not sure is redundant or not. Then, I created the wrapper script in 8a590d9 which uses the paths in the Nix store to run fstar with the pulse libraries loaded. Extra arguments can be passed as normal to fstar. To continue with packaging |
| --include ${config.packages.pulse}/lib/pulse/lib/pledge \ | ||
| --load_cmxs pulse \ | ||
| "$@" | ||
| ''; |
There was a problem hiding this comment.
A nit here, given that lib/fstar.include exists, the only thing needed is --include ${config.packages.pulse}/lib.
(Also F* will try to automatically load plugins when there's is a #lang-X directive, so the --load_cmxs is mostly redundant, but still required for some files currently, so best to keep it.)
There was a problem hiding this comment.
OK, I have to figure out how to get the lib/fstar.include to be found. For some reason I could not get the command to work unless the paths are exhaustively and explicitly included.
There was a problem hiding this comment.
Ah.. interesting. Then this is fine and we can later try to reduce it, fstar.include is rather new so no worries.
flake.nix
Outdated
| stdint | ||
| yojson | ||
| zarith | ||
| ]); |
There was a problem hiding this comment.
This list is here to specify only a subset of the F* ocaml packages, right? Would this break if F* took more dependencies?
|
Hi Juuso, thanks for this! I left a question (total non-Nix-expert here). Could we add a Nix CI job too? I think this workflow https://github.com/FStarLang/FStar/blob/master/.github/workflows/nix.yaml should just work. |
Changes done in a9b8313 should enable all to work ( |
Hi there,
I have packaged the pulse project with Nix while targeting the earlier release branch made earlier the year. I'm opening this PR to gauge interest in upstreaming these configurations -- I noticed that FStar and Karamel had these already, but pulse did not.
Are you interested in accepting Nix packaging for pulse?
To elaborate on this, this adds a flake.nix with
devenvintegration that uses the upstream FStar Nix flake to build a pulse artifact that compiles. Currently, you still need to runmakeandmake installmanually, but I plan to properly package pulse later on.I think it makes sense to make a bash wrapper for pulse that automatically populates the basic library files, and then allow additional arguments to be passed as
$2bash argument, where$1is the filename.Some things that are still missing:
I plan to have at least the pulse2rust be built as well, since that is what I want to target.
Before that, I am marking this as draft.
Let me know if there is something else to consider!