Help in compiling hello world.

[scyleaf]

Hey, I am a uni student and I've been really interested in learning FStar and LowStar.
However, I seem to be struggling a lot in understanding the compiling process. :(
I used project everest to obtain FStar and karamel, and I am on linux currently.

Namely, I've been trying to compile this example:

module Intro

module P = LowStar.Printf
module C = LowStar.Comment
module B = LowStar.Buffer

open FStar.HyperStack.ST
open LowStar.BufferOps

let main (): St Int32.t =
  push_frame ();
  let b: B.buffer UInt32.t = B.alloca 0ul 8ul in
  b.(0ul) <- 255ul;
  C.comment "Calls to printf are desugared via meta-programming";
  let s = "from Low*!" in
  P.(printf "Hello from %s\nbuffer contents: %xul\n"
    s 8ul b done);
  pop_frame ();
  0l

If I invoke karamel like so krml src/Intro.fst -tmpdir build/Debug
I get an undefined reference to main, and undefined references to `WasmSupport_trap'.
If I instead directly use fstar to get out.krml, and then use karamel on that, the WasmSupport_trap undefined references magically disappear. Why does this happen?

Still in both cases, I get an undefined reference to main.
The generated C file looks like so:

/* 
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
  KaRaMeL invocation: krml src/Intro.fst -tmpdir build/Debug
  F* version: b5839bfc
  KaRaMeL version: c73dd273
 */

#include "Intro.h"

#include "internal/LowStar.h"

int32_t Intro_main(void)
{
  uint32_t b[8U] = { 0U };
  b[0U] = (uint32_t)255U;
  /* Calls to printf are desugared via meta-programming */
  Prims_string s = "from Low*!";
  LowStar_Printf_print_string("Hello from ");
  LowStar_Printf_print_string(s);
  LowStar_Printf_print_string("\nbuffer contents: ");
  LowStar_Printf_print_lmbuffer_u32((uint32_t)8U, (uint32_t *)b);
  LowStar_Printf_print_string("\n");
  return (int32_t)0;
}

Why is main given this Intro_main name?
Is there a simple way I could compile this example?

I apologize to be asking this but I haven't been able to find how to do this in the documentation.
Thank you for your help in advance!

[msprotz]

Regarding WasmSupport: I pushed a fix so that the default behavior is to eliminate this file and not cause any issues about undefined references to WasmSupport_trap

Regarding Intro_main and not main: this is the default behavior of krml, you can use -no-prefix Intro to generate a main.

With the fix in #323, I can do krml -no-prefix Intro.fst and I get a successful compilation run.

Feel free to submit a PR to explain this behavior to the book/ subdirectory.

Generally, the mode where you invoke krml directly over the .fst files is super deprecated and I recommend looking at https://fstarlang.github.io/lowstar/html/Setup.html for a reference setup.

Hope this helps!