Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
Coq doesn't compile in debug mode #6243
Original bug ID: 6243
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.
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.