We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
--exec
Consider I have a file Main.idr with the following contents:
Main.idr
namespace XX export main : IO () main = putStrLn "Hi, XX!" namespace YY export main : IO () main = putStrLn "Hi, YY!"
If we run
$ idris2 --exec main Main.idr
we expectedly get
Error: Ambiguous elaboration. Possible results: Main.XX.main Main.YY.main
Now, try to specify the namespace by running either
$ idris2 --exec YY.main Main.idr
or
$ idris2 --exec Main.YY.main Main.idr
Runs successfully and prints
Hi, YY!
or at least saying that namespaced main functions are not supported, if so.
Error: Undefined name YY.main.
and
Error: Undefined name Main.YY.main.
The text was updated successfully, but these errors were encountered:
The reason for this behavior is that --exec does not parse the string, but simply wraps it in Basic
Basic
Idris2/src/Idris/SetOptions.idr
Lines 517 to 518 in ec74792
Sorry, something went wrong.
[ fix idris-lang#3398 ] Add name parsing to --exec
3a80c6b
6eebcb2
Successfully merging a pull request may close this issue.
Steps to Reproduce
Consider I have a file
Main.idr
with the following contents:If we run
$ idris2 --exec main Main.idr
we expectedly get
Now, try to specify the namespace by running either
$ idris2 --exec YY.main Main.idr
or
$ idris2 --exec Main.YY.main Main.idr
Expected Behavior
Runs successfully and prints
Hi, YY!
or at least saying that namespaced main functions are not supported, if so.
Observed Behavior
Error: Undefined name YY.main.
and
Error: Undefined name Main.YY.main.
The text was updated successfully, but these errors were encountered: