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

Coq doesn't compile in debug mode #6243

Closed
vicuna opened this issue Nov 19, 2013 · 3 comments
Closed

Coq doesn't compile in debug mode #6243

vicuna opened this issue Nov 19, 2013 · 3 comments
Labels

Comments

@vicuna
Copy link

vicuna commented Nov 19, 2013

Original bug ID: 6243
Reporter: @ppedrot
Status: closed (set by @xavierleroy on 2015-12-11T18:25:22Z)
Resolution: fixed
Priority: normal
Severity: major
Version: 4.01.0
Fixed in version: 4.01.1+dev
Category: misc
Monitored by: @gasche

Bug description

Coq trunk compilation in debug mode in 4.01 raises an assertion failure in asmcomp/emitaux.ml at line 226. It seems that CAMLP4 is the faulty one, because it generates dummy locations which break the assertion.

File attachments

@vicuna
Copy link
Author

vicuna commented Nov 19, 2013

Comment author: @mshinwell

I haven't looked at where in camlp4 the problem arises, but I think we should maybe do some work on the compiler side as well.

At the moment, the assertion doesn't seem to be appropriate; the condition being checked is not impossible. I think it would probably be better to catch the construction of locations that are not "no location", but have (e.g.) a zero line number, in [Debuginfo]. I'd actually maybe argue that the interface to that module should be changed so that it isn't possible to (e.g.) retrieve a line number when the location is "none"; and also so that it is possible to (e.g.) encode a location consisting of a source filename but not a line number. I wonder if this latter case is what camlp4 is trying to do.

@vicuna
Copy link
Author

vicuna commented Nov 19, 2013

Comment author: @xavierleroy

Tentative fix (against 4.01) attached. This doesn't fix the Camlp4 issue: it just skips the .loc statement if line is 0, instead of bombing out.

@vicuna
Copy link
Author

vicuna commented Nov 28, 2013

Comment author: @xavierleroy

No feedback. Applied proposed patch to 4.01 bugfix branch (r14321) and to trunk (r14322).

@vicuna vicuna closed this as completed Dec 11, 2015
@vicuna vicuna added the bug label Mar 20, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant