The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Dec 31, 2014, at 2:44 , Jason Gross <jasongross9 AT gmail.com> wrote:

This is a bug in coq, you should report it on the bug tracker with code that reproduces it.  If you do not have a small test-case that reproduces it, you can use my coq-bug-minimizer script to construct a small example test-case to reproduce the error, and report that on the bug tracker.  (And please let me know if you have any questions or suggestions about the use of my script.)

The script would be handy as my code uses several 3rd party libraries and part of a bigger project.

I tried the script but no luck so far. The test.v file it produced is 12Mb in size :) The first couple of problems it exhibits

are repeating definitions like this in test.v:

Module .

Module .

Module .

After removing them the next one is:

Import CoLoR_DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT_Volumes_DOT_CoqLibs_DOT_color_DOT_color_DOT_Util_DOT_Logic_DOT_LogicUtil.CoLoR..

Import CoLoR_DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT_Volumes_DOT_CoqLibs_DOT_color_DOT_color_DOT_Util_DOT_Logic_DOT_LogicUtil.CoLoR...

Import CoLoR_DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT__DOT_Volumes_DOT_CoqLibs_DOT_color_DOT_color_DOT_Util_DOT_Logic_DOT_LogicUtil.CoLoR....

Apparently these are an artifacts produced by the script as there original code does not seem to have constructs like this.

I honestly wish to help to locate this bug in Coq but I do not want to submit all my source code as an example how to reproduce it. If there is a way to dump coq state at the time it occurs I can do that.

Meanwhile I am going to change the code which exhibits the bug as I realized it needs to be implemented differently, and hopefully it won’t be triggered by my new implementation.

Sincerely,
Vadim Zaliva

--

CMU ECE PhD student

Mobile: +1(510)220-1060

Skype: vzaliva