Re: [O] How do I specify the language for a :results code block

2013-12-05 Thread Alan Schmitt
Hello Fabrice,

fni-n...@pirilampo.org writes:

 Hello Alan,

 Alan Schmitt wrote:
 I tried to apply the drawer trick to the :wrap src but it does not work,
 unfortunately. I like your approach better anyway as it allows me to specify
 not only the language used by the output source block, but other properties
 (such as whether it should be evaluated) which wrap does not let me do.

 Not sure this is true. Look at the following tricky example from my slides for
 the stage LaTeX de Dunkerque 2013 [1]:

 #+begin_src org :results latex replace :wrap SRC latex :exports code 
 :exports results
 exemple-liste-itemize
 #+end_src

...

 So, you definitely can pass extra options to the wrap header argument...

Using quotes, of course! Thank you for the heads up.

Alan



Re: [O] How do I specify the language for a :results code block

2013-12-04 Thread Alan Schmitt
Hi Thomas,

 IIUC, your goal is to export the coq source code blocks. Does the
 following, which uses :results org, do what you want? It seems to work
 for me.

It almost works. What I get upon export is an org blog, where I can see
the #+BEGIN_SRC coq marker. The code inside is correctly displayed, though.

 P.S. I remembered :wrap just now. This doesn't export well, though.

 #+call: fetchcoq2(demo.v) :wrap src coq

 #+results:
 #+BEGIN_src coq
 demo.v
 #+END_src

This is very nice! The fact that it does not export well seems to be a
bug. I'll report it (in a new thread). Thank you for the suggestion.

Alan



Re: [O] How do I specify the language for a :results code block

2013-12-04 Thread Alan Schmitt
Hi Sean,

sean.ohal...@gmail.com writes:

 Taking a slightly different approach, you could use the :post header
 argument to wrap the results in a source block.

 See http://orgmode.org/org.html#post (from which the example below is 
 derived).

 For example, you could use something like this:

   #+OPTIONS: d:RESULTS

   * Example

   #+name: eg-1
   #+begin_src sh :results replace drawer :exports results :post
 wrap-src(text=*this*)
   head -n 3 demo.v
   #+end_src

   Output
   #+results: eg-1

   * Utils   :noexport:
   #+name: wrap-src
   #+begin_src emacs-lisp :var text= :results raw
   (concat #+BEGIN_SRC coq\n text \n#+END_SRC)
   #+end_src

Thank you for the suggestion. Unfortunately I get the same problem than
with wrap: if the results are present, they become duplicated in the
export. Here is a small example showing it:

--8---cut here---start-8---
#+name: mywrap
#+BEGIN_SRC sh :exports none :results raw
echo (+ 1 2)
#+END_SRC

Exporting using ~:post~

#+name: wrap-src
#+BEGIN_SRC emacs-lisp :var text= :results raw :exports none
(concat #+BEGIN_SRC emacs-lisp\n text \n#+END_SRC)
#+END_SRC

#+name: test4
#+call: mywrap() :post wrap-src(text=*this*) :results raw

#+RESULTS: test4
#+BEGIN_SRC emacs-lisp
(+ 1 2)

#+END_SRC
--8---cut here---end---8---

If you export this, you will see some duplication of the test4 block.

Your example showed more than the ~:post~ approach: there is also the
use of a drawer. And this solves my export problem (with a drawer,
things are not duplicated). Thanks a lot! (I tried to apply the drawer
trick to the :wrap src but it does not work, unfortunately. I like your
approach better anyway as it allows me to specify not only the language
used by the output source block, but other properties (such as whether
it should be evaluated) which wrap does not let me do.)

 BTW I answered a question similar to this on Stack Overflow recently
 (http://stackoverflow.com/questions/20194347/org-mode-with-code-example-as-html/20232922#20232922)
 - must be something in the air.

I grabbed some additional information from there, and this is what I
ended up with. Thanks again for the help.

--8---cut here---start-8---
#+OPTIONS: d:RESULTS

* utilities:noexport:
#+name: fetchfile
#+BEGIN_SRC sh :exports none :results raw :var f=foo.v
head $f
#+END_SRC

#+name: wrap-coq
#+BEGIN_SRC emacs-lisp :var text= :results raw
(concat #+BEGIN_SRC coq\n text \n#+END_SRC)
#+END_SRC

* example
:PROPERTIES:
:results: drawer
:post: wrap-coq(text=*this*)
:END:

#+call: fetchfile(demo.v)

#+RESULTS:
:RESULTS:
#+BEGIN_SRC coq
Definition toto : forall x, exists y, x = y.

Lemma foo: forall x, x=x.
#+END_SRC
:END:
--8---cut here---end---8---

Alan



Re: [O] How do I specify the language for a :results code block

2013-12-04 Thread Fabrice Niessen
Hello Alan,

Alan Schmitt wrote:
 I tried to apply the drawer trick to the :wrap src but it does not work,
 unfortunately. I like your approach better anyway as it allows me to specify
 not only the language used by the output source block, but other properties
 (such as whether it should be evaluated) which wrap does not let me do.

Not sure this is true. Look at the following tricky example from my slides for
the stage LaTeX de Dunkerque 2013 [1]:

#+begin_src org :results latex replace :wrap SRC latex :exports code :exports 
results
exemple-liste-itemize
#+end_src

It does eval as:

#+results:
#+BEGIN_SRC latex :exports code
\begin{itemize}
\item Premier élément
\begin{itemize}
\item Niveau plus profond
\end{itemize}
\item Autre élément
\item Dernier élément
\end{itemize}
#+END_SRC

which in turn evals (for the export) into the results:

#+results:
#+BEGIN_LaTeX
\begin{itemize}
\item Premier élément
\begin{itemize}
\item Niveau plus profond
\end{itemize}
\item Autre élément
\item Dernier élément
\end{itemize}
#+END_LaTeX

So, you definitely can pass extra options to the wrap header argument...

Best regards,
Fabrice

[1] See http://www.slideshare.net/fniessen/org-modelatexexport or
https://github.com/fniessen/stage-latex-dunkerque-2013/.

-- 
Fabrice Niessen
Leuven, Belgium




Re: [O] How do I specify the language for a :results code block

2013-12-02 Thread Alan Schmitt
t...@tsdye.com writes:

 Alan Schmitt alan.schm...@polytechnique.org writes:

 I tried this alternate approach, to directly generate the block:

 #+name: fetchcoq2
 #+BEGIN_SRC sh :exports none :results raw :var f=demo.v
 echo #+BEGIN_SRC coq
 head $f
 echo
 echo #+END_SRC
 #+END_SRC

 #+call: fetchcoq2(demo.v)

 But then I get a result like this, with extra quoting:

 #+RESULTS:
 : #+BEGIN_SRC coq
 : Definition toto : forall x, exists y, x = y.
 : 
 : Lemma foo: forall x, x=x.
 : #+END_SRC

 I feel like I'm missing something obvious. :results code is exactly
 what I want (put the results in a SRC block), but I don't know how to
 specify the headers of the generated code block.

 You need :results raw at the end of the call line.

 #+name: fetchcoq2
 #+BEGIN_SRC sh :exports none :results raw :var f=demo.v
 echo #+BEGIN_SRC coq
 echo $f
 echo #+END_SRC
 #+END_SRC

 #+results: fetchcoq2
 #+BEGIN_SRC coq
 demo.v
 #+END_SRC

 #+call: fetchcoq2(demo.v) :results raw

 #+results:
 #+BEGIN_SRC coq
 demo.v
 #+END_SRC

Thanks, this is helping me much.

There are still one thing that I don't understand: I cannot make this
work when I have already evaluated the call in the buffer. More
precisely, if I have the following:

--8---cut here---start-8---
#+name: fetchcoq
#+BEGIN_SRC sh :exports none :results raw :var f=foo.v
echo #+BEGIN_SRC coq
head $f
echo
echo #+END_SRC
#+END_SRC

#+call: fetchcoq(f=demo.v) :results raw
--8---cut here---end---8---

when I evaluate the call line, I get this (as expected):

--8---cut here---start-8---
#+name: fetchcoq
#+BEGIN_SRC sh :exports none :results raw :var f=foo.v
echo #+BEGIN_SRC coq
head $f
echo
echo #+END_SRC
#+END_SRC

#+call: fetchcoq(f=demo.v) :results raw

#+RESULTS:
#+BEGIN_SRC coq
Definition toto : forall x, exists y, x = y.

Lemma foo: forall x, x=x.
#+END_SRC
--8---cut here---end---8---

Unfortunately, if I export this, the code is duplicated. Here is the
generated html, for instance:

,
| pre class=src src-coqspan style=color: #FBDE2D;Definition/span 
span style=color: #ff1493;toto/span : span style=color: 
#D8FA3C;forall/span span style=color: #D8FA3C;x/span, span 
style=color: #9370db;exists/span y, x = y.
| 
| span style=color: #FBDE2D;Lemma/span span style=color: 
#ff1493;foo/span: span style=color: #D8FA3C;forall/span span 
style=color: #D8FA3C;x/span, x=x.
| #+END_SRC#+BEGIN_SRC coq
| span style=color: #FBDE2D;Definition/span span style=color: 
#ff1493;toto/span : span style=color: #D8FA3C;forall/span span 
style=color: #D8FA3C;x/span, span style=color: #9370db;exists/span 
y, x = y.
| 
| span style=color: #FBDE2D;Lemma/span span style=color: 
#ff1493;foo/span: span style=color: #D8FA3C;forall/span span 
style=color: #D8FA3C;x/span, x=x.
| /pre
`

Exporting if the result is not in the buffer is fine. I tried adding a
:results replace as inner header argument to the call line and to the
fetchcoq block, but it does not change anything.

How can I tell the call line to replace the results when exporting?

Thanks,

Alan



Re: [O] How do I specify the language for a :results code block

2013-12-02 Thread Sebastien Vauban
Alan Schmitt wrote:
 t...@tsdye.com writes:
 Alan Schmitt alan.schm...@polytechnique.org writes:

 I tried this alternate approach, to directly generate the block:

 #+name: fetchcoq2
 #+BEGIN_SRC sh :exports none :results raw :var f=demo.v
 echo #+BEGIN_SRC coq
 head $f
 echo
 echo #+END_SRC
 #+END_SRC

 #+call: fetchcoq2(demo.v)

 But then I get a result like this, with extra quoting:

 #+RESULTS:
 : #+BEGIN_SRC coq
 : Definition toto : forall x, exists y, x = y.
 : 
 : Lemma foo: forall x, x=x.
 : #+END_SRC

 I feel like I'm missing something obvious. :results code is exactly
 what I want (put the results in a SRC block), but I don't know how to
 specify the headers of the generated code block.

 You need :results raw at the end of the call line.

 #+name: fetchcoq2
 #+BEGIN_SRC sh :exports none :results raw :var f=demo.v
 echo #+BEGIN_SRC coq
 echo $f
 echo #+END_SRC
 #+END_SRC

 #+results: fetchcoq2
 #+BEGIN_SRC coq
 demo.v
 #+END_SRC

 #+call: fetchcoq2(demo.v) :results raw

 #+results:
 #+BEGIN_SRC coq
 demo.v
 #+END_SRC

 Thanks, this is helping me much.

 There are still one thing that I don't understand: I cannot make this
 work when I have already evaluated the call in the buffer. More
 precisely, if I have the following:

 #+name: fetchcoq
 #+BEGIN_SRC sh :exports none :results raw :var f=foo.v
 echo #+BEGIN_SRC coq
 head $f
 echo
 echo #+END_SRC
 #+END_SRC

 #+call: fetchcoq(f=demo.v) :results raw

 when I evaluate the call line, I get this (as expected):

 #+name: fetchcoq
 #+BEGIN_SRC sh :exports none :results raw :var f=foo.v
 echo #+BEGIN_SRC coq
 head $f
 echo
 echo #+END_SRC
 #+END_SRC

 #+call: fetchcoq(f=demo.v) :results raw

 #+RESULTS:
 #+BEGIN_SRC coq
 Definition toto : forall x, exists y, x = y.

 Lemma foo: forall x, x=x.
 #+END_SRC

 Unfortunately, if I export this, the code is duplicated. Here is the
 generated html, for instance:

 ,
 | pre class=src src-coqspan style=color: #FBDE2D;Definition/span
 | span style=color: #ff1493;toto/span : span style=color:
 | #D8FA3C;forall/span span style=color: #D8FA3C;x/span, span
 | style=color: #9370db;exists/span y, x = y.
 | 
 | span style=color: #FBDE2D;Lemma/span span style=color: 
 #ff1493;foo/span: span style=color: #D8FA3C;forall/span span 
 style=color: #D8FA3C;x/span, x=x.
 | #+END_SRC#+BEGIN_SRC coq
 | span style=color: #FBDE2D;Definition/span span style=color:
 | #ff1493;toto/span : span style=color: #D8FA3C;forall/span span
 | style=color: #D8FA3C;x/span, span style=color: 
 #9370db;exists/span
 | y, x = y.
 | 
 | span style=color: #FBDE2D;Lemma/span span style=color: 
 #ff1493;foo/span: span style=color: #D8FA3C;forall/span span 
 style=color: #D8FA3C;x/span, x=x.
 | /pre
 `

 Exporting if the result is not in the buffer is fine. I tried adding a
 :results replace as inner header argument to the call line and to the
 fetchcoq block, but it does not change anything.

 How can I tell the call line to replace the results when exporting?

The syntax of the call line is:

#+call: NAME[HEADER-ARGS-FOR-BLOCK](ARGUMENTS) 
HEADER-ARGS-FOR-CALL-LINE

So, you should add your option either in [] after the name, or at the end of
the line -- I'm always hesitating about where to put the right stuff (not so
enough clear yet in my mind)...

Best regards,
  Seb

-- 
Sebastien Vauban




Re: [O] How do I specify the language for a :results code block

2013-12-02 Thread Alan Schmitt
Hi Sébastien,

sva-n...@mygooglest.com writes:

 Exporting if the result is not in the buffer is fine. I tried adding a
 :results replace as inner header argument to the call line and to the
 fetchcoq block, but it does not change anything.

 How can I tell the call line to replace the results when exporting?

 The syntax of the call line is:

 #+call: NAME[HEADER-ARGS-FOR-BLOCK](ARGUMENTS) 
 HEADER-ARGS-FOR-CALL-LINE

 So, you should add your option either in [] after the name, or at the end of
 the line -- I'm always hesitating about where to put the right stuff (not so
 enough clear yet in my mind)...

I tried both, and neither works. Here is an org file showing the
problem:

--8---cut here---start-8---
#+name: testcall
#+BEGIN_SRC sh :exports none :results raw
echo #+BEGIN_SRC emacs-lisp
echo (+ 1 2)
echo #+END_SRC
#+END_SRC

Test fails:
#+call: testcall() :results raw

#+RESULTS:
#+BEGIN_SRC emacs-lisp
(+ 1 2)
#+END_SRC

Test fails:
#+call: testcall[:results replace]() :results raw

#+RESULTS:
#+BEGIN_SRC emacs-lisp
(+ 1 2)
#+END_SRC

Test fails:
#+call: testcall() :results raw replace

#+RESULTS:
#+BEGIN_SRC emacs-lisp
(+ 1 2)
#+END_SRC

Test succeeds (results not already in the file):
#+call: testcall() :results raw
--8---cut here---end---8---

If you export this, you'll see that only the last call generates the
expected output.

Alan



Re: [O] How do I specify the language for a :results code block

2013-12-02 Thread Thomas S. Dye
Aloha Alan,

Alan Schmitt alan.schm...@polytechnique.org writes:

 Unfortunately, if I export this, the code is duplicated. Here is the
 generated html, for instance:

Yes, the code is partially duplicated when I run it. It looks to me as
if the problem stems from :results raw and the fact that results is
itself a source code block that includes lines like #+BEGIN_SRC and
#+END_SRC.

Perhaps the same confusion shows if you change the :results raw header
argument for the call line to :results org, evaluate, change back to
:results raw, and then evaluate again. You should find an extra
#+END_SRC in the buffer.

IIUC, your goal is to export the coq source code blocks. Does the
following, which uses :results org, do what you want? It seems to work
for me.

#+name: fetchcoq2
#+BEGIN_SRC sh :exports none :results raw :var f=demo.v
echo #+BEGIN_SRC coq
echo $f
echo #+END_SRC
#+END_SRC

#+results: fetchcoq2
#+BEGIN_SRC coq
demo.v
#+END_SRC

#+name: fetchcoq-call
#+call: fetchcoq2(demo.v) :results org

#+results: fetchcoq-call
#+BEGIN_SRC org
,#+BEGIN_SRC coq
demo.v
,#+END_SRC
#+END_SRC

hth,
Tom

P.S. I remembered :wrap just now. This doesn't export well, though.

#+call: fetchcoq2(demo.v) :wrap src coq

#+results:
#+BEGIN_src coq
demo.v
#+END_src

Tom

-- 
T.S. Dye  Colleagues, Archaeologists
735 Bishop St, Suite 315, Honolulu, HI 96813
Tel: 808-529-0866, Fax: 808-529-0884
http://www.tsdye.com



Re: [O] How do I specify the language for a :results code block

2013-12-02 Thread Sean O'Halpin
Hi,

Taking a slightly different approach, you could use the :post header
argument to wrap the results in a source block.

See http://orgmode.org/org.html#post (from which the example below is derived).

For example, you could use something like this:

  #+OPTIONS: d:RESULTS

  * Example

  #+name: eg-1
  #+begin_src sh :results replace drawer :exports results :post
wrap-src(text=*this*)
  head -n 3 demo.v
  #+end_src

  Output
  #+results: eg-1

  * Utils   :noexport:
  #+name: wrap-src
  #+begin_src emacs-lisp :var text= :results raw
  (concat #+BEGIN_SRC coq\n text \n#+END_SRC)
  #+end_src

BTW I answered a question similar to this on Stack Overflow recently
(http://stackoverflow.com/questions/20194347/org-mode-with-code-example-as-html/20232922#20232922)
- must be something in the air.

Regards,
Sean

On Mon, Dec 2, 2013 at 1:04 PM, Alan Schmitt
alan.schm...@polytechnique.org wrote:
 Hi Sébastien,

 sva-n...@mygooglest.com writes:

 Exporting if the result is not in the buffer is fine. I tried adding a
 :results replace as inner header argument to the call line and to the
 fetchcoq block, but it does not change anything.

 How can I tell the call line to replace the results when exporting?

 The syntax of the call line is:

 #+call: NAME[HEADER-ARGS-FOR-BLOCK](ARGUMENTS) 
 HEADER-ARGS-FOR-CALL-LINE

 So, you should add your option either in [] after the name, or at the end of
 the line -- I'm always hesitating about where to put the right stuff (not so
 enough clear yet in my mind)...

 I tried both, and neither works. Here is an org file showing the
 problem:

 --8---cut here---start-8---
 #+name: testcall
 #+BEGIN_SRC sh :exports none :results raw
 echo #+BEGIN_SRC emacs-lisp
 echo (+ 1 2)
 echo #+END_SRC
 #+END_SRC

 Test fails:
 #+call: testcall() :results raw

 #+RESULTS:
 #+BEGIN_SRC emacs-lisp
 (+ 1 2)
 #+END_SRC

 Test fails:
 #+call: testcall[:results replace]() :results raw

 #+RESULTS:
 #+BEGIN_SRC emacs-lisp
 (+ 1 2)
 #+END_SRC

 Test fails:
 #+call: testcall() :results raw replace

 #+RESULTS:
 #+BEGIN_SRC emacs-lisp
 (+ 1 2)
 #+END_SRC

 Test succeeds (results not already in the file):
 #+call: testcall() :results raw
 --8---cut here---end---8---

 If you export this, you'll see that only the last call generates the
 expected output.

 Alan




Re: [O] How do I specify the language for a :results code block

2013-11-30 Thread Alan Schmitt
Hello Thomas and Charles,

ccbe...@ucsd.edu writes:

 A simple example: generate code in sh that is run in emacs-lisp

This is almost what I want, with two differences: I don't want to run
the generated code, but to pretty-print it, and I want to do this with
another language than emacs-lisp.

 #+name: make-elisp
 #+BEGIN_SRC sh :exports none :var fun=+
 echo ( $fun 1 2)
 #+END_SRC

 #+BEGIN_SRC emacs-lisp :noweb yes :exports results
 make-elisp()
 #+END_SRC

 #+RESULTS:
 : 3

 #+BEGIN_SRC emacs-lisp :noweb yes :exports results
 make-elisp(-)
 #+END_SRC

 #+RESULTS:
 : -1

 #+BEGIN_SRC emacs-lisp :noweb yes :exports results
 make-elisp(list)
 #+END_SRC

 #+RESULTS:
 | 1 | 2 |

I tried this, but I cannot make it fit my purpose. What I want is a
function that will create an org mode source block to be exported as
nicely formatted source code.

Here is what I tried:

#+name: fetchcoq
#+BEGIN_SRC sh :exports none :var f=demo.v
head $f
#+END_SRC

#+BEGIN_SRC coq :noweb yes :exports code
fetchcoq(demo.v)
#+END_SRC

If I export this, I get a block with lists, as if the results of
fetchcoq was translated into an elisp data structure:

,
| ((Definition toto : forall x exists y x = y.) (  ) (Lemma foo: 
forall x x=x. ))
`

I tried this alternate approach, to directly generate the block:

#+name: fetchcoq2
#+BEGIN_SRC sh :exports none :results raw :var f=demo.v
echo #+BEGIN_SRC coq
head $f
echo
echo #+END_SRC
#+END_SRC

#+call: fetchcoq2(demo.v)

But then I get a result like this, with extra quoting:

#+RESULTS:
: #+BEGIN_SRC coq
: Definition toto : forall x, exists y, x = y.
: 
: Lemma foo: forall x, x=x.
: #+END_SRC

I feel like I'm missing something obvious. :results code is exactly
what I want (put the results in a SRC block), but I don't know how to
specify the headers of the generated code block.

Thanks,

Alan



Re: [O] How do I specify the language for a :results code block

2013-11-30 Thread Thomas S. Dye
Alan Schmitt alan.schm...@polytechnique.org writes:

 I tried this alternate approach, to directly generate the block:

 #+name: fetchcoq2
 #+BEGIN_SRC sh :exports none :results raw :var f=demo.v
 echo #+BEGIN_SRC coq
 head $f
 echo
 echo #+END_SRC
 #+END_SRC

 #+call: fetchcoq2(demo.v)

 But then I get a result like this, with extra quoting:

 #+RESULTS:
 : #+BEGIN_SRC coq
 : Definition toto : forall x, exists y, x = y.
 : 
 : Lemma foo: forall x, x=x.
 : #+END_SRC

 I feel like I'm missing something obvious. :results code is exactly
 what I want (put the results in a SRC block), but I don't know how to
 specify the headers of the generated code block.

You need :results raw at the end of the call line.

#+name: fetchcoq2
#+BEGIN_SRC sh :exports none :results raw :var f=demo.v
echo #+BEGIN_SRC coq
echo $f
echo #+END_SRC
#+END_SRC

#+results: fetchcoq2
#+BEGIN_SRC coq
demo.v
#+END_SRC

#+call: fetchcoq2(demo.v) :results raw

#+results:
#+BEGIN_SRC coq
demo.v
#+END_SRC

hth,
Tom

-- 
Thomas S. Dye
http://www.tsdye.com



Re: [O] How do I specify the language for a :results code block

2013-11-29 Thread Thomas S. Dye
Aloha Alan,

Alan Schmitt alan.schm...@polytechnique.org writes:

 Hello,

 I'm trying to write a block in some language (right now shell, but it
 will probably be something different) whose output is an org source
 block is some language (here coq). I keep looking at the documentation
 and I cannot see how to specify the language. If I try something like:

 #+BEGIN_SRC sh :results code
 head -n 3 demo.v
 #+END_SRC

 When I evaluate the block I get:

 #+RESULTS:
 #+BEGIN_SRC sh
 Definition toto : forall x, exists y, x = y.

 Lemma foo: forall x, x=x.
 #+END_SRC

 How can I have a block with #+BEGIN_SRC coq instead? I looked at
 http://orgmode.org/manual/Specific-header-arguments.html#Specific-header-arguments
 and at http://orgmode.org/manual/results.html#results and could not find
 where one would specify the language.

I think this can be accomplished by chaining:

#+name: first-link
#+begin_src sh
ECHO XXX
#+end_src

#+begin_src emacs-lisp :var x=first-link()
(princ x)
#+end_src

#+results:
: XXX

hth,
Tom

-- 
Thomas S. Dye
http://www.tsdye.com



Re: [O] How do I specify the language for a :results code block

2013-11-29 Thread Charles Berry
Thomas S. Dye tsd at tsdye.com writes:

 
 Aloha Alan,
 
 Alan Schmitt alan.schmitt at polytechnique.org writes:
 
  Hello,
 
  I'm trying to write a block in some language (right now shell, but it
  will probably be something different) whose output is an org source
  block is some language (here coq). I keep looking at the documentation
  and I cannot see how to specify the language. If I try something like:
[example-deleted]

 
  How can I have a block with #+BEGIN_SRC coq instead?
[snip]
 
 I think this can be accomplished by chaining:
 
[example-deleted]

The problem I see is that the :var x=y() idiom can hand an object to the
src block that is hard to parse and execute -- depending on the language.

If the object is create code in one language and run it in another, it
is sometimes easier to insert results using noweb abc() calls. 

A simple example: generate code in sh that is run in emacs-lisp

#+name: make-elisp
#+BEGIN_SRC sh :exports none :var fun=+
echo ( $fun 1 2)
#+END_SRC

#+BEGIN_SRC emacs-lisp :noweb yes :exports results
make-elisp()
#+END_SRC

#+RESULTS:
: 3

#+BEGIN_SRC emacs-lisp :noweb yes :exports results
make-elisp(-)
#+END_SRC

#+RESULTS:
: -1

#+BEGIN_SRC emacs-lisp :noweb yes :exports results
make-elisp(list)
#+END_SRC

#+RESULTS:
| 1 | 2 |

HTH,

Chuck