The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

Hi,

The reason for the stack overflow could be that Coq's termination checker
unfolds too many and the wrong definitions while trying to verify that the
recursive call is on structurally smaller arguments.

To check whether that's the case, you could try to separate the recursion
pattern of the fixpoint from the body of the fixpoint, so that the fixpoint
is as small as possible and the termination checker can't do anything stupid
while checking it.

This might look as follows (untested, probably won't compile, but hopefully
conveys the idea):

Section test.

Variable T R: Type.

Variable complex_function_body: list T -> R -> R.

Variable base_case: R.

Fixpoint rec(l: list T): R :=
  match l with
  | h :: tl => complex_function_body l (rec tl)
  | nil => base_case
  end.

End test.

Arguments rec {T R}.

Definition LRyamtab_list_rec :=
  rec 
    (fun outer recursiveResult =>
      (fun innev inner 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 <- recursiveResult row.2 inn inn0 row.1] |
                   row <- rows]))
    [:: [::]].


If the above works, you know that the regression is in the termination
checker, and if it fails on the definition of LRyamtab_list_rec, you know
that the regression is in the typechecker and should be independent of
termination checking, so this could be a first step towards tracking down the
problem.

Best,

Sam




On Thu, 2017-12-14 at 22:42 +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
> 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 [:: [::]].