Ssreflect Users Discussion List

[Enrico Tassi <>]

On Thu, Dec 14, 2017 at 10:42:32PM +0100, Florent Hivert wrote:
>       Dear all,
> 
> I've just hit a problem when upgrading Coq from 8.6 to 8.7.0. My code works
> perfectly with 8.5 and 8.6, but when switching with 8.7.0, the symptom is 
> that
> when compiling in batch coqc run forever during the first make. Interrupting
> with ctrl+c and relauching make gives:
> 
>    File "./theories/LRrule/implem.v", line 127, characters 0-532:
>    Error: Stack overflow.
> 
> Deleting implem.glob and implem.v.d restores the run for ever behavior.  
> Also

Could you try passing to coqc the -noglob option?
It is not solving the problem, but will probably make things more
predictable.

> * clone the repository https://github.com/hivert/Coq-Combi
> * and just type make.
> 
> The compilation should hang on theories/LRrule/implem.v
> 
> Fixpoint LRyamtab_list_rec innev inner outer sh0 row0 :=
>   if outer is out0 :: out then
>     let inn0 := head 0 inner in let inn := behead inner in
>     let rowres := yamtab_row innev (take (out0 - sh0) row0) in
>     let rows :=
>         flatten [seq yamtab_shift res.2 (head (size innev) res.1)
>                      ((minn sh0 out0) - inn0) res.1
>                 | res <- rowres ] in
>     flatten [seq [seq row.1 :: tab |
>                   tab <- LRyamtab_list_rec row.2 inn out inn0 row.1] |
>              row <- rows]
>   else [:: [::]].

I think you should open an issue at https://github.com/coq/coq the the
instruction above. 

Best,
-- 
Enrico Tassi