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.

Sign up for GitHub

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

Anomaly: Uncaught exception Not_found(_). Please report. (polyproj) #110

Open
JasonGross opened this issue Apr 15, 2014 · 0 comments
Open

Anomaly: Uncaught exception Not_found(_). Please report. (polyproj) #110

JasonGross opened this issue Apr 15, 2014 · 0 comments

Comments

@JasonGross
Copy link 

Inductive paths A (x : A) : A -> Type := idpath : paths A x x.
Notation "x = y" := (@paths _ x y) : type_scope.

Axioms A B : Type.
Axiom P : A = B.
Definition foo : (A = B) * (A = B).
split; abstract (rewrite <- P; reflexivity).
Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)

There's another error that I get on the rewrite, sometimes, but I'm still working on a test case for that one.
@JasonGross JasonGross mentioned this issue Apr 15, 2014
Open
letouzey pushed a commit to coq/coq that referenced this issue Jun 8, 2014
@gares
ind_tables: always declare side effects (Closes: HoTT#110)
e1ba720 
declare takes care of ignoring side effects that are available in the
global environment.  This is yet another instance of what the "abominion"
(aka abstract) can do: the code was checking for the existence in the
environment of the elimination principle, and not regenerating it (nor
declaring the corresponding side effect) if the elimination principle
is used twice.
Of course to functionalize the imperative actions on the environment
when two proofs generated by abstract use the same elim principle,
such elim principle has to be inlined twice, once in each abstracted
proof.  In other words, a side effect generated by a tactic inside
an abstract is *global* but will be made local, si it must always
be declared, no matter what.

Now the system works like this:
- side effects are always declared, even if a caching mechanism thinks
  the constant is already there (it can be there, no need to regenerate it
  but the intent to generate it *must* be declared anyhow)
- at Qed time, we filter the list of side effects and decide which ones are
  really needed to be inlined.

bottom line: STOP using abstract.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@JasonGross