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
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_foundtogether with the error message. Similar to #306 .Example
Fails with
(some debugging annotations added)