coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: Adam Chlipala <adamc AT csail.mit.edu>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Multi-core execution?
- Date: Sat, 9 Mar 2013 14:54:21 -0500
Are the terms sufficiently big that [Set Printing All.] or [Unset Printing Notations.] (possibly together with [Set Printing Implicit.]) would be prohibitively costly?
On Sat, Mar 9, 2013 at 2:27 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:
This would almost work, except that Coq's term parsing and printing are not inverses of each other. I believe almost all of my subgoals would fail to parse back into Coq terms.
On 03/09/2013 02:20 PM, Jason Gross wrote:I'm not sure if you already thought of this, but you could probably script this process, either by an OCaml plugin or a shell script: you could probably use a tactic like
Ltac display_and_solve_by_tac_or_display_db_and_admit tac x y db :=idtac "Tactic: " tac " . Solve Tactic: " y " . Database: " db;x; (solve [ tac ]|| repeat match goal with| [ H : _ |- _ ] => revert H| [ H : _ |- _ ] => fail 2 "cannot revert hypothesis:" H| [ |- ?G ] => idtac "Theorem foo : " G "." y ". Qed. Hint Immediate foo : " db "."; admitend).and call it with something like [ltac:(auto with my_db)] as [tac], some tactic as [x], some string representing a tactic as [y], and ["my_db"] as [db], and then write a script to parse the output of coqc, place the theorems in separate files, run coqc on them, and construct a single file which imports all of the relevant files, and import that file into your original file. (Admittedly, this is a terrible hack, and probably not something you'd want to keep around in a project.)
- [Coq-Club] Multi-core execution?, Adam Chlipala, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, AUGER Cédric, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Jason Gross, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Jason Gross, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, AUGER Cédric, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Pierre-Marie Pédrot, 03/12/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/15/2013
- Re: [Coq-Club] Multi-core execution?, Pierre-Marie Pédrot, 03/12/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, AUGER Cédric, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Jason Gross, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Pierre-Marie Pédrot, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Enrico Tassi, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, Enrico Tassi, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, Enrico Tassi, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, AUGER Cédric, 03/09/2013
Archive powered by MHonArc 2.6.18.