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

Runtime exceptions are printed in wrong environment #532

Open
haselwarter opened this issue Apr 11, 2020 · 0 comments
Open

Runtime exceptions are printed in wrong environment #532

haselwarter opened this issue Apr 11, 2020 · 0 comments
Labels

Comments

@haselwarter
Copy link
Member

haselwarter commented Apr 11, 2020

Problem

When a lexing / desugar / typing / runtime / nucleus exception is caught in toplevel.ml, it gets reraised as a toplevel exception. However, when this toplevel exception gets printed, the toplevel state is reset to what it was prior to the evaluation of the current file. For example, if a file extends the nucleus signature, and the exception requires printing of a term judgement, the new symbol is not available in the old signature. This leads to a Fatal error: exception Not_found together with the error message. Similar to #306 .

Example

rule A type
rule B type
rule s : B

let _ = s : A

Fails with

Processing file toplevel_error.m31
Rule A is postulated.
Rule B is postulated.
Rule s is postulated.

Looking up rule s

Toplevel.Error: 
state = initial_environment
File "toplevel_error.m31", line 5, characters 9-13:
Runtime error: unhandled operation ML.coerce 
Looking up rule s

Fatal error: exception Not_found
Raised at file "map.ml", line 135, characters 10-25
Called from file "src/nucleus/signature.ml" (inlined), line 7, characters 48-64
Called from file "src/nucleus/sanity.ml", line 52, characters 14-41
Called from file "src/nucleus/sanity.ml", line 85, characters 27-49
Called from file "src/nucleus/sanity.ml", line 104, characters 22-55
Called from file "src/runtime/runtime.ml", line 700, characters 17-78
Called from file "src/utils/print.ml", line 26, characters 6-19
Called from file "format.ml", line 1252, characters 4-20
Called from file "format.ml", line 1313, characters 16-34
Called from file "format.ml", line 1313, characters 16-34
Called from file "format.ml", line 1252, characters 4-20
Called from file "format.ml", line 1313, characters 16-34
Called from file "format.ml", line 1252, characters 4-20
Called from file "format.ml", line 1252, characters 4-20
Called from file "format.ml", line 1313, characters 16-34
Called from file "src/andromeda.ml", line 183, characters 12-77
Called from file "src/andromeda.ml", line 187, characters 14-63

Compilation exited abnormally with code 2 at Sat Apr 11 15:10:02

(some debugging annotations added)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant