[Agda] Possibly infinite/exponential compilation time by just calling a certain function

[Jan Bracker]

I would certainly appreciate the effort if this is properly merged into the
next stable release!

I plan to use some of my proofs in a paper and it would be very
disappointing if people needed to use a modified compiler to be able to
verify them.

2017-06-30 15:27 GMT+01:00 Andrea Vezzosi <sanzhiyan at gmail.com>:

> On Fri, Jun 30, 2017 at 3:14 PM, Jan Bracker <jan.bracker at googlemail.com>
> wrote:
> > @Wolfram: That patch is amazing!
> > I patched it into the 2.5.2 stable release and it compiled the postulates
> > within a matter of seconds. Before the patch it wasn't done after 90+
> > minutes.
> > Is this going to be included in the release of 2.5.3? I hope it will be.
> > I do feel a bit of a twinge modifying the compiler to make my proofs type
> > check. I hope this does not introduce any inconsistencies or problems?
> > I rechecked all of my code and as far as I can tell none of my work takes
> > longer to compile. If anything it all appears to compile quicker now,
> though
> > I do not have actual numbers to back this up.
>
> That patch is not planned to be merged, because it's more of an
> experiment. However if it helps so much it's tempting to try and do a
> proper job of comparing definitions without reducing them as much.
>
> It shouldn't introduce inconsistencies, it might however reject some
> programs that would otherwise be accepted, because it makes the
> typechecker heuristically assume things like:
> if (_A + _B) = (e1 + e2) then _A = e1 and _B = e2.
>
> while the program might need different solutions for _A and _B to
> typecheck.
>
> Best,
> Andrea
>
>
> > I hope I don't hit another performance wall any time soon.
> >
> > Best,
> > Jan
> >
> > 2017-06-28 10:41 GMT+01:00 Nils Anders Danielsson <nad at cse.gu.se>:
> >>
> >> On 2017-06-27 17:09, Jan Bracker wrote:
> >>>
> >>> I tried to add the last postulate I need, but even though I now have
> >>> marked all of the proofs as abstract the compilation time is again at
> >>> 30+ minutes with no end in sight:
> >>
> >>
> >> Some other things to try:
> >>
> >> * Use copatterns to define records.
> >>
> >> * Turn off η-equality for record types.
> >>
> >> (I don't know if either of these things will help.)
> >>
> >> --
> >> /NAD
> >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170630/c66dd89f/attachment.html>