get Parser from Lean

Stream: Is there code for X?

[Asei Inoue]

When I was writing a parser, I realized that since Lean comes equipped with powerful parser combinators, it would be great if I could leverage them to obtain a parser more easily.

With that in mind, I attempted to construct a parser based on Lean’s own parser. The attempt was somewhat successful, but I have the following concerns:

1. parseArith ended up being an unsafe function.

2. The return value of parseArith is wrapped in the TermElabM monad. Ideally, I would like to implement it as a function of type String → Arith.

Is there any way to address these issues?

import Lean
import Qq

/-- A set of binary operations -/
inductive Op where
  /-- Addition -/
  | add
  /-- Multiplication -/
  | mul
deriving DecidableEq, Repr

/-- Arithmetic expressions -/
inductive Arith where
  /-- Numeric literal -/
  | val : Nat → Arith
  /-- Application of a binary operator -/
  | app : Op → Arith → Arith → Arith
deriving DecidableEq, Repr

section Arith

  /-- Syntax category for `Arith` -/
  declare_syntax_cat arith

  /-- Custom syntax for easily writing `Arith` expressions -/
  syntax "[arith|" arith "]" : term

  -- A numeric literal is treated as an arithmetic expression
  syntax:max num : arith

  -- Arithmetic expressions connected with `+` or `*` are expressions
  -- The precedence of `+` and `*` is specified
  syntax:30 arith:30 " + " arith:31 : arith
  syntax:35 arith:35 " * " arith:36 : arith

  -- Expressions enclosed in parentheses are expressions
  syntax:max "(" arith ")" : arith

  macro_rules
    | `([arith| $n:num]) => `(Arith.val $n)
    | `([arith| $l:arith + $r:arith]) => `(Arith.app Op.add [arith| $l] [arith| $r])
    | `([arith| $l:arith * $r:arith]) => `(Arith.app Op.mul [arith| $l] [arith| $r])
    | `([arith| ($e:arith)]) => `([arith| $e])

end Arith

open Lean Elab Term Syntax Qq

/-- Parse a string using Lean's parser and return an `Arith` expression -/
unsafe def parseArith (input : String) : TermElabM Arith := do
  let env ← getEnv
  let stx ← Lean.ofExcept <| Parser.runParserCategory env `term s!"[arith| {input}]"
  let expr : Q(Arith) ← elabTerm stx q(Arith)
  let arith : Arith ← Meta.evalExpr Arith q(Arith) expr
  return arith

#eval show TermElabM Bool from do
  let expected := Arith.app Op.add (Arith.val 1) (Arith.val 2)
  let actual ← parseArith "1 + 2"
  return expected = actual

[Asei Inoue]

I would be happy if I could obtain a parsing function of type String → Arith, even if it has to be unsafe.

[Robin Arnez]

You can actually do it quite manually:

import Lean.Parser

/-- A set of binary operations -/
inductive Op where
  /-- Addition -/
  | add
  /-- Multiplication -/
  | mul
deriving DecidableEq, Repr, Inhabited

/-- Arithmetic expressions -/
inductive Arith where
  /-- Numeric literal -/
  | val : Nat → Arith
  /-- Application of a binary operator -/
  | app : Op → Arith → Arith → Arith
deriving DecidableEq, Repr, Inhabited

open Lean Parser in
unsafe def parseArith : Parser :=
  arithParser 0
where
  num : Parser := Term.num
  add : TrailingParser := trailing_parser:30:30 " + " >> arithParser 31
  mul : TrailingParser := trailing_parser:35:35 " * " >> arithParser 36
  paren : Parser := leading_parser:maxPrec "(" >> arithParser 0 >> ")"

  arithParserFnCore : ParserFn :=
    prattParser `arith parsingTables .default (mkAntiquot "arith" `arith (isPseudoKind := true)).fn
  arithParser (prec : Nat) : Parser :=
    { fn := adaptCacheableContextFn ({ · with prec }) (withCacheFn `arith arithParserFnCore) }
  parsingTables : PrattParsingTables := {
    trailingParsers := []
    trailingTable := [(`«+», add, 30), (`«*», mul, 30)].foldl (fun map (a, b) => map.insert a b) {}
    leadingParsers := []
    leadingTable := [(`«$», num, maxPrec), (`num, num, maxPrec), (`«(», paren, maxPrec)].foldl (fun map (a, b) => map.insert a b) {}
  }

open Lean in
partial def elabArith : TSyntax `arith → Except String Arith
  | `(parseArith| $a:arith + $b:arith) => return .app .add (← elabArith a) (← elabArith b)
  | `(parseArith| $a:arith * $b:arith) => return .app .mul (← elabArith a) (← elabArith b)
  | `(parseArith| $n:num) => return .val n.getNat
  | `(parseArith| ($a:arith)) => elabArith a
  | _ => throw s!"unexpected syntax"

open Lean Parser in
instance : Insert Token TokenTable := ⟨fun a b => b.insert a a⟩
open Lean Parser in
instance : Singleton Token TokenTable := ⟨fun a => insert a ∅⟩

open Lean Parser in
def arithFromString (input : String) : Except String Arith := unsafe
  let env : Environment := unsafeCast () -- we won't use it, right?
  let tokens : TokenTable := {"$", "(", ")", "+", "*"}
  let state := parseArith.fn.run (mkInputContext input "<input>") (ParserModuleContext.mk env {} .anonymous []) tokens (mkParserState input)
  if state.hasError then
    throw state.errorMsg.get!.toString
  else
    elabArith ⟨state.stxStack.back⟩

#eval arithFromString "(3 + 2) * 5"

That way you have a pure function. Also, the unsafe term prevents unsafe propagation, i.e. you can have unsafe code within safe code.

[Asei Inoue]

oh, nice… Are you a magician?

why you use Parser, instead of ParserDescr?

[Asei Inoue]

Is it impossible by using syntax command?

[Asei Inoue]

alternatively, is it impossible to get Parser from ParserDescr?

[Robin Arnez]

You can use docs#Lean.Parser.compileParserDescr but you need ImportM context for that (in particular an Environment).

[Robin Arnez]

So not really usable in pure code

[Robin Arnez]

The code above is roughly what Lean does internally.

[Paul Mure]

@Robin Arnez How would you run an ImportM action in impure code? So that you can use the syntax command.

[Paul Mure]

I tried to create an environment with

Lean.importModules #[{module := `MyModule}] {}

But it keeps saying unknown parser category when I tried to run a category parser.

[Adam Topaz]

Can you provide a #mwe ?

[Paul Mure]

@Adam Topaz Here's a MWE
Scratch/Basic.lean

import Lean

namespace Arith

open Lean Elab

declare_syntax_cat arith

inductive Arith
  | ident : String → Arith
  | plus : Arith → Arith → Arith

scoped syntax ident : arith
scoped syntax:50 arith:50 " + " arith:51 : arith
scoped syntax "(" arith ")" : arith

partial def expandArith : TSyntax `arith → CoreM (TSyntax `term)
  | `(arith| $i:ident) =>
    let s := Syntax.mkStrLit i.getId.toString
    `(Arith.ident $s)
  | `(arith| $e1:arith + $e2:arith) => do
    let e1 ← expandArith e1
    let e2 ← expandArith e2
    `(Arith.plus $e1 $e2)
  | `(arith| ($e:arith)) => expandArith e
  | _ => throwUnsupportedSyntax

def parseArithFromString (s : String) : CoreM (Except String String) := do
  let env ← getEnv
  let stx := Parser.runParserCategory env `arith s
  match stx with
  | .ok stx => do
    let stx ← expandArith ⟨stx⟩
    return .ok s!"{(Syntax.prettyPrint stx)}"
  | .error msg => return .error msg

elab "#parse_arith_local" s:str : command => do
  let e ← Command.liftCoreM <| parseArithFromString s.getString
  IO.println e

-- this works as expected
#parse_arith_local "a + (b + c)"

def parseArithFromStringIO (s : String) : IO (Except String String) := do
  let env ← importModules #[{module := `Scratch.Basic}] {}
  let parse := parseArithFromString s
  let ctx : Core.Context := {fileName := "<input>", fileMap := s.toFileMap}
  let (s, _) ← (parse.run ctx {env}).toIO (fun _ => .userError "unexpected error")
  return s

-- this does not work
#eval parseArithFromStringIO "a + (b + c)"

[Robin Arnez]

Well you can't import yourself :-) That'd be recursive

[Paul Mure]

I've tried doing this from a separate module as well. I can only get it to work if the syntax commands are not scoped. So something like this defined in Main.lean will work as expected:

def parseArithFromStringIO (s : String) : IO (Except String String) := do
  let env ← importModules #[{module := `Scratch.Basic}] {} (loadExts := true)
  let parse := Arith.parseArithFromString s
  let ctx := {fileName := "<input>", fileMap := s.toFileMap, currNamespace := `Scratch.Arith}
  let (s, _) ← (parse.run ctx {env}).toIO (fun _ => .userError "unexpected error")
  return s

But I have to remove the scoped keywords from the syntax declaration.

[Paul Mure]

I assume the issue is I'm not correctly opening the namespace in the meta functions?

[Paul Mure]

I expected this to solve the namespace issue but it doesn't work either:

  let ctx : Core.Context := {
    fileName := "<input>",
    fileMap := s.toFileMap,
    openDecls := [.simple `Arith []]
  }
  let (s, _) ← (parse.run ctx {env}).toIO (fun _ => .userError "unexpected error")

[Robin Arnez]

There seems to be something called docs#Lean.activateScoped

[Robin Arnez]

What about adding activateScoped `Arith at the top of parseArithFromString instead?

[Paul Mure]

That worked! Thank you so much :thank_you:

[Paul Mure]

I feel like just gained a whole new level of respect for Lean's meta-programming abilities. I thought this setup would need to be a lot more hacky. But this is actually quite nice!

[Paul Mure]

Robin Arnez said:

Well you can't import yourself :-) That'd be recursive

The self-import actually seems to work in some cases, which blows my mind.

[Robin Arnez]

Heh I guess if it has a compiled version already

[Robin Arnez]

But then anybody else building your project won't be able to

[Paul Mure]

Just check again after running lake clean. It seems like self-imports are fine if the function where this happens is called from a different file. Wild!

[Asei Inoue]

Does that mean it is also possible to implement parseArith as a function of type String → IO Arith?

import Lean
import Qq

/-- A set of binary operations -/
inductive Op where
  /-- Addition -/
  | add
  /-- Multiplication -/
  | mul
deriving DecidableEq, Repr

/-- Arithmetic expressions -/
inductive Arith where
  /-- Numeric literal -/
  | val : Nat → Arith
  /-- Application of a binary operator -/
  | app : Op → Arith → Arith → Arith
deriving DecidableEq, Repr

section Arith

  /-- Syntax category for `Arith` -/
  declare_syntax_cat arith

  /-- Custom syntax for easily writing `Arith` expressions -/
  syntax "[arith|" arith "]" : term

  -- A numeric literal is treated as an arithmetic expression
  syntax:max num : arith

  -- Arithmetic expressions connected with `+` or `*` are expressions
  -- The precedence of `+` and `*` is specified
  syntax:30 arith:30 " + " arith:31 : arith
  syntax:35 arith:35 " * " arith:36 : arith

  -- Expressions enclosed in parentheses are expressions
  syntax:max "(" arith ")" : arith

  macro_rules
    | `([arith| $n:num]) => `(Arith.val $n)
    | `([arith| $l:arith + $r:arith]) => `(Arith.app Op.add [arith| $l] [arith| $r])
    | `([arith| $l:arith * $r:arith]) => `(Arith.app Op.mul [arith| $l] [arith| $r])
    | `([arith| ($e:arith)]) => `([arith| $e])

end Arith

open Lean Elab Term Syntax Qq

/-- Parse a string using Lean's parser and return an `Arith` expression -/
unsafe def parseArith (input : String) : TermElabM Arith := do
  let env ← getEnv
  let stx ← Lean.ofExcept <| Parser.runParserCategory env `term s!"[arith| {input}]"
  let expr : Q(Arith) ← elabTerm stx q(Arith)
  let arith : Arith ← Meta.evalExpr Arith q(Arith) expr
  return arith

#eval show TermElabM Bool from do
  let expected := Arith.app Op.add (Arith.val 1) (Arith.val 2)
  let actual ← parseArith "1 + 2"
  return expected = actual

[Asei Inoue]

hmm... why "incomplete case" error occurs?

import Lean
import Qq

/-- A set of binary operations -/
inductive Op where
  /-- Addition -/
  | add
  /-- Multiplication -/
  | mul
deriving DecidableEq, Repr, Inhabited

/-- Arithmetic expressions -/
inductive Arith where
  /-- Numeric literal -/
  | val : Nat → Arith
  /-- Application of an operator -/
  | app : Op → Arith → Arith → Arith
deriving DecidableEq, Repr, Inhabited

section Arith

  /-- Syntax category for `Arith` -/
  declare_syntax_cat arith

  /-- Syntax to define `Arith` expressions more readably -/
  syntax "[arith|" arith "]" : term

  -- Numeric literals are expressions
  syntax:max num : arith

  -- Expressions joined with `+` or `*` are expressions
  -- Set parse precedence for `+` and `*`
  syntax:30 arith:30 " + " arith:31 : arith
  syntax:35 arith:35 " * " arith:36 : arith

  -- Expressions enclosed in parentheses are expressions
  syntax:max "(" arith ")" : arith

  macro_rules
    | `([arith| $n:num]) => `(Arith.val $n)
    | `([arith| $l:arith + $r:arith]) => `(Arith.app Op.add [arith| $l] [arith| $r])
    | `([arith| $l:arith * $r:arith]) => `(Arith.app Op.mul [arith| $l] [arith| $r])
    | `([arith| ($e:arith)]) => `([arith| $e])

end Arith

open Lean Elab Term Syntax Qq

/-- Use Lean's parser to parse a string into an `Arith` expression -/
def TermElabM.parseArith (input : String) : TermElabM Arith := unsafe do
  let env ← getEnv
  let stx ← Lean.ofExcept <| Parser.runParserCategory env `term s!"[arith| {input}]"
  let expr : Q(Arith) ← elabTerm stx q(Arith)
  let arith : Arith ← Meta.evalExpr Arith q(Arith) expr
  return arith

unsafe def TermElabM.unsafeRun {α : Type} (m : TermElabM α) : α := @unsafeCast (TermElabM α) α m

def parseArith (input : String) : Arith := unsafe
  TermElabM.unsafeRun <| TermElabM.parseArith input

/- Incomplete case error occurs -/
#eval parseArith "1 + 2 * 3"

[Asei Inoue]

Lean.Elab.Term.TermElabM.toIO is useful here ....?

[Robin Arnez]

TermElabM α and α are not compatible, TermElabM is

Lean.Elab.Term.Context →
    ST.Ref IO.RealWorld Lean.Elab.Term.State →
      Lean.Meta.Context →
        ST.Ref IO.RealWorld Lean.Meta.State →
          Lean.Core.Context → ST.Ref IO.RealWorld Lean.Core.State → IO.RealWorld → EStateM.Result Lean.Exception IO.RealWorld α

[Robin Arnez]

You can't really run a TermElabM in pure code

[Asei Inoue]

Thank you!

[Asei Inoue]

Then, would it be possible to define a parser function of type String → IO Arith?
If so, I think we could use an unsafe function of type IO α → α to create a function of type String → Arith.

[Robin Arnez]

You need an environment which is a bit difficult to get unless you have the necessary olean files somewhere. In other words, it's pretty difficult to make this into an standalone executable.

[Robin Arnez]

That being said; nobody prevents you from using Lean.mkEmptyEnvironment and adding everything necessary yourself.

[Asei Inoue]

I've resolved this problem!!! :tada:

Thank you for everyone

[Asei Inoue]

How to resolve this?

first, make a file named Project/Syntax.lean with following content:

import Lean

inductive Op where
  | add
  | mul
deriving DecidableEq, Repr

inductive Arith where
  | val (n : Nat) : Arith
  | app (op : Op) (lhs rhs : Arith) : Arith
deriving DecidableEq, Inhabited, Repr

section arith_syntax

  declare_syntax_cat arith

  syntax "[arith| " arith "]" : term

  syntax:max num : arith

  syntax:30 arith:30 " + " arith:31 : arith
  syntax:35 arith:35 " * " arith:36 : arith

  syntax:max "(" arith ")" : arith

  #check_failure [arith| 1 + 2]
  #check_failure [arith| 1 * 2]
  #check_failure [arith| (1 + 2) * 3]

end arith_syntax

[Asei Inoue]

Next, create a file as following:

import Lean
import LeanByExample.Playground

open Lean

partial def mkArith (stx : Syntax) : Except String Arith :=
  match stx with
  | `(arith| $n:num) =>
    return Arith.val n.getNat
  | `(arith| $l:arith + $r:arith) => do
    return Arith.app Op.add (← mkArith l) (← mkArith r)
  | `(arith| $l:arith * $r:arith) => do
    return Arith.app Op.mul (← mkArith l) (← mkArith r)
  | `(arith| ($e:arith)) => mkArith e
  | _ => throw s!"unexpected syntax: {stx}"

def parseArithOfEnv (s : String) (env : Environment) : Except String Arith := do
  let stx ← Parser.runParserCategory env `arith s
  let arith ← mkArith stx
  return arith

def getEnvIO : IO Environment := do
  let env ← importModules #[{module := `Project.Syntax}] {} (loadExts := true)
  return env

def environment : Environment := unsafe
  match unsafeIO getEnvIO with
    | .error _ => unsafeCast ()
    | .ok env => env

def parseArith (s : String) : Except String Arith := do
  parseArithOfEnv s environment

#eval parseArith "1 + 2 * 3"

[Robin Arnez]

btw the safe way to get environment is to

initialize environment : Environment ← importModules #[{module := `Project.Syntax}] {} (loadExts := true)

[Robin Arnez]

But then you can't use it in the same file, only in files that import the file containing parseArith

[Asei Inoue]

@Robin Arnez

Thank you but your code doesn't work when I run this by lake exe.

[Asei Inoue]

This is a file named LeanByExample/Declarative/Syntax/Environment.lean:

import LeanByExample.Declarative.Syntax.Syntax
import Lean

open Lean

private def fileName : Name := `LeanByExample.Declarative.Syntax.Syntax

initialize env_of_arith_stx : Environment
  ← importModules #[{module := fileName}] {} (loadExts := true)

[Asei Inoue]

My lakefile is:

lean_exe parse where
  root := `Exe.Declarative.Syntax.Parse

The content of Exe.Declarative.Syntax.Parse is:

import LeanByExample.Declarative.Syntax.Environment

def main : IO Unit := do
  IO.println "Hello, Lean!"

Then this fails:

lake exe parse

[Asei Inoue]

error message of lake exe parse is:

lean-by-example on  main [$!?]
❯ lake exe parse
uncaught exception: unknown module prefix 'LeanByExample'

No directory 'LeanByExample' or file 'LeanByExample.olean' in the search path entries:

[Asei Inoue]

importModules is not compatible with lake exe?

[Adam Topaz]

I think you need to set supportInterpreter := true in your lakefile for the exe.

[Asei Inoue]

@Adam Topaz Thank you, but still same error occurs

[Adam Topaz]

do you have a repo on github with your project that I could look at?

[Asei Inoue]

@Adam Topaz Here: https://github.com/lean-ja/lean-by-example/tree/problematic (not main branch)

[Asei Inoue]

checkout and run lake exe parse

[Adam Topaz]

okay, thanks. I don't have time to look right now, but I'll try to do it soon.

[Adam Topaz]

If you want to come up with a more minimal example where it fails, that would be helpful.

[Asei Inoue]

Thank you!

[Asei Inoue]

I will create MWE when I have a time, ok

[Asei Inoue]

@Adam Topaz

I've made a MWE.
see https://github.com/Seasawher/mwe-environment-error and run lake exe mwe-environment-error

[Adam Topaz]

Hmmm... I've never tried initializing an environment like that. Why do you need to do that instead of just using importModules in your main function?

[Asei Inoue]

to make it faster.

[Asei Inoue]

@Robin Arnez proposed using initialize block for Environment. This remove unsafe code and make it faster. (Thanks)

why lake exe fails? Is this a bug?

[Adam Topaz]

I don't know enough about the internals of the compiler to understand why this fails.

[Asei Inoue]

ok. Who to ask..? Who has the knowledge on this problem…?

[Kevin Buzzard]

The people in #**lean4> ?

[Asei Inoue]

who is working on compiler?

[Asei Inoue]

@Henrik Böving Please help me?

[Adam Topaz]

I think your best bet is indeed to ask in #lean4. I'm afraid the answer is going to be "you can't do it this way, and you should use importModules directly in your IO function"

[Henrik Böving]

A couple of things, for one, if you want to actually do this our @Mac Malone has already done a library for this in the past: https://github.com/tydeu/lean4-partax. As for this thing, it's a matter of setting up the search path environment variable correctly I think.

[Asei Inoue]

@Henrik Böving Thank you!

@Mac Malone partax seems to be not updated for long time. Is there small fix to my code?

I want to obtain a parser on String from Lean’s builtin parser. And I want to use syntax command and declare_syntax_cat command because they are easy to use for me.

[Asei Inoue]

And how to fix the search path environment variable?

[Adam Topaz]

initialize env_of_arith_stx : Environment ← do
    initSearchPath (← findSysroot)
    importModules #[{module := `MweEnvironmentError.Basic}] {} (loadExts := true)

This seems to work.

[Adam Topaz]

And indeed that was the only issue. importModules runs in IO, and you need to tell lean where to find the oleans so that it can find MweEnvironmentError.Basic's olean.

[Asei Inoue]

@Adam Topaz Thank you!!!

[Asei Inoue]

deleted

[Asei Inoue]

deleted

[Asei Inoue]

@Adam Topaz @Mac Malone

When supportInterpreter := true is set, then we can not evaluate compiled binary directly...?
Is it impossible to obtain the Environment in the way described above while still keeping the condition that the compiled binary can be executed directly?

[Mac Malone]

@Asei Inoue What do you mean by "can not evaluate the compile binary directly"? There are two distinct limitations here:

• With supportIntepreter := true, Lean is dynamically rather than statically linked to the executable. Thus, to run the executable, libleanshared needs to be available on the system (e.g., in the same directory or in the library path).
• Separately, to use importModules in an executable, the imported module oleans need to be available via LEAN_PATH when the executable is run.

You can avoid importing modules to run a parser if that parser is builtin (e.g., @[builtin_arith_parser] for your example).

[Mac Malone]

In my free time, I have been writing a toy Python interpreter in Lean. The grammar for it is also currently written via syntax and I compile these to builtin parsers , which can then be run in an executable. The code for this may be of interest to you: see here.

[Asei Inoue]

@Mac Malone
Thank you for your reply.

What do you mean by "can not evaluate the compile binary directly"?

.\.lake\build\bin\mwe.exe in shell does not work. (mwe is exeName)

see: https://github.com/Seasawher/mwe-environment-error

[Asei Inoue]

You can avoid import modules to run a parser if that parser is builtin

I'm interested in this. How can I make my parser builtin?

[Mac Malone]

@Asei Inoue Ah, so you are on Windows. In that case, you need Lean's shared libaries to be collocated with your executable when you run it (or in PATH). When distirbuting an executable on Windows, the usual approach is to have an installer that ships the executable along with its necessary shared libraries (and any other resources the executable uses).

[Mac Malone]

Asei Inoue said:

You can avoid import modules to run a parser if that parser is builtin

I'm interested in this. How can I make my parser builtin?

Upon reflection, while it is may be possible to make your parser builitin, I do not think that would be sufficient for your use case. You are also attempting to evaluate the syntax into an Arith expression via term macros, and that kind of evaluation cannot be builtin in the desired way. Thus, you would still need to importModules.

If you defined a custom elaboration attribute and used custom elaborators to build your Arith, you could make both the parsers and the elaborators work around this. However, that is rather complex, and I am not confident that the steps can be well-explained simply through Zulip messages. Hopefully, one day, Lean will have a guide for this kind of thing, but it does not right now.

[Asei Inoue]

@Mac Malone

Thank you. By the way, is there another approach?
For example, can I dump an Environment term to a file and read a file to get an Environment?
then importModules is not needed, I think.

[Mac Malone]

That is not possible.

[Mac Malone]

(OLeans are the essentially this -- nothing simpler will work here.)

[Mac Malone]

Since you are elaborating sophisticated terms in your current code, you need essentially all of what makes Lean, Lean.

[Mac Malone]

There are ways parse and elaborate syntax that do not involve elaborating arbitrary terms, but this would lead to signficantly different code than your original example.

[Mac Malone]

As such, am not sure it woud still be accomplishing your original goal.

[Asei Inoue]

so conclusion is:

my goal

reuse Lean's metaprogramming framework such as

• parser generated by syntax and declare_syntax_cat
• macro expansion rule defined by macro_rules command

and get a parser String → Except String α where α is AST

restriction

This needs importModules and generated binary does not work directly (suitable installer is needed)

---

Thank you

[Asei Inoue]

Sorry I have another question. How to make installer for this?

[Mac Malone]

It has been a long while since I have made a Windows installer, so I am not sure what the best software for this these days is. Perhaps someone else here has some insight (or searching the web might be sufficient).