Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear Enrico,

On Fri, Dec 15, 2017 at 12:10:46AM +0100, Enrico Tassi wrote:
> Could you try passing to coqc the -noglob option?
> It is not solving the problem, but will probably make things more
> predictable.

$ make clean
$ make OTHERFLAGS=-noglob

That doesn't seems to change the behavior, ie:

* if implem.v.d is not present, Coq hangs eating slowly all the memory:

$ make OTHERFLAGS=-noglob
"coqdep" -c -R "theories" Combi -R "3rdparty/ALEA" ALEA 
"theories/LRrule/implem.v" > "theories/LRrule/implem.v.d" || ( RV=$?; rm -f 
"theories/LRrule/implem.v.d"; exit ${RV} )
"coqc"  -q  -R "theories" Combi -R "3rdparty/ALEA" ALEA -noglob  
theories/LRrule/implem
File "./theories/LRrule/implem.v", line 16, characters 0-77:
Warning: Notation _ + _ was already used in scope nat_scope.
[notation-overridden,parsing]
[...] # A bunch of similar warnings


* if implem.v.d is present: Coq returns in a second with

$ make OTHERFLAGS=-noglob
"coqc"  -q  -R "theories" Combi -R "3rdparty/ALEA" ALEA -noglob  
theories/LRrule/implem
[...] # same warning as before
File "./theories/LRrule/implem.v", line 127, characters 0-532:
Error: Stack overflow.

Best,

Florent





> 
> > * 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

-- 
Florent Hivert
  ---
   Il y a trois sortes de gens dans le monde : ceux qui savent compter et
ceux qui ne savent pas.
   There are three kinds of people in the world: those who can count,
and those who cannot.
  ---
Professeur, LRI, Univ. Paris Sud 11, CNRS.
Responsable Master 2 CCI
Bureau 33, Laboratoire de Recherche en Informatique (UMR CNRS 8623)
Bâtiment 650, Université Paris Sud 11, 91405 ORSAY CEDEX
Tél: 01-69-15-65-99
http://www.lri.fr/~hivert