added ability to loadDynlib through command line flag

[FrederickPu]

User can specify dynlibs when running lean repl using command line flag lake env path/to/repl --dynlib pathtodynlib1.so pathtodynlib2.so ...

Added general interface for creating command line flags

[FrederickPu]

I'm trying to make a test for loading dynlibs but seems to crash whenever you actually call the extern function

@FrederickPu ➜ /workspaces/repl/test/dynlib (dynlib-option) $ lake env ../../.lake/build/bin/repl --dynlib lib/libmylib.so 
Loading dynlib: lib/libmylib.so
{ "cmd": "@[extern \"add\"]\nopaque add (a b : UInt32) : UInt32\n" }                        

{"env": 0}

{ "cmd": "#eval 2 + 2" }

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 5},
   "data": "4"}],
 "env": 1}

{ "cmd": "#eval 2 + 2", "env": 0} 

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 5},
   "data": "4"}],
 "env": 2}

{ "cmd": "#eval add 2 2", "env": 0}

The cmakelists.txt and .c file can be found in test/dynlib

[tydeu]

@FrederickPu You cannot define an @[extern[ definition and then #eval it in the same environment. The @[extern] definition would need to be in a separate module that is compiled, loaded as a dynlib, and then imported into the REPL.

[FrederickPu]

thx.
but the fact that the repl just exits without printing anything is also an error handling issue right?

[FrederickPu]

Also even when I put it into a compiled module it still fails:

@FrederickPu ➜ /workspaces/repl/test/dynlib (dynlib-option) $ lake env ../../.lake/build/bin/repl --dynlib lib/libmylib.so
Loading dynlib: lib/libmylib.so
{ "cmd": "import Dynlib" }

{"env": 0}

{ "cmd": "#eval add 2 2", "env": 0 }

@FrederickPu ➜ /workspaces/repl/test/dynlib (dynlib-option) $ 

[FrederickPu]

I've just pushed my changes to the test/dynlib folder

[tydeu]

@FrederickPu

Also even when I put it into a compiled module it still fails

The imported module itself has to be compiled into the dynlib, not just the FFI code. That is, the Lean module Dynlib needs to be compiled into a dynlib, loaded, and imported.

[FrederickPu]

now i get the following issue:

lake env ../../.lake/build/bin/repl --dynlib ./.lake/build/lib/libmylib.so 
Loading dynlib: ./.lake/build/lib/libmylib.so
{ "cmd": "import Dynlib" }

{"env": 0}

{ "cmd": "#eval add 2 2", "env": 0 }

{"messages":
 [{"severity": "error",
   "pos": {"line": 1, "column": 6},
   "endPos": {"line": 1, "column": 13},
   "data": "unknown constant 'Unit'"}],
 "env": 1}