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).

Improve this question
2
  • 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 8, 2020 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 8, 2020 at 23:46

1 Answer 1

Reset to default
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.

Improve this answer
6
  • 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 8, 2020 at 21:59
  • Yes, it is a fixed list of choices: 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 8, 2020 at 23:12
  • 1
    You are right - I stand corrected.
    – NickD
    May 8, 2020 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 9, 2020 at 12:32
  • You meand @db48x's answer?
    – NickD
    May 9, 2020 at 17:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.