2.3. Portable Executable Generation

The makePEfile function generates Windows EXEs and DLLs:

Definition bytes :=
  makePEfile EXE "winfact.exe" #x"00760000"
    [::Build_DLLImport "MSVCRT.DLL"
       [::ImportByName "printf"]]
    (dd #0)
    (fun _ imports => main (hd #0 (hd nil imports))).

This handles PE headers, import tables, relocations—everything needed for a working executable.