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

Anomaly Not_found with empty custom entry #15160

Open
Alizter opened this issue Nov 10, 2021 · 0 comments
Open

Anomaly Not_found with empty custom entry #15160

Alizter opened this issue Nov 10, 2021 · 0 comments
Labels
kind: anomaly An uncaught exception has been raised. part: custom The custom notation system. part: notations The notation system.

Comments

@Alizter
Copy link
Contributor

Alizter commented Nov 10, 2021

Description of the problem

Empty custom entries throw a not found exception if used, we should probably catch this and print an error.

Declare Custom Entry FOO.

Axiom bar : Type -> Type.

Notation "[> s <]" := (bar s)
  (s custom FOO at level 105,
  format "[>  s  <]").

Goal forall s, [> s <].
Anomaly
"Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
Raised at Stdlib__hashtbl.find in file "hashtbl.ml", line 539, characters 13-28
Called from LStream.get_loc in file "lib/lStream.ml" (inlined), line 54, characters 2-22
Called from Gramlib__Grammar.GMake.Parsable.parse_parsable.get_parsing_loc in file "gramlib/grammar.ml", line 1614, characters 16-53
Called from Gramlib__Grammar.GMake.Parsable.parse_parsable in file "gramlib/grammar.ml", line 1622, characters 16-34
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Dune__exe__Idetop.add in file "ide/coqide/idetop.ml", line 82, characters 8-64
Called from Dune__exe__Idetop.eval_call.interruptible in file "ide/coqide/idetop.ml", line 443, characters 12-15
Called from Xmlprotocol.abstract_eval_call in file "ide/coqide/protocol/xmlprotocol.ml", line 690, characters 29-44

Coq Version

8.15
c70e317

@Alizter Alizter added part: notations The notation system. kind: anomaly An uncaught exception has been raised. part: custom The custom notation system. labels Nov 10, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: anomaly An uncaught exception has been raised. part: custom The custom notation system. part: notations The notation system.
Projects
None yet
Development

No branches or pull requests

1 participant