Skip to content

avoid warnings emitted by Coq#76

Open
ybertot wants to merge 3 commits into
rocq-community:coq-masterfrom
ybertot:coq-deprecation-8.13
Open

avoid warnings emitted by Coq#76
ybertot wants to merge 3 commits into
rocq-community:coq-masterfrom
ybertot:coq-deprecation-8.13

Conversation

@ybertot

@ybertot ybertot commented Sep 24, 2020

Copy link
Copy Markdown
Collaborator

Only modifications in the Coq source files.

@Karmaki

Karmaki commented Oct 29, 2020

Copy link
Copy Markdown
Collaborator

Sorry to be late, but now, it seems that there are still some warnings, and moreover, it fails on:

Error: Unbound module Names.GlobRef.Ordered_env

A version problem?

@ybertot ybertot force-pushed the coq-deprecation-8.13 branch from cf22d16 to ec2d8bf Compare October 29, 2020 12:07
@ybertot

ybertot commented Oct 29, 2020

Copy link
Copy Markdown
Collaborator Author

After git rebase, it seems the error has disappeared.

@ybertot

ybertot commented Oct 30, 2020

Copy link
Copy Markdown
Collaborator Author

Only the test-suite fails, and it seems this is only due to re-ordering in the graph.

@Karmaki

Karmaki commented Oct 30, 2020

Copy link
Copy Markdown
Collaborator

What about merging your other PR into this one and updating the oracles? Sorry, but I prefer not to merge a branch where the tests fail...

@ybertot

ybertot commented Oct 30, 2020

Copy link
Copy Markdown
Collaborator Author

I agree on the point concerning not merging a branch where tests fails.

@ybertot

ybertot commented Oct 30, 2020

Copy link
Copy Markdown
Collaborator Author

Some of the changes cannot be fixed by sorting results. It seems there was a symbol for the section variable A that was removed and it shifts the indices of all nodes (this is for the graph.dpd file).

@Karmaki

Karmaki commented Oct 30, 2020

Copy link
Copy Markdown
Collaborator

OK, but if it looks "normal" (I mean, due to coq internal modifications), you can just copy the new results in the oracles, and it will be ok then.

@ybertot

ybertot commented Oct 30, 2020

Copy link
Copy Markdown
Collaborator Author

I agree, I am checking the normalcy of the graph just now.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants