coqc loops(?) when coqtop doesn't

[JasonGross]

At https://github.com/JasonGross/HoTT/tree/be130e7b72e8b5bf804e3612b095de0ba01d864c, time ./hoqtop < theories/categories/Limits/Functors.v finishes in under 1 second, while hoqc theories/categories/Limits/Functors.v spins for a quite a while.

[JasonGross]

It seems to be looping on the End colimit. command, or the section start right after that.

[mattam82]

You're sure you're in no-native-compiler mode ?

Le samedi 28 décembre 2013, Jason Gross a écrit :

It seems to be looping on the End colimit. command, or the section start right after that.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/coq/issues/65#issuecomment-31299767 .

-- Matthieu

[JasonGross]

hoqc definately passes -no-native-compiler, though I don't think I passed -no-native-compiler to ./configure. Should I have?

[mattam82]

Just to be sure that's not it, I would try.

Le samedi 28 décembre 2013, Jason Gross a écrit :

hoqc definately passes -no-native-compiler, though I don't think I passed -no-native-compiler to ./configure. Should I have?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/coq/issues/65#issuecomment-31300480 .

-- Matthieu

[JasonGross]

Looking back at my bash history, I believe I did pass -no-native-compiler to configure. But I will build it again to be sure.

[JasonGross]

I've tried building again with -no-native-compiler; ./hoqc -time ... still gives me

Chars 0 - 69 [Require~Import~Category.Core~F...] Chars 70 - 120 [Require~Import~Comma.Core~Init...] Chars 121 - 178 [Require~Import~KanExtensions.C...] Chars 179 - 206 [Require~Import~Limits.Core.] Chars 207 - 249 [Require~Import~Adjoint.Univers...] Chars 250 - 286 [Require~Import~FunctorCategory...] Chars 287 - 315 [Require~Import~Adjoint.Core.] Chars 316 - 367 [Require~Import~InitialTerminal...] Chars 369 - 395 [Set~Universe~Polymorphism.] Chars 396 - 419 [Set~Implicit~Arguments.] Chars 420 - 448 [Generalizable~Variables~all.] Chars 449 - 473 [Set~Asymmetric~Patterns.] Chars 517 - 549 [Local~~Open~Scope~category_sco...] Chars 551 - 568 [Section~functors.] Chars 571 - 589 [Context~~`{Funext}.] Chars 592 - 617 [Variable~C~:~PreCategory.] Chars 620 - 645 [Variable~D~:~PreCategory.] Chars 649 - 665 [Section~colimit.] Chars 835 - 967 [Variable~~~colimits~:~~~~~fora...] Chars 972 - 1086 [Variable~~~has_colimits~:~fora...] Chars 1377 - 1483 [Definition~colimit_functor~:~F...] Chars 1489 - 1619 [Definition~colimit_adjunction~...] Chars 1622 - 1634 [End~colimit.]

and then sits there ~forever.