Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom

[Isabelle2020] Incomprehensible Error Message #29

Open
wimmers opened this issue May 3, 2020 · 0 comments
Open

[Isabelle2020] Incomprehensible Error Message #29

wimmers opened this issue May 3, 2020 · 0 comments
Labels
bug Something isn't working good first issue Good for newcomers

Comments

@wimmers
Copy link
Collaborator

wimmers commented May 3, 2020

If one uses imports Main instead of import Defs one gets the following incomprehensible error message:
Internal error | writing theory files failed - (list index out of range)
We should improve on this, as new users will likely run into that error very often.
@wimmers wimmers added bug Something isn't working good first issue Good for newcomers labels May 3, 2020
# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
bug Something isn't working good first issue Good for newcomers
Milestone
No milestone
Development

No branches or pull requests
1 participant
@wimmers