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 UGraph.AlreadyDeclared." #7795

Closed
jad-hamza opened this issue Jun 13, 2018 · 2 comments
Closed

Anomaly "Uncaught exception UGraph.AlreadyDeclared." #7795

jad-hamza opened this issue Jun 13, 2018 · 2 comments
Labels
kind: anomaly An uncaught exception has been raised. part: universes The universe system.
Milestone
8.8.2

Comments

@jad-hamza
Copy link

Version

8.8.0
coq-stdpp dev.2018-06-10.1.aa942ca8

Operating system

Debian

Description of the problem

https://gist.github.com/jad-hamza/4dd6d528a353d8268a39a89da0668f72

This example gives the error message:

Error: Anomaly "Uncaught exception UGraph.AlreadyDeclared."

Maybe related to #7792?

Removing the stdpp.set import prevents the problem. I'm not sure whether this is a Coq bug or a stdpp problem, so I also posted there: https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/issues/20
@SkySkimmer SkySkimmer added part: universes The universe system. kind: anomaly An uncaught exception has been raised. labels Aug 22, 2018
@SkySkimmer
Copy link
Contributor

Is it possible to minimize to the point there are no 3rd party libraries?

@jad-hamza
Copy link
Author

jad-hamza commented Aug 22, 2018 •
edited

Yes, here is the new version: https://gist.github.com/jad-hamza/596a7bd0babb7fb16b6b6038b35b6410
(Program Mode is still necessary for the bug)

Edit: on version 8.8.1

SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Aug 23, 2018
@SkySkimmer
Fix coq#7795: UGraph.AlreadyDeclared with Program
b17d809 
This change is based on noticing that we use a default value for the
`sideff` argument even though we have a similarly named `side_eff`
available. Someone who knows how side effects and universes are
supposed to interact should check this.
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Aug 23, 2018
@SkySkimmer
Fix coq#7795: UGraph.AlreadyDeclared with Program
18839cf 
This change is based on noticing that we use a default value for the
`sideff` argument even though we have a similarly named `side_eff`
available. Someone who knows how side effects and universes are
supposed to interact should check this.
mattam82 added a commit that referenced this issue Sep 6, 2018
@mattam82
Merge PR #8302: Fix #7795: UGraph.AlreadyDeclared with Program
3af27f4
ejgallego pushed a commit to ejgallego/coq that referenced this issue Sep 6, 2018
@SkySkimmer @ejgallego
Fix coq#7795: UGraph.AlreadyDeclared with Program
585d386 
This change is based on noticing that we use a default value for the
`sideff` argument even though we have a similarly named `side_eff`
available. Someone who knows how side effects and universes are
supposed to interact should check this.
Zimmi48 pushed a commit that referenced this issue Sep 7, 2018
@SkySkimmer @coqbot
Fix #7795: UGraph.AlreadyDeclared with Program
54e32b4 
This change is based on noticing that we use a default value for the
`sideff` argument even though we have a similarly named `side_eff`
available. Someone who knows how side effects and universes are
supposed to interact should check this.

(cherry picked from commit e705297)
Zimmi48 pushed a commit that referenced this issue Sep 7, 2018
@coqbot
Backport PR #8302: Fix #7795: UGraph.AlreadyDeclared with Program
dd0cf72
Zimmi48 pushed a commit to Zimmi48/coq that referenced this issue Sep 28, 2018
@SkySkimmer @Zimmi48
Fix coq#7795: UGraph.AlreadyDeclared with Program
affc97c 
This change is based on noticing that we use a default value for the
`sideff` argument even though we have a similarly named `side_eff`
available. Someone who knows how side effects and universes are
supposed to interact should check this.

(cherry picked from commit e705297)
@Zimmi48 Zimmi48 mentioned this issue Sep 28, 2018
Merged
@Zimmi48 Zimmi48 added this to the 8.8.2 milestone Sep 28, 2018
Zimmi48 pushed a commit to Zimmi48/coq that referenced this issue Sep 28, 2018
@SkySkimmer @Zimmi48
Fix coq#7795: UGraph.AlreadyDeclared with Program
5fec5b9 
This change is based on noticing that we use a default value for the
`sideff` argument even though we have a similarly named `side_eff`
available. Someone who knows how side effects and universes are
supposed to interact should check this.

(cherry picked from commit e705297)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: anomaly An uncaught exception has been raised. part: universes The universe system.
Projects
None yet
Milestone
8.8.2
Development

No branches or pull requests
3 participants
@Zimmi48 @SkySkimmer @jad-hamza