Can't get karamel nix flake to work

[ambiso]

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.

[tahina-pro]

Thank you for your question. Karamel has its separate repository, https://github.com/FStarLang/karamel . Could you please post an issue there? Thanks again!

[ambiso]

Sure: FStarLang/karamel#338