2

I have been writing some Coq code in Org, but when I try to run a source block, I get the following message:

No org-babel-execute function for coq!

I have tried to initialize the coq language in the org-babel-load-languages variable, but coq isn't an option on the list.

Is there anyway of running coq src blocks outside of the temporary buffer? My overall goal is to be able to define terms in one block and reference them in another, which activating the language should hopefully let me do (I think).

James Leslie
  • 123
  • 5
  • The `org-babel-load-languages` list is not a list of options: it's a list of languages that you have already added to it. You can just `(require 'ob-coq)` to load it in the current session and use it, but if you want it always available, you have to add it to the list as shown in the answer. – NickD May 08 '20 at 22:02
  • I was wrong: customize does present a fixed list of choices as @db48x points out, but it's not up to date (perhaps unsurprisingly). – NickD May 08 '20 at 23:46

1 Answers1

2

It's looking for a function called org-babel-execute:coq and not finding one. Your idea to modify org-babel-load-languages is the right one, since it doesn't load any of these functions by default; you must specifically request that they be loaded.

I've double checked, and my emacs does come with a file called ob-coq.el which looks like it has everything needed for this to work, but Coq is still not one of the choices available when customizing org-babel-load-languages. Apparently it's just not been added to the possible choices for the variable, which is defined in org.el. Maybe they forgot? Or maybe it's experimental still? At any rate, you can still set the value of the variable directly. You can either add something like this to your init file:

(org-babel-do-load-languages 'org-babel-load-languages
                             '((coq . t) …))

Or you can choose "Show Saved Lisp Expression" in the menu you get by clicking the State button, then edit it to add coq to the list.

db48x
  • 15,741
  • 1
  • 19
  • 23
  • There are no choices available when customizing `org-babel-load-languages`: it's just a list and you have to add any language(s) that you want. So the portion of the answer that reads " but Coq is still not one of the choices.... Or maybe it's experimental still?" is wrong. But the rest of the answer is spot-on. Assuming that you fix the wrong part, I will certainly upvote. – NickD May 08 '20 at 21:59
  • Yes, it is a fixed list of choices: https://code.orgmode.org/bzg/org-mode/src/master/lisp/org.el#L240-L307. A quick look at the history shows that it has been like that since 2010. If you've modified the value so that it no longer matches the type that Customize expects, it will show you the raw list instead. Perhaps you have done so. – db48x May 08 '20 at 23:12
  • 1
    You are right - I stand corrected. – NickD May 08 '20 at 23:43
  • @NickD your answer worked for me; however, it seems that this isn't going to be the solution to my overall goal. I now get an error asking to load the file "coq-inferior.el" which is meant to be packaged with Coq, but isn't any more. It seems like a lot of dependencies have also been removed with it, so I will look for a different way to achieve literate programming with coq and org! Thanks again. – James Leslie May 09 '20 at 12:32
  • You meand @db48x's answer? – NickD May 09 '20 at 17:20
  • Oops! Sorry, yes! – James Leslie May 10 '20 at 03:53