The Coq mailing list

["William J. Bowman" <wilbowma AT ccs.neu.edu>]

-- 

Sent from my phoneamajig

On Sep 20, 2019, at 17:47, Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:

I suspect that Solve Obligations closes proofs transparently, which should consume much time to compute something irrelevant.

https://coq.inria.fr/refman/addendum/program.html#coq:flag.transparent-obligations

Program — Coq 8.9.1 documentation

We present here the Program tactic commands, used to build certified Coq programs, elaborating them from their algorithmic skeleton and a rich specification .It can be thought of as a dual of Extraction.The goal of Program is to program as in a regular functional programming language whilst using as rich a specification as desired and proving that the code meets the specification using the ...

coq.inria.fr

> Controls whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Abhishek Anand <abhishek.anand.iitg AT gmail.com>
Sent: September 20, 2019 8:35 PM
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Debugging an apparently diverging Coq program

 

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