cocalc csi error

[haraldschilly]

this is the error I get when running this (the server command, slightly modified) in cocalc

$ /srv/conda/envs/notebook/bin/python /srv/conda/envs/notebook/bin/jupyter-notebook --log-level=DEBUG --port-retries=0 --no-browser --NotebookApp.iopub_data_rate_limit=2000000 --NotebookApp.iopub_msg_rate_limit=50 --NotebookApp.mathjax_url=/static/mathjax-2.7.4/MathJax.js --NotebookApp.base_url=/3b98b61c-ecc1-44aa-8dda-ee98827e7442/port/4141/ --ip=192.168.195.165 --port=4141 --NotebookApp.token= --NotebookApp.password= --NotebookApp.allow_remote_access=True

[I 12:47:30.178 NotebookApp] KernelRestarter: restarting kernel (4/5), new random ports
[D 12:47:30.180 NotebookApp] Starting kernel: ['/srv/conda/envs/notebook/bin/python', '-m', 'coq_jupyter', '-f', '/tmp/xdg-runtime-user/jupyter/kernel-79d5edc1-0059-40ec-8e99-a28bc5208918.json']
[D 12:47:30.185 NotebookApp] Connecting to: tcp://127.0.0.1:37393
^C[I 12:47:30.735 NotebookApp] interrupted
Serving notebooks from local directory: /home/user
1 active kernel
The Jupyter Notebook is running at:
http://192.168.195.165:4141/3b98b61c-ecc1-44aa-8dda-ee98827e7442/port/4141/
Shutdown this notebook server (y/[n])? Fatal error: exception Not_found
Fatal error: exception Not_found
[IPKernelApp] ERROR | CoqtopError has occured. Scheduling shutdown.
Traceback (most recent call last):
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/coq_jupyter/coqtop.py", line 57, in __init__
    raise CoqtopError("Failed to locate 'coqidetop' or 'coqtop' executables")
coq_jupyter.coqtop.CoqtopError: Failed to locate 'coqidetop' or 'coqtop' executables

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/coq_jupyter/kernel.py", line 59, in wrapper
    return function(self, *args, **kwargs)
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/coq_jupyter/kernel.py", line 99, in __init__
    self._coqtop = Coqtop(self, self.coqtop_args)
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/coq_jupyter/coqtop.py", line 85, in __init__
    raise_with_traceback(CoqtopError("Cause: {}".format(repr(e))))
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/future/utils/__init__.py", line 446, in raise_with_traceback
    raise exc.with_traceback(traceback)
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/coq_jupyter/coqtop.py", line 57, in __init__
    raise CoqtopError("Failed to locate 'coqidetop' or 'coqtop' executables")
coq_jupyter.coqtop.CoqtopError: Cause: CoqtopError("Failed to locate 'coqidetop' or 'coqtop' executables")
Traceback (most recent call last):
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/coq_jupyter/coqtop.py", line 57, in __init__
    raise CoqtopError("Failed to locate 'coqidetop' or 'coqtop' executables")
coq_jupyter.coqtop.CoqtopError: Failed to locate 'coqidetop' or 'coqtop' executables

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/srv/conda/envs/notebook/lib/python3.7/runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  File "/srv/conda/envs/notebook/lib/python3.7/runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/coq_jupyter/__main__.py", line 5, in <module>
    IPKernelApp.launch_instance(kernel_class=CoqKernel, args=argv)
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/traitlets/config/application.py", line 657, in launch_instance
    app.initialize(argv)
  File "</srv/conda/envs/notebook/lib/python3.7/site-packages/decorator.py:decorator-gen-124>", line 2, in initialize
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/traitlets/config/application.py", line 87, in catch_config_error
    return method(app, *args, **kwargs)
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/ipykernel/kernelapp.py", line 484, in initialize
    self.init_kernel()
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/ipykernel/kernelapp.py", line 389, in init_kernel
    user_ns=self.user_ns,
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/traitlets/config/configurable.py", line 412, in instance
    inst = cls(*args, **kwargs)
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/coq_jupyter/kernel.py", line 59, in wrapper
    return function(self, *args, **kwargs)
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/coq_jupyter/kernel.py", line 99, in __init__
    self._coqtop = Coqtop(self, self.coqtop_args)
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/coq_jupyter/coqtop.py", line 85, in __init__
    raise_with_traceback(CoqtopError("Cause: {}".format(repr(e))))
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/future/utils/__init__.py", line 446, in raise_with_traceback
    raise exc.with_traceback(traceback)
  File "/srv/conda/envs/notebook/lib/python3.7/site-packages/coq_jupyter/coqtop.py", line 57, in __init__
    raise CoqtopError("Failed to locate 'coqidetop' or 'coqtop' executables")
coq_jupyter.coqtop.CoqtopError: Cause: CoqtopError("Failed to locate 'coqidetop' or 'coqtop' executables")
[W 12:47:33.188 NotebookApp] KernelRestarter: restart failed
[W 12:47:33.188 NotebookApp] Kernel 79d5edc1-0059-40ec-8e99-a28bc5208918 died, removing from map.
^C[C 12:47:33.269 NotebookApp] received signal 2, stopping
[I 12:47:33.270 NotebookApp] Shutting down 0 kernels

---

$ echo $PATH
/cocalc/bin:/cocalc/src/smc-project/bin:/home/user/bin:/home/user/.local/bin:/home/user/.local/bin:/home/user/.local/bin:/srv/conda/envs/notebook/bin:/srv/conda/bin:/srv/npm/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin

[haraldschilly]

So, somehow, it's a matter for fixing a path or how the binaries are searched. With other custom environments (repo2docker builds) I've not seen such a problem before. Hmm …

~$ find /srv -name coqtop
/srv/conda/envs/notebook/bin/coqtop
~$ find /srv -name coqidetop
/srv/conda/envs/notebook/bin/coqidetop

[Zimmi48]

Thanks for the feedback. The weird thing is that this works fine with MyBinder. I don't know what the difference could be that would explain this. @EugeneLoy (coq_jupyter author) or @slel (feedstocks author): maybe you have an idea?

[haraldschilly]

Well, there are certainly many differences. There must be something going on with mybinder regarding how it does start the environment. In particular, there is an anaconda env called "notebook". Is this always defined? Is MyBinder starting this environment explicitly? If someone can tell me more details or just point me to the code, I'm sure I can figure this out. There are also some environment variables, which must be relevant. I don't know if anaconda sets them (I assume it does).

[EugeneLoy]

@Zimmi48

maybe you have an idea?

I don't see any obvious problems yet.

@haraldschilly

What conda environment are you using to run jupyter server? Also, are you able to run\what is the output of the coqtop --version and coqidetop --version under that environment?

[haraldschilly]

well, I don't know how to get this to work at all. probably my main problem is that I don't know what's going on and therefore I lack insight into debugging this. What are these tools doing?

My alternative approach is to just get this to work in cocalc. As far as I can tell it installs fine, but the jupyter server's attempts to run the kernel crash with

Traceback (most recent call last):
  File "/ext/anaconda-2019.03/lib/python3.7/runpy.py", line 183, in _run_module_as_main
    mod_name, mod_spec, code = _get_module_details(mod_name, _Error)
  File "/ext/anaconda-2019.03/lib/python3.7/runpy.py", line 142, in _get_module_details
    return _get_module_details(pkg_main_name, error)
  File "/ext/anaconda-2019.03/lib/python3.7/runpy.py", line 109, in _get_module_details
    __import__(pkg_name)
  File "/ext/anaconda-2019.03/lib/python3.7/site-packages/coq_jupyter/__init__.py", line 3, in <module>
    from .kernel import __version__
  File "/ext/anaconda-2019.03/lib/python3.7/site-packages/coq_jupyter/kernel.py", line 7, in <module>
    from traitlets import Unicode
  File "/ext/anaconda-2019.03/lib/python3.7/site-packages/traitlets/__init__.py", line 1, in <module>
    from .traitlets import *
  File "/ext/anaconda-2019.03/lib/python3.7/site-packages/traitlets/traitlets.py", line 57, in <module>
    import six
  File "/ext/anaconda-2019.03/lib/python3.7/site-packages/six.py", line 631, in <module>
    import struct
  File "/ext/anaconda-2019.03/lib/python3.7/struct.py", line 13, in <module>
    from _struct import *
ModuleNotFoundError: No module named '_struct'

---

(base) ~$ coqtop --version; coqidetop --version
The Coq Proof Assistant, version 8.11.0 (February 2020)
compiled on Feb 2 2020 16:19:59 with OCaml 4.06.1
The Coq Proof Assistant, version 8.11.0 (February 2020)
compiled on Feb 2 2020 16:19:59 with OCaml 4.06.1

What environment variables or other settings are relevant? What are the dependencies?