Can't get karamel nix flake to work

Question

Can't get karamel nix flake to work

ambiso opened this issue 2 years ago · 8 comments

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.

Answer 1 · 2023-03-21T17:15:33.000Z

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;
}

Answer 2 · 2023-03-21T19:03:03.000Z

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)

Answer 3 · 2023-03-22T10:20:40.000Z

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

Answer 4 · 2023-07-24T16:30:18.000Z

@pnmadelaine any thoughts?