Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Multi-core execution?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Multi-core execution?


Chronological Thread 
  • 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 "."; admit
                 end).
                   
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.)





Archive powered by MHonArc 2.6.18.

Top of Page