search

HoTT / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
http://coq.inria.fr/
GNU Lesser General Public License v2.1
27 stars 5 forks source link

coqc loops(?) when coqtop doesn't #65

Open JasonGross opened 10 years ago

JasonGross commented 10 years ago

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 commented 10 years ago

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

mattam82 commented 10 years ago

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 commented 10 years ago

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

mattam82 commented 10 years ago

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 commented 10 years ago

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 commented 10 years ago

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.