Ssreflect Users Discussion List

[Florent Hivert <>]

      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
whether I delete those two files or not, if I run the script in
Emacs/ProofGeneral I also got the Stack overflow message. The Fixpoint
definition which generate the stack overflow it at the end of this message.

Unfortunately, this happens in the last file of my relatively important
development and I've no idea on how to reduce the bug to something which is
not a dozens of Coq files in a bunch of directory. Moreover, I've no
experience debugging Coq / Ocaml. So I'd like to have some suggestions,
advises or help on how to attack the problem.

Unfortunately, I've no idea if it's a plain Coq problem or if it comes from
SSReflect plugin and no idea on how to investigate this.

Some informations: I'm using

- Coq 8.7.0 installed from Opam using my distrib (OpenSuSE LEAP 42.3) OCaml
compiler which is 4.03.0.
- coq-mathcomp-ssreflect.1.6.4
- coq-mathcomp-fingroup     1.6.4
- coq-mathcomp-algebra      1.6.4
- coq-mathcomp-field        1.6.4
- coq-mathcomp-character    1.6.4
- coq-mathcomp-solvable     1.6.4

- coq-mathcomp-multinomials 1.0

All of those where installed with Opam too.

If you want to try to reproduce the problem:

* clone the repository https://github.com/hivert/Coq-Combi
* and just type make.

The compilation should hang on theories/LRrule/implem.v

Thanks for any help !

Florent Hivert

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 [:: [::]].