coqidetop.opt returned non-zero exit status 2

[nthiery]

Hello,

With @amahboubi, we are trying to use coq_jupyter in Jupyter Lab. The kernel
is however crashing on start up. Any clue?

Thanks in advance,

How to reproduce

mamba install coq-jupyter
...
  Install:
  + coq                 8.12.0  0                conda-forge/linux-64     135MB
  + coq-jupyter          1.6.0  py310hff52083_2  conda-forge/linux-64      35kB
  + ocaml               4.06.1  h14c3975_1007    conda-forge/linux-64      91MB
  + ocaml-findlib        1.8.1  0                conda-forge/linux-64       1MB
  + ocaml-num              1.2  0                conda-forge/linux-64     376kB
...

log for: jupyter console --kernel=coq

Fatal error: exception Not_found
[IPKernelApp] ERROR | CoqtopError has occured. Scheduling shutdown.
Traceback (most recent call last):
  File "/opt/conda/lib/python3.10/site-packages/coq_jupyter/coqtop.py", line 39, in __init__
    banner = check_output([cmd, '--version']).decode('utf-8')
  File "/opt/conda/lib/python3.10/subprocess.py", line 421, in check_output
    return run(*popenargs, stdout=PIPE, timeout=timeout, check=True,
  File "/opt/conda/lib/python3.10/subprocess.py", line 526, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command '['coqidetop.opt', '--version']' returned non-zero exit status 2.
During handling of the above exception, another exception occurred:
Traceback (most recent call last):

File "/opt/conda/lib/python3.10/site-packages/coq_jupyter/kernel.py", line 59, in wrapper

return function(self, *args, **kwargs)

File "/opt/conda/lib/python3.10/site-packages/coq_jupyter/kernel.py", line 100, in init

self._coqtop = Coqtop(self, self.coqtop_executable, self.coqtop_args)

File "/opt/conda/lib/python3.10/site-packages/coq_jupyter/coqtop.py", line 73, in init

raise_with_traceback(CoqtopError("Cause: {}".format(repr(e))))

File "/opt/conda/lib/python3.10/site-packages/future/utils/init.py", line 449, in raise_with_traceback

raise exc.with_traceback(traceback)

File "/opt/conda/lib/python3.10/site-packages/coq_jupyter/coqtop.py", line 39, in init

banner = check_output([cmd, '--version']).decode('utf-8')

File "/opt/conda/lib/python3.10/subprocess.py", line 421, in check_output

return run(*popenargs, stdout=PIPE, timeout=timeout, check=True,

File "/opt/conda/lib/python3.10/subprocess.py", line 526, in run

raise CalledProcessError(retcode, process.args,

coq_jupyter.coqtop.CoqtopError: Cause: CalledProcessError(2, ['coqidetop.opt', '--version'])

Traceback (most recent call last):

File "/opt/conda/lib/python3.10/site-packages/coq_jupyter/coqtop.py", line 39, in init

banner = check_output([cmd, '--version']).decode('utf-8')

File "/opt/conda/lib/python3.10/subprocess.py", line 421, in check_output

return run(*popenargs, stdout=PIPE, timeout=timeout, check=True,

File "/opt/conda/lib/python3.10/subprocess.py", line 526, in run

raise CalledProcessError(retcode, process.args,

subprocess.CalledProcessError: Command '['coqidetop.opt', '--version']' returned non-zero exit status 2.
During handling of the above exception, another exception occurred:
Traceback (most recent call last):

File "/opt/conda/lib/python3.10/runpy.py", line 196, in _run_module_as_main

return _run_code(code, main_globals, None,

File "/opt/conda/lib/python3.10/runpy.py", line 86, in _run_code

exec(code, run_globals)

File "/opt/conda/lib/python3.10/site-packages/coq_jupyter/main.py", line 5, in 

IPKernelApp.launch_instance(kernel_class=CoqKernel, args=argv)

File "/opt/conda/lib/python3.10/site-packages/traitlets/config/application.py", line 1040, in launch_instance

app.initialize(argv)

File "/opt/conda/lib/python3.10/site-packages/traitlets/config/application.py", line 113, in inner

return method(app, *args, **kwargs)

File "/opt/conda/lib/python3.10/site-packages/ipykernel/kernelapp.py", line 692, in initialize

self.init_kernel()

File "/opt/conda/lib/python3.10/site-packages/ipykernel/kernelapp.py", line 540, in init_kernel

kernel = kernel_factory(

File "/opt/conda/lib/python3.10/site-packages/traitlets/config/configurable.py", line 551, in instance

inst = cls(*args, **kwargs)

File "/opt/conda/lib/python3.10/site-packages/coq_jupyter/kernel.py", line 59, in wrapper

return function(self, *args, **kwargs)

File "/opt/conda/lib/python3.10/site-packages/coq_jupyter/kernel.py", line 100, in init

self._coqtop = Coqtop(self, self.coqtop_executable, self.coqtop_args)

File "/opt/conda/lib/python3.10/site-packages/coq_jupyter/coqtop.py", line 73, in init

raise_with_traceback(CoqtopError("Cause: {}".format(repr(e))))

File "/opt/conda/lib/python3.10/site-packages/future/utils/init.py", line 449, in raise_with_traceback

raise exc.with_traceback(traceback)

File "/opt/conda/lib/python3.10/site-packages/coq_jupyter/coqtop.py", line 39, in init

banner = check_output([cmd, '--version']).decode('utf-8')

File "/opt/conda/lib/python3.10/subprocess.py", line 421, in check_output

return run(*popenargs, stdout=PIPE, timeout=timeout, check=True,

File "/opt/conda/lib/python3.10/subprocess.py", line 526, in run

raise CalledProcessError(retcode, process.args,

coq_jupyter.coqtop.CoqtopError: Cause: CalledProcessError(2, ['coqidetop.opt', '--version'])

Traceback (most recent call last):

File "/opt/conda/lib/python3.10/site-packages/jupyter_console/ptshell.py", line 434, in init_kernel_info

reply = self.client.get_shell_msg(timeout=1)

File "/opt/conda/lib/python3.10/site-packages/jupyter_client/utils.py", line 30, in wrapped

raise e

File "/opt/conda/lib/python3.10/site-packages/jupyter_client/utils.py", line 27, in wrapped

return loop.run_until_complete(future)

File "/opt/conda/lib/python3.10/site-packages/nest_asyncio.py", line 90, in run_until_complete

return f.result()

File "/opt/conda/lib/python3.10/asyncio/futures.py", line 201, in result

raise self._exception.with_traceback(self._exception_tb)

File "/opt/conda/lib/python3.10/asyncio/tasks.py", line 232, in __step

result = coro.send(None)

File "/opt/conda/lib/python3.10/site-packages/jupyter_client/client.py", line 143, in _async_get_shell_msg

return await self.shell_channel.get_msg(*args, **kwargs)

File "/opt/conda/lib/python3.10/site-packages/jupyter_client/channels.py", line 230, in get_msg

raise Empty

_queue.Empty
The above exception was the direct cause of the following exception:
Traceback (most recent call last):

File "/opt/conda/bin/jupyter-console", line 8, in 

sys.exit(main())

File "/opt/conda/lib/python3.10/site-packages/jupyter_core/application.py", line 277, in launch_instance

return super().launch_instance(argv=argv, **kwargs)

File "/opt/conda/lib/python3.10/site-packages/traitlets/config/application.py", line 1040, in launch_instance

app.initialize(argv)

File "/opt/conda/lib/python3.10/site-packages/traitlets/config/application.py", line 113, in inner

return method(app, *args, **kwargs)

File "/opt/conda/lib/python3.10/site-packages/jupyter_console/app.py", line 136, in initialize

self.init_shell()

File "/opt/conda/lib/python3.10/site-packages/jupyter_console/app.py", line 106, in init_shell

self.shell = ZMQTerminalInteractiveShell.instance(parent=self,

File "/opt/conda/lib/python3.10/site-packages/traitlets/config/configurable.py", line 551, in instance

inst = cls(*args, **kwargs)

File "/opt/conda/lib/python3.10/site-packages/jupyter_console/ptshell.py", line 352, in init

self.init_kernel_info()

File "/opt/conda/lib/python3.10/site-packages/jupyter_console/ptshell.py", line 437, in init_kernel_info

raise RuntimeError("Kernel didn't respond to kernel_info_request") from e

RuntimeError: Kernel didn't respond to kernel_info_request

[EugeneLoy]

Hi.
At a glance, it looks like a problem with Coq installation\availability.
Are you able to run coqidetop.opt --version? What is the output?

[nthiery]

$ coqidetop.opt --version
Fatal error: exception Not_found
$ coqidetop.opt 
Fatal error: exception Not_found

[nthiery]

Ah, but digging further, the above error occur only when running within our
JupyterHub; not on my machine:

(coq) ➜  sage git:(master) ✗ coqidetop.opt --version                   
The Coq Proof Assistant, version 8.12.0 (July 2020)
compiled on Jul 25 2020 10:36:41 with OCaml 4.06.1
(coq) ➜  sage git:(master) ✗ coqidetop.opt          
Fatal error: ideslave communication channels not set.

And indeed the coq kernel seems to work fine there.

Could this be because running within a docker container? Does the
kernel need to do, e.g., particular system calls?

I'll now try on a local docker container.

[EugeneLoy]

Ok, it looks like coq ide top is somehow broken in your installation.

For context, coqidetop.opt (previously coqidetop) is the utility/interface that is used by Coq IDE (and coq_jupyter) to evaluate Coq code.

Unfortunately, I can't suggest much based on this error message. My guess is that there is some sort of dependency (of coqidetop.opt) that is not present. This might be a packaging issue.

I would try installing different version of coq package or maybe install coq through different package manager altogether.
Anyway, the goal is to make coqidetop.opt --version not crash.

In case this helps, here are mamba packages that got installed on my machine after installing coq-jupyter using mamba:

mamba list
# packages in environment at /root/mambaforge:
#
# Name                    Version                   Build  Channel
_libgcc_mutex             0.1                 conda_forge    conda-forge
_openmp_mutex             4.5                       2_gnu    conda-forge
asttokens                 2.4.0              pyhd8ed1ab_0    conda-forge
backcall                  0.2.0              pyh9f0ad1d_0    conda-forge
backports                 1.0                pyhd8ed1ab_3    conda-forge
backports.functools_lru_cache 1.6.5              pyhd8ed1ab_0    conda-forge
binutils_impl_linux-64    2.40                 hf600244_0    conda-forge
binutils_linux-64         2.40                 hbdbef99_1    conda-forge
boltons                   23.0.0             pyhd8ed1ab_0    conda-forge
brotli-python             1.1.0           py310hc6cd4ac_0    conda-forge
bzip2                     1.0.8                h7f98852_4    conda-forge
c-ares                    1.19.1               hd590300_0    conda-forge
ca-certificates           2023.7.22            hbcca054_0    conda-forge
certifi                   2023.7.22          pyhd8ed1ab_0    conda-forge
cffi                      1.15.1          py310h255011f_3    conda-forge
charset-normalizer        3.2.0              pyhd8ed1ab_0    conda-forge
colorama                  0.4.6              pyhd8ed1ab_0    conda-forge
comm                      0.1.4              pyhd8ed1ab_0    conda-forge
conda                     23.3.1          py310hff52083_0    conda-forge
conda-libmamba-solver     23.3.0             pyhd8ed1ab_0    conda-forge
conda-package-handling    2.2.0              pyh38be061_0    conda-forge
conda-package-streaming   0.9.0              pyhd8ed1ab_0    conda-forge
coq                       8.12.0                        0    conda-forge
coq-jupyter               1.6.0           py310hff52083_2    conda-forge
cryptography              41.0.3          py310h75e40e8_0    conda-forge
debugpy                   1.8.0           py310hc6cd4ac_1    conda-forge
decorator                 5.1.1              pyhd8ed1ab_0    conda-forge
exceptiongroup            1.1.3              pyhd8ed1ab_0    conda-forge
executing                 1.2.0              pyhd8ed1ab_0    conda-forge
fmt                       9.1.0                h924138e_0    conda-forge
future                    0.18.3             pyhd8ed1ab_0    conda-forge
gcc_impl_linux-64         13.1.0               hc4be1a9_0    conda-forge
gcc_linux-64              13.1.0               hd2d1137_1    conda-forge
icu                       73.2                 h59595ed_0    conda-forge
idna                      3.4                pyhd8ed1ab_0    conda-forge
importlib-metadata        6.8.0              pyha770c72_0    conda-forge
importlib_metadata        6.8.0                hd8ed1ab_0    conda-forge
ipykernel                 6.25.2             pyh2140261_0    conda-forge
ipython                   8.16.1             pyh0d859eb_0    conda-forge
jedi                      0.19.1             pyhd8ed1ab_0    conda-forge
jsonpatch                 1.32               pyhd8ed1ab_0    conda-forge
jsonpointer               2.0                        py_0    conda-forge
jupyter-console           6.6.3                    pypi_0    pypi
jupyter_client            8.3.1              pyhd8ed1ab_0    conda-forge
jupyter_core              5.3.2           py310hff52083_0    conda-forge
kernel-headers_linux-64   2.6.32              he073ed8_16    conda-forge
keyutils                  1.6.1                h166bdaf_0    conda-forge
krb5                      1.21.2               h659d440_0    conda-forge
ld_impl_linux-64          2.40                 h41732ed_0    conda-forge
libarchive                3.6.2                h039dbb9_1    conda-forge
libcurl                   8.2.1                hca28451_0    conda-forge
libedit                   3.1.20191231         he28a2e2_2    conda-forge
libev                     4.33                 h516909a_1    conda-forge
libffi                    3.4.2                h7f98852_5    conda-forge
libgcc-devel_linux-64     13.1.0               he3cc6c4_0    conda-forge
libgcc-ng                 13.1.0               he5830b7_0    conda-forge
libgomp                   13.1.0               he5830b7_0    conda-forge
libiconv                  1.17                 h166bdaf_0    conda-forge
libmamba                  1.4.2                hcea66bb_0    conda-forge
libmambapy                1.4.2           py310h1428755_0    conda-forge
libnghttp2                1.52.0               h61bc06f_0    conda-forge
libnsl                    2.0.0                h7f98852_0    conda-forge
libsanitizer              13.1.0               hfd8a6a1_0    conda-forge
libsodium                 1.0.18               h36c2ea0_1    conda-forge
libsolv                   0.7.24               hfc55251_3    conda-forge
libsqlite                 3.43.0               h2797004_0    conda-forge
libssh2                   1.11.0               h0841786_0    conda-forge
libstdcxx-ng              13.1.0               hfd8a6a1_0    conda-forge
libuuid                   2.38.1               h0b41bf4_0    conda-forge
libxml2                   2.11.5               h232c23b_1    conda-forge
libzlib                   1.2.13               hd590300_5    conda-forge
lz4-c                     1.9.4                hcb278e6_0    conda-forge
lzo                       2.10              h516909a_1000    conda-forge
mamba                     1.4.2           py310h51d5547_0    conda-forge
matplotlib-inline         0.1.6              pyhd8ed1ab_0    conda-forge
ncurses                   6.4                  hcb278e6_0    conda-forge
nest-asyncio              1.5.6              pyhd8ed1ab_0    conda-forge
ocaml                     4.06.1            h14c3975_1007    conda-forge
ocaml-findlib             1.8.1                         0    conda-forge
ocaml-num                 1.2                           0    conda-forge
openssl                   3.1.3                hd590300_0    conda-forge
packaging                 23.1               pyhd8ed1ab_0    conda-forge
parso                     0.8.3              pyhd8ed1ab_0    conda-forge
pexpect                   4.8.0              pyh1a96a4e_2    conda-forge
pickleshare               0.7.5                   py_1003    conda-forge
pip                       23.2.1             pyhd8ed1ab_0    conda-forge
platformdirs              3.11.0             pyhd8ed1ab_0    conda-forge
pluggy                    1.3.0              pyhd8ed1ab_0    conda-forge
prompt-toolkit            3.0.39             pyha770c72_0    conda-forge
prompt_toolkit            3.0.39               hd8ed1ab_0    conda-forge
psutil                    5.9.5           py310h2372a71_1    conda-forge
ptyprocess                0.7.0              pyhd3deb0d_0    conda-forge
pure_eval                 0.2.2              pyhd8ed1ab_0    conda-forge
pybind11-abi              4                    hd8ed1ab_3    conda-forge
pycosat                   0.6.4           py310h5764c6d_1    conda-forge
pycparser                 2.21               pyhd8ed1ab_0    conda-forge
pygments                  2.16.1             pyhd8ed1ab_0    conda-forge
pyopenssl                 23.2.0             pyhd8ed1ab_1    conda-forge
pysocks                   1.7.1              pyha2e5f31_6    conda-forge
python                    3.10.12         hd12c33a_0_cpython    conda-forge
python-dateutil           2.8.2              pyhd8ed1ab_0    conda-forge
python_abi                3.10                    3_cp310    conda-forge
pyzmq                     25.1.1          py310h5bbb5d0_1    conda-forge
readline                  8.2                  h8228510_1    conda-forge
reproc                    14.2.4               h0b41bf4_0    conda-forge
reproc-cpp                14.2.4               hcb278e6_0    conda-forge
requests                  2.31.0             pyhd8ed1ab_0    conda-forge
ruamel.yaml               0.17.32         py310h2372a71_0    conda-forge
ruamel.yaml.clib          0.2.7           py310h1fa729e_1    conda-forge
setuptools                68.1.2             pyhd8ed1ab_0    conda-forge
six                       1.16.0             pyh6c4a22f_0    conda-forge
stack_data                0.6.2              pyhd8ed1ab_0    conda-forge
sysroot_linux-64          2.12                he073ed8_16    conda-forge
tk                        8.6.12               h27826a3_0    conda-forge
toolz                     0.12.0             pyhd8ed1ab_0    conda-forge
tornado                   6.3.3           py310h2372a71_1    conda-forge
tqdm                      4.66.1             pyhd8ed1ab_0    conda-forge
traitlets                 5.11.2             pyhd8ed1ab_0    conda-forge
typing-extensions         4.8.0                hd8ed1ab_0    conda-forge
typing_extensions         4.8.0              pyha770c72_0    conda-forge
tzdata                    2023c                h71feb2d_0    conda-forge
urllib3                   2.0.4              pyhd8ed1ab_0    conda-forge
wcwidth                   0.2.8              pyhd8ed1ab_0    conda-forge
wheel                     0.41.2             pyhd8ed1ab_0    conda-forge
xz                        5.2.6                h166bdaf_0    conda-forge
yaml-cpp                  0.7.0                h27087fc_2    conda-forge
zeromq                    4.3.4                h9c3ff4c_1    conda-forge
zipp                      3.17.0             pyhd8ed1ab_0    conda-forge
zstandard                 0.19.0          py310h5764c6d_0    conda-forge
zstd                      1.5.5                hfc55251_0    conda-forge
(

Machine OS info:

cat /etc/os-release
PRETTY_NAME="Ubuntu 22.04.2 LTS"
NAME="Ubuntu"
VERSION_ID="22.04"
VERSION="22.04.2 LTS (Jammy Jellyfish)"
VERSION_CODENAME=jammy
ID=ubuntu
ID_LIKE=debian
HOME_URL="https://www.ubuntu.com/"
SUPPORT_URL="https://help.ubuntu.com/"
BUG_REPORT_URL="https://bugs.launchpad.net/ubuntu/"
PRIVACY_POLICY_URL="https://www.ubuntu.com/legal/terms-and-policies/privacy-policy"
UBUNTU_CODENAME=jammy

I can confirm that with this setup coq ide top works fine.

Also, is there any way I could reproduce your problem on my end? Maybe, cold look into this over weekend.

[EugeneLoy]

Could this be because running within a docker container? Does the kernel need to do, e.g., particular system calls?

No, nothing like that. I was able to run ci tests for kernel within Docker (based on coqorg/coq images).

[nthiery]

Hmm. Two suggestions to reproduce:

Directly with docker:

$ sudo docker run -ti --rm condaforge/mambaforge bash
...
(base) root@fa98a9c7dde8:/# mamba install coq-jupyter
...
(base) root@fa98a9c7dde8:/# coqidetop.opt 
Fatal error: exception Not_found

If you have an account on the Federation Education Recherche:
connect on our Jupyter (jupyterhub.ijclab.in2p3.fr), launch JupyterLab,
and run the mamba install as above from a terminal.

Thank you for the quick feedback! It would be nice to be able to make the coq
kernel available on our hub.

[Zimmi48]

Note that by installing Coq using conda, it's likely that you will be stuck on Coq 8.12 forever as the Coq package (and also the OCaml package) have been unmaintained there for many years. You should consider installing Coq with either opam, Nix, Snap, or even basing your Docker image on the official Coq Docker images. Actually, now that I think of it, even installing Coq using APT (if you are on Debian/Ubuntu) would give you a much more up-to-date (and less likely to be broken) version.

For reference, see:

• https://coq.inria.fr/download
• https://coq.inria.fr/opam-using.html
• https://snapcraft.io/coq-prover
• https://hub.docker.com/r/coqorg/coq
• https://repology.org/project/coq/versions

[nthiery]

Thanks @Zimmi48 for the feedback. At this stage, we are stuck in our JupyterHub
deployment with a single image for all software. It's convenient to use a single
package manager, and conda is a good fit given that all the rest of the stack
(~200 packages + dependencies) is packaged there. That being said, worst to worst,
we could use the debian package manager of the base image.