Skip to content
New issue

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

Jump to bottom

The --interactive mode does not load the Primitive module #5100

Open
andreasabel opened this issue Dec 15, 2020 · 0 comments
Open

The --interactive mode does not load the Primitive module #5100

andreasabel opened this issue Dec 15, 2020 · 0 comments
Labels
builtin Enhancements to the builtin modules and builtin definitions REPL Interactive toplevel type: bug Issues and pull requests about actual bugs
Milestone
icebox

Comments

@andreasabel
Copy link
Member

I guess it would make sense to load the Primitive module even if no input file was supplied to --interactive.

$ agda --interactive
                 _ 
   ____         | |
  / __ \        | |
 | |__| |___  __| | ___
 |  __  / _ \/ _  |/ __\     Agda Interactive
 | |  |/ /_\ \/_| / /_| \
 |_|  |\___  /____\_____/    Type :? for help.
        __/ /
        \__/

The interactive mode is no longer under active development. Use at your own risk.
Main> Set
1,1-4
Not in scope:
  Set at 1,1-4
when scope checking Set
Main> \ x -> x
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Monad/Builtin.hs:449:31 in Agda-2.6.2-IymqxoxZr9b2Sz3kgFx3aF:Agda.TypeChecking.Monad.Builtin
@andreasabel andreasabel added type: bug Issues and pull requests about actual bugs builtin Enhancements to the builtin modules and builtin definitions REPL Interactive toplevel labels Dec 15, 2020
@jespercockx jespercockx added this to the icebox milestone Jan 31, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
builtin Enhancements to the builtin modules and builtin definitions REPL Interactive toplevel type: bug Issues and pull requests about actual bugs
Projects
None yet
Milestone
icebox
Development

No branches or pull requests
2 participants
@andreasabel @jespercockx