The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Note that if you instantiate the three variables the computation is instantaneous also inside Coq. No need to extract to ocaml there.

(* Parameter atom : Type. *)
Definition atom := nat.
(* Parameter atomeq_dec : forall x y : atom, {x = y} + {x <> y}. *)
Definition atomeq_dec := Nat.eq_dec.

...

(* Parameter fresh : atoms -> atom. *)
Definition fresh (s:atoms): atom :=
  set_fold_left (fun acc x => if le_gt_dec acc x then x else acc) s 0.

Le lun. 23 sept. 2019 à 19:47, William J. Bowman <wjb AT williamjbowman.com> a écrit :

Thanks all for the feedback!

This should give me plenty of places to continue debugging and some workarounds
if it's simply a limitation of the code generated by Program.

--
William J. Bowman

PS: Sorry for my mis-sent empty email.

On Mon, Sep 23, 2019 at 07:36:54PM +0200, Xavier Leroy wrote:
> On Mon, Sep 23, 2019 at 7:19 PM Jason -Zhong Sheng- Hu <
> fdhzs2010 AT hotmail.com> wrote:
>
> > have you tried to extract to ocaml or haskell to reduce noise from Prop?
> >
>
> "Program Fixpoint" produces terms that don't play well with extraction:
> https://github.com/coq/coq/issues/10757
>
> The problem could come from accessibility proofs that don't compute.  The
> following trick can help:
> https://sympa.inria.fr/sympa/arc/coq-club/2013-09/msg00034.html
>
> - Xavier Leroy
>
>
> >
> > *Thanks,*
> > *Jason Hu*
> > *https://hustmphrrr.github.io/ <https://hustmphrrr.github.io/>*
> > ------------------------------
> > *From:* coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf
> > of William J. Bowman <wilbowma AT ccs.neu.edu>
> > *Sent:* September 20, 2019 8:46 PM
> > *To:* coq-club AT inria.fr <coq-club AT inria.fr>
> > *Subject:* Re: [Coq-Club] Debugging an apparently diverging Coq program
> >
> > I don’t think that’s the problem. Another model does get stuck on that
> > equality and returns the if statement waiting for an interpretation of
> > “==“. I didn’t expect Program to be efficient, but I do expect it to
> > terminate quickly on this example, without using 20 GB of memory.
> >
> > I’ll see if I can reduce the other model to something as small.
> >
> > --
> > Sent from my phoneamajig
> >
> > On Sep 20, 2019, at 17:35, Abhishek Anand <abhishek.anand.iitg AT gmail.com>
> > wrote:
> >
> > Perhaps they forgot to instantiate the atom type?  the computation would
> > get stuck on (x == x'). `Program` often produces humongous functions.
> >
> > -- Abhishek
> > http://www.cs.cornell.edu/~aa755/
> >
> >
> > On Fri, Sep 20, 2019 at 5:15 PM William J. Bowman <wjb AT williamjbowman.com>
> > wrote:
> >
> > All,
> >
> > At the following URL is a model of a language with capture-avoiding
> > substitution
> > that a student wrote:
> >
> >   https://gist.github.com/wilbowma/acf125222c64ff715a33b26a0ce8b4ab
> >
> > The program looks (to me) like it ought to terminate quickly, and it's
> > proven
> > terminating using Program, yet when we run the substitution function on a
> > small
> > example... coqtop eats about 20 GB of memory and doesn't terminate within 5
> > minutes.
> > I'm using Coq 8.9.1 on MacOS 10.14.2; the same behavior is also observed on
> > Windows 10.
> >
> > I'd appreciate any help debugging this.
> >
> > --
> > William J. Bowman
> >
> >