Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Can't get karamel nix flake to work #338

Open
ambiso opened this issue Mar 21, 2023 · 8 comments
Open

Can't get karamel nix flake to work #338

ambiso opened this issue Mar 21, 2023 · 8 comments

Comments

@ambiso
Copy link

ambiso commented Mar 21, 2023

I'm trying to get karamel to run with nix. Maybe I missed a guide somewhere, but here's my documented failures. I would be very grateful for any pointers what I can fix in my setup to get it to run.

I have the following example Test.fst:

module Test
    let square (x: UInt32.t): UInt32.t =
        let open FStar.UInt32 in
        x *%^ x

My ~/.config/nix/nix.conf contains

experimental-features = nix-command flakes

I then ran

$ nix shell github:FStarLang/karamel
error:
       … while updating the lock file of flake 'github:FStarLang/karamel/bd359d86d59401b001788468fa7366e741836c02'

       error: cannot write modified lock file of flake 'github:FStarLang/karamel' (use '--no-write-lock-file' to ignore)

$ # adding the flag...
$ nix shell github:FStarLang/karamel --no-write-lock-file
warning: not writing modified lock file of flake 'github:FStarLang/karamel':
• Added input 'flake-utils':
    follows 'fstar/flake-utils'
• Added input 'fstar':
    'github:fstarlang/fstar/71facac07710a40cfb2ad1bfe052d0c06d3d2e09' (2023-03-17)
• Added input 'fstar/flake-utils':
    'github:numtide/flake-utils/5aed5285a952e0b949eb3ba02c12fa4fcfef535f' (2022-11-02)
• Added input 'fstar/nixpkgs':
    'github:NixOS/nixpkgs/2788904d26dda6cfa1921c5abb7a2466ffe3cb8c' (2022-11-22)
• Added input 'nixpkgs':
    follows 'fstar/nixpkgs'
warning: not writing modified lock file of flake 'github:FStarLang/karamel':
• Added input 'flake-utils':
    follows 'fstar/flake-utils'
• Added input 'fstar':
    'github:fstarlang/fstar/71facac07710a40cfb2ad1bfe052d0c06d3d2e09' (2023-03-17)
• Added input 'fstar/flake-utils':
    'github:numtide/flake-utils/5aed5285a952e0b949eb3ba02c12fa4fcfef535f' (2022-11-02)
• Added input 'fstar/nixpkgs':
    'github:NixOS/nixpkgs/2788904d26dda6cfa1921c5abb7a2466ffe3cb8c' (2022-11-22)
• Added input 'nixpkgs':
    follows 'fstar/nixpkgs'

I then try:

$ krml -skip-linking -no-prefix Test Test.fst
⚙ KaRaMeL auto-detecting tools. Here's what we found:
readlink is: readlink
KaRaMeL called via: krml
the Karamel executable is: /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/bin/krml
KaRaMeL home is: /nix/store
⚙ KaRaMeL will drive F*. Here's what we found:
Did not find fstar.exe in PATH and FSTAR_HOME is not set
Fatal error: exception Warn.Fatal("Unrecoverable error")

$ which fstar.exe
fstar.exe not found

Since apparently it's insufficient to just add the karamel flake, I ^D out of the shell and run

$ nix shell github:FStarLang/karamel --no-write-lock-file github:FStarLang/fstar
$ which fstar.exe
/nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/bin/fstar.exe
$ krml -skip-linking -no-prefix Test Test.fst
⚙ KaRaMeL auto-detecting tools. Here's what we found:
readlink is: readlink
KaRaMeL called via: krml
the Karamel executable is: /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/bin/krml
KaRaMeL home is: /nix/store
⚙ KaRaMeL will drive F*. Here's what we found:
FSTAR_HOME is /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09 (via fstar.exe in PATH)
F* library not found in ulib; falling back to lib/fstar
fstar is: /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/bin/fstar.exe /nix/store/runtime/WasmSupport.fst /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/lib/fstar/FStar.UInt128.fst --trace_error --expose_interfaces --include /nix/store/krmllib --include /nix/store/include
⚡ Calling F* (use -verbose to see the output)
✘ [F*,extract] (use -verbose to see the output)
Unexpected error
FStar_Errors.Err(_)
Raised at FStar_Compiler_Effect.raise in file "fstar-lib/FStar_Compiler_Effect.ml" (inlined), line 10, characters 12-17
Called from FStar_Errors.raise_err in file "fstar-lib/generated/FStar_Errors.ml", line 718, characters 8-42
Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28
Called from FStar_Compiler_Effect.op_Bar_Greater in file "fstar-lib/FStar_Compiler_Effect.ml" (inlined), line 1, characters 52-55
Called from FStar_Parser_Dep.collect in file "fstar-lib/generated/FStar_Parser_Dep.ml", line 1979, characters 8-637
Called from FStar_Dependencies.find_deps_if_needed in file "fstar-lib/generated/FStar_Dependencies.ml", line 10, characters 18-76
Called from FStar_Main.go in file "fstar-lib/generated/FStar_Main.ml", line 226, characters 32-196
Called from FStar_Compiler_Util.record_time in file "fstar-lib/FStar_Compiler_Util.ml", line 24, characters 14-18
Called from FStar_Main.main.(fun) in file "fstar-lib/generated/FStar_Main.ml", line 328, characters 28-62

(Error 129) File /nix/store/runtime/WasmSupport.fst could not be found

1 error was reported (see above)

Warning 3: run_or_warn: the following command failed:
/nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/bin/fstar.exe --odir . --codegen krml --lax /nix/store/runtime/WasmSupport.fst /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/lib/fstar/FStar.UInt128.fst --trace_error --expose_interfaces --include /nix/store/krmllib --include /nix/store/include Test.fst
Warning 3 is fatal, exiting.

Since its assuming the karamel home is /nix/store I give it export KRML_HOME=/nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/. Unfortunately this still does not work:

$ which krml
/nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/bin/krml
$ export KRML_HOME=/nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/
$ krml -skip-linking -no-prefix Test Test.fst
⚙ KaRaMeL auto-detecting tools. Here's what we found:
readlink is: readlink
KaRaMeL called via: krml
KaRaMeL home is: /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/
⚙ KaRaMeL will drive F*. Here's what we found:
FSTAR_HOME is /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09 (via fstar.exe in PATH)
F* library not found in ulib; falling back to lib/fstar
fstar is: /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/bin/fstar.exe /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty//runtime/WasmSupport.fst /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/lib/fstar/FStar.UInt128.fst --trace_error --expose_interfaces --include /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty//krmllib --include /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty//include
⚡ Calling F* (use -verbose to see the output)
✘ [F*,extract] (use -verbose to see the output)
Unexpected error
FStar_Errors.Err(_)
Raised at FStar_Compiler_Effect.raise in file "fstar-lib/FStar_Compiler_Effect.ml" (inlined), line 10, characters 12-17
Called from FStar_Errors.raise_err in file "fstar-lib/generated/FStar_Errors.ml", line 718, characters 8-42
Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28
Called from FStar_Compiler_Effect.op_Bar_Greater in file "fstar-lib/FStar_Compiler_Effect.ml" (inlined), line 1, characters 52-55
Called from FStar_Parser_Dep.collect in file "fstar-lib/generated/FStar_Parser_Dep.ml", line 1979, characters 8-637
Called from FStar_Dependencies.find_deps_if_needed in file "fstar-lib/generated/FStar_Dependencies.ml", line 10, characters 18-76
Called from FStar_Main.go in file "fstar-lib/generated/FStar_Main.ml", line 226, characters 32-196
Called from FStar_Compiler_Util.record_time in file "fstar-lib/FStar_Compiler_Util.ml", line 24, characters 14-18
Called from FStar_Main.main.(fun) in file "fstar-lib/generated/FStar_Main.ml", line 328, characters 28-62

(Error 129) File /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty//runtime/WasmSupport.fst could not be found

1 error was reported (see above)

Warning 3: run_or_warn: the following command failed:
/nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/bin/fstar.exe --odir . --codegen krml --lax /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty//runtime/WasmSupport.fst /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/lib/fstar/FStar.UInt128.fst --trace_error --expose_interfaces --include /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty//krmllib --include /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty//include Test.fst
Warning 3 is fatal, exiting.

From here I'm not sure how to continue, I tried adding lib/krml to the KRML_HOME, but then I get a different error:

$ export KRML_HOME=/nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/lib/krml
$ krml -skip-linking -no-prefix Test Test.fst
⚙ KaRaMeL auto-detecting tools. Here's what we found:
readlink is: readlink
KaRaMeL called via: krml
KaRaMeL home is: /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/lib/krml
⚙ KaRaMeL will drive F*. Here's what we found:
FSTAR_HOME is /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09 (via fstar.exe in PATH)
F* library not found in ulib; falling back to lib/fstar
fstar is: /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/bin/fstar.exe /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/lib/krml/runtime/WasmSupport.fst /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/lib/fstar/FStar.UInt128.fst --trace_error --expose_interfaces --include /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/lib/krml/krmllib --include /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/lib/krml/include
⚡ Calling F* (use -verbose to see the output)
✘ [F*,extract] (use -verbose to see the output)
Unexpected error
FStar_Errors.Err(_)
Raised at FStar_Compiler_Effect.raise in file "fstar-lib/FStar_Compiler_Effect.ml" (inlined), line 10, characters 12-17
Called from FStar_Errors.raise_err in file "fstar-lib/generated/FStar_Errors.ml", line 718, characters 8-42
Called from BatList.map.loop in file "src/batList.mlv", line 237, characters 28-33
Called from BatList.map in file "src/batList.mlv", line 240, characters 4-12
Called from FStar_List_Tot_Base.concatMap in file "fstar-lib/FStar_List_Tot_Base.ml" (inlined), line 35, characters 28-37
Called from FStar_Parser_Dep.build_inclusion_candidates_list in file "fstar-lib/generated/FStar_Parser_Dep.ml", line 726, characters 4-1023
Called from FStar_Parser_Dep.build_map in file "fstar-lib/generated/FStar_Parser_Dep.ml", line 776, characters 18-52
Called from FStar_Parser_Dep.collect in file "fstar-lib/generated/FStar_Parser_Dep.ml", line 1993, characters 28-57
Called from FStar_Dependencies.find_deps_if_needed in file "fstar-lib/generated/FStar_Dependencies.ml", line 10, characters 18-76
Called from FStar_Main.go in file "fstar-lib/generated/FStar_Main.ml", line 226, characters 32-196
Called from FStar_Compiler_Util.record_time in file "fstar-lib/FStar_Compiler_Util.ml", line 24, characters 14-18
Called from FStar_Main.main.(fun) in file "fstar-lib/generated/FStar_Main.ml", line 328, characters 28-62

(Error 152) not a valid include directory: /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/lib/krml/krmllib

1 error was reported (see above)

Warning 3: run_or_warn: the following command failed:
/nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/bin/fstar.exe --odir . --codegen krml --lax /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/lib/krml/runtime/WasmSupport.fst /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/lib/fstar/FStar.UInt128.fst --trace_error --expose_interfaces --include /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/lib/krml/krmllib --include /nix/store/qwq5102fkdv934vv731f1chjn2fln3n7-karamel-dirty/lib/krml/include Test.fst
Warning 3 is fatal, exiting.
@pnmadelaine
Copy link
Contributor

Thanks for the report!
It seems to me like FStar expects KRML_HOME to point to the build directory of Karamel instead of the install directory.
I apologize that I did not document this properly, but the Karamel derivation exposes this directory as a second output.
Could you try using the following shell.nix to define KRML_HOME?

let
  system = "x86_64-linux";
  pkgs = import <nixpkgs> { inherit system; };
  karamel = builtins.getFlake "github:fstarlang/karamel";
in pkgs.mkShell {
  KRML_HOME = karamel.packages.${system}.karamel.home;
}

@ambiso
Copy link
Author

ambiso commented Mar 21, 2023 •
edited
Loading

With the above shell.nix

running nix-shell shell.nix I get a shell without krml or fstar.exe on PATH:

warning: not writing modified lock file of flake 'github:fstarlang/karamel':
• Added input 'flake-utils':
    follows 'fstar/flake-utils'
• Added input 'fstar':
    'github:fstarlang/fstar/c24591d8371304cc252a0ecbe55f8167c9bf440b' (2023-03-21)
• Added input 'fstar/flake-utils':
    'github:numtide/flake-utils/5aed5285a952e0b949eb3ba02c12fa4fcfef535f' (2022-11-02)
• Added input 'fstar/nixpkgs':
    'github:NixOS/nixpkgs/2788904d26dda6cfa1921c5abb7a2466ffe3cb8c' (2022-11-22)
• Added input 'nixpkgs':
    follows 'fstar/nixpkgs'

[nix-shell:~/krml-test]$ which krml
which: no krml in (/nix/store/mm2mnl0n16gi56dh85xsp2wfbzfkw88w-bash-interactive-5.2-p15/bin:/nix/store/zbr5i1jzfaj29v62g9r9xlibhv8295r6-patchelf-0.15.0/bin:/nix/store/rj91g41smpmp92xvhx6rjxz6878bn2b4-gcc-wrapper-12.2.0/bin:/nix/store/np14qqgvvnyna3vv640hmhi21flymiia-gcc-12.2.0/bin:/nix/store/qrzv77rkn5vf0fbbxl77rhhdd41xs8sk-glibc-2.35-224-bin/bin:/nix/store/z2k31yvarhcnlc98a76wm07q7a6ryla5-coreutils-9.1/bin:/nix/store/q5znq2mx417jj4mp3lmfqaql6k2jjnaz-binutils-wrapper-2.40/bin:/nix/store/nydwzhllkq0a21dny69zdjczh6v275lb-binutils-2.40/bin:/nix/store/z2k31yvarhcnlc98a76wm07q7a6ryla5-coreutils-9.1/bin:/nix/store/5pm0j70fz1b2jj6krvxbaamq3v0p5b69-findutils-4.9.0/bin:/nix/store/rmw415sc407q7wp1pp8qbqy6yg21rmif-diffutils-3.9/bin:/nix/store/sfiyijw1gp063ymv2m4zl58imkrfidsv-gnused-4.9/bin:/nix/store/a1s15jpz7fad571j2cyyczjpnxfnag0k-gnugrep-3.7/bin:/nix/store/45ncc133v5ncn8ivb1lkfv0wzfab9lx2-gawk-5.2.1/bin:/nix/store/6x4vhsssfhsirjxzim2j4c5qsqngd2gx-gnutar-1.34/bin:/nix/store/bm7gnjqqz2xp2gl82j0mvrrxmzgzdbv7-gzip-1.12/bin:/nix/store/plgdgfn64rz3x5ficwl0zp72sz17ycdq-bzip2-1.0.8-bin/bin:/nix/store/9qdfdlnzx4kgk5jqpim1xkrmp31bcraw-gnumake-4.4.1/bin:/nix/store/k32c6vzr9g1nln6v0gypz6ar6lqjb63l-bash-5.2-p15/bin:/nix/store/k1rd97yqvvaxch3nxli1gz7kbna8zxp1-patch-2.7.6/bin:/nix/store/y743qym3d429lkpp2j62jsrh90mziwk6-xz-5.4.1-bin/bin:/nix/store/s96idpb2aygp4jpj7zhnl6vvv9g6q83r-file-5.44/bin:/home/projects/.nix-profile/bin:/nix/var/nix/profiles/default/bin:/home/projects/.emacs.d/bin:/home/projects/.local/bin:/usr/local/bin:/usr/local/sbin:/usr/local/bin:/usr/bin: [... some more home-dir bin directories ...])

[nix-shell:~/krml-test]$ which fstar.exe
which: no fstar.exe in (/nix/store/mm2mnl0n16gi56dh85xsp2wfbzfkw88w-bash-interactive-5.2-p15/bin:/nix/store/zbr5i1jzfaj29v62g9r9xlibhv8295r6-patchelf-0.15.0/bin:/nix/store/rj91g41smpmp92xvhx6rjxz6878bn2b4-gcc-wrapper-12.2.0/bin:/nix/store/np14qqgvvnyna3vv640hmhi21flymiia-gcc-12.2.0/bin:/nix/store/qrzv77rkn5vf0fbbxl77rhhdd41xs8sk-glibc-2.35-224-bin/bin:/nix/store/z2k31yvarhcnlc98a76wm07q7a6ryla5-coreutils-9.1/bin:/nix/store/q5znq2mx417jj4mp3lmfqaql6k2jjnaz-binutils-wrapper-2.40/bin:/nix/store/nydwzhllkq0a21dny69zdjczh6v275lb-binutils-2.40/bin:/nix/store/z2k31yvarhcnlc98a76wm07q7a6ryla5-coreutils-9.1/bin:/nix/store/5pm0j70fz1b2jj6krvxbaamq3v0p5b69-findutils-4.9.0/bin:/nix/store/rmw415sc407q7wp1pp8qbqy6yg21rmif-diffutils-3.9/bin:/nix/store/sfiyijw1gp063ymv2m4zl58imkrfidsv-gnused-4.9/bin:/nix/store/a1s15jpz7fad571j2cyyczjpnxfnag0k-gnugrep-3.7/bin:/nix/store/45ncc133v5ncn8ivb1lkfv0wzfab9lx2-gawk-5.2.1/bin:/nix/store/6x4vhsssfhsirjxzim2j4c5qsqngd2gx-gnutar-1.34/bin:/nix/store/bm7gnjqqz2xp2gl82j0mvrrxmzgzdbv7-gzip-1.12/bin:/nix/store/plgdgfn64rz3x5ficwl0zp72sz17ycdq-bzip2-1.0.8-bin/bin:/nix/store/9qdfdlnzx4kgk5jqpim1xkrmp31bcraw-gnumake-4.4.1/bin:/nix/store/k32c6vzr9g1nln6v0gypz6ar6lqjb63l-bash-5.2-p15/bin:/nix/store/k1rd97yqvvaxch3nxli1gz7kbna8zxp1-patch-2.7.6/bin:/nix/store/y743qym3d429lkpp2j62jsrh90mziwk6-xz-5.4.1-bin/bin:/nix/store/s96idpb2aygp4jpj7zhnl6vvv9g6q83r-file-5.44/bin:/home/projects/.nix-profile/bin:/nix/var/nix/profiles/default/bin:/home/projects/.emacs.d/bin:/home/projects/.local/bin:/usr/local/bin:/usr/local/sbin:/usr/local/bin:/usr/bin: [... some more home-dir bin directories ...])

However, they both exist:

[nix-shell:~/krml-test]$ find /nix/store -name fstar.exe
/nix/store/3lc816q4fq0fr4164jlw6w462wpyqm6q-ocaml4.14.0-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/bin/fstar.exe
/nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/bin/fstar.exe
/nix/store/cspc4pvyqi7vzivdm1h232dx3zw8d4lc-ocaml4.14.0-fstar-c24591d8371304cc252a0ecbe55f8167c9bf440b/bin/fstar.exe
/nix/store/80fjw1wzkxzsqgkqn660zx3l90nyww6n-fstar-c24591d8371304cc252a0ecbe55f8167c9bf440b/bin/fstar.exe

Defining FSTAR_HOME and running krml directly, it works:

[nix-shell:~/krml-test]$ export FSTAR_HOME=/nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09

[nix-shell:~/krml-test]$ /nix/store/62v72mn6vr397j6pqf53naw4hqhd7dkv-karamel-dirty-home/krml -skip-linking -no-prefix Test Test.fst
⚙ KaRaMeL auto-detecting tools. Here's what we found:
readlink is: readlink
KaRaMeL called via: /nix/store/62v72mn6vr397j6pqf53naw4hqhd7dkv-karamel-dirty-home/krml
KaRaMeL home is: /nix/store/62v72mn6vr397j6pqf53naw4hqhd7dkv-karamel-dirty-home
⚙ KaRaMeL will drive F*. Here's what we found:
read FSTAR_HOME via the environment
F* library not found in ulib; falling back to lib/fstar
fstar is: /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/bin/fstar.exe /nix/store/62v72mn6vr397j6pqf53naw4hqhd7dkv-karamel-dirty-home/runtime/WasmS
upport.fst /nix/store/79r8qsdjv30ayqa5012mp56iayvx43xr-fstar-71facac07710a40cfb2ad1bfe052d0c06d3d2e09/lib/fstar/FStar.UInt128.fst --trace_error --expose_interfaces --include /nix/store/62v72m
n6vr397j6pqf53naw4hqhd7dkv-karamel-dirty-home/krmllib --include /nix/store/62v72mn6vr397j6pqf53naw4hqhd7dkv-karamel-dirty-home/include
⚡ Calling F* (use -verbose to see the output)
✔ [F*,extract] (use -verbose to see the output)
[...]
✔ [F*] ⏱️ 7s and 264ms
Warning 18: After bundling, two C files are named WasmSupport
✔ [Monomorphization] ⏱️ 36ms
✔ [Inlining] ⏱️ 2ms
✔ [Pattern matches compilation] ⏱️ 3ms
✔ [Structs + Simplify 2] ⏱️ 4ms
✔ [Drop] ⏱️ <1ms
✔ [AstToCStar] ⏱️ 2ms
✔ [CStarToC] ⏱️ <1ms
✔ [PrettyPrinting] ⏱️ <1ms
KaRaMeL: wrote out .c files for Test
KaRaMeL: wrote out .h files for Test
⚙ KaRaMeL will drive the C compiler. Here's what we found:
gcc is: x86_64-w64-mingw32-gcc
x86_64-w64-mingw32-gcc options are: -I /nix/store/62v72mn6vr397j6pqf53naw4hqhd7dkv-karamel-dirty-home/krmllib/dist/minimal -I /nix/store/62v72mn6vr397j6pqf53naw4hqhd7dkv-karamel-dirty-home/kr
mllib -I /nix/store/62v72mn6vr397j6pqf53naw4hqhd7dkv-karamel-dirty-home/include -I . -Wall -Werror -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-fu
nction -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -Wno-parentheses -std=c11
⚡ Generating object files
✔ [CC,./Test.c] (use -verbose to see the output)

@ambiso
Copy link
Author

ambiso commented Mar 22, 2023

If there's anything else I can do to help resolve this issue please let me know. Thanks for your help so far!

@msprotz
Copy link
Contributor

msprotz commented Jul 24, 2023

@pnmadelaine any thoughts?

@Parrot7483
Copy link
Contributor

I was trying to get the Tutorial from the book to compile.

After some tinkering I got the following working nix shell:

let
  system = "x86_64-linux";
  pkgs = import <nixpkgs> { inherit system; };
  karamel = builtins.getFlake "github:fstarlang/karamel";
  fstar = karamel.inputs.fstar.packages.${system}.fstar;
in pkgs.mkShell {
  buildInputs = [ fstar ];
  KRML_HOME = karamel.packages.${system}.karamel.home;
  FSTAR_HOME = fstar.out;
}

I then get

[nix-shell:~/Repositories/karamel]$ which fstar.exe
/nix/store/n3flnf5vl2iv63jrlw5nnxndbixwrh7g-fstar-51da68d61444ea33960617dccbb963fde73c3efb/bin/fstar.exe

[nix-shell:~/Repositories/karamel]$ echo $FSTAR_HOME
/nix/store/n3flnf5vl2iv63jrlw5nnxndbixwrh7g-fstar-51da68d61444ea33960617dccbb963fde73c3efb

[nix-shell:~/Repositories/karamel]$ which krml
/nix/store/b25azb9q0j9qzg7yfgsia4fllqjhrgw7-karamel-dirty/bin/krml

[nix-shell:~/Repositories/karamel]$ echo $KRML_HOME
/nix/store/s3s9alkdc4av75c5blvr2bhqiykwapj6-karamel-dirty-home

@Parrot7483
Copy link
Contributor

I had another look into the karamel and fstar flakes. fstar is an output of the karamel flake.

The buildInputs = [ fstar ]; should not be needed in the shell.nix.

@pnmadelaine Do have an idea of why this is?

@msprotz
Copy link
Contributor

msprotz commented Dec 3, 2024

Maybe @Nadrieril knows -- the karamel flake is being used regularly on CI so I'm not sure what the issue is here (I am not a nix expert)

@Nadrieril
Copy link

You may be interested in eurydice's flake.nix which has a dune package built with the karamel ocaml library. Is what you're trying to do different than what eurydice does (I know very little of karamel)?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
5 participants
@ambiso @Nadrieril @msprotz @pnmadelaine @Parrot7483