COQ - cannot import name 'autodie' from 'std2.sys'

[pupbrained]

Plugin affected: coq-nvim Nixpkgs channel: unstable Home-manager version: unstable

Description

As of the past week or two, coq-nvim has been completely broken for me with the error:

cannot import name 'autodie' from 'std2.sys' (/Users/(REDACTED)/.local/share/nvim/coqrt/lib/python3.10/site-packages/std2/sys.py)                                                                                                             

Please update dependencies using :COQdeps                                                                                                                                                                                                   
-                                                                                                                                                                                                                                           
-                                                                                                                                                                                                                                           
Dependencies will be installed privately inside `/Users/(REDACTED)/.cache/coq_nvim/vars`                                                                                                                                                      
`rm -rf sgchbg01mdkpxkqyzqrvbik823s92fz0-vimplugin-coq_nvim-2023-05-28` will cleanly remove everything

Attempting to run :COQdeps like said in the error message returns:

Traceback (most recent call last):
  File "/nix/store/xmxc0xc03fqq8b19sxfxwyd8k71kaz5m-python3-3.10.11/lib/python3.10/runpy.py", line 196, in _run_module_as_main
    return _run_code(code, main_globals, None,
  File "/nix/store/xmxc0xc03fqq8b19sxfxwyd8k71kaz5m-python3-3.10.11/lib/python3.10/runpy.py", line 86, in _run_code
    exec(code, run_globals)
  File "/nix/store/sgchbg01mdkpxkqyzqrvbik823s92fz0-vimplugin-coq_nvim-2023-05-28/coq/__main__.py", line 85, in <module>
    assert not _IN_VENV
AssertionError

[Process exited 1]

Config

https://github.com/pupbrained/nix-config/blob/mac/pkgs/nixvim/default.nix

[GaetanLepage]

Hello ! Thanks for reporting this bug. When does the error actually appears ? When you run neovim or when completion is supposed to happen ? I was not able to reproduce the error.

For a few weeks now, the python dependencies of coq-nvim have been included in the nix package. Hence, you shouldn't have to run :COQdeps as the dependencies should already be available.

Please, make sure that your nixpkgs source is up to date.

[GaetanLepage]

Completely unrelated: You can simplify your keymap declaration by using mkMaps {silent = true;}. See an example in my config: https://github.com/GaetanLepage/dotfiles/blob/bbaf4ab590e3a50a39f1c859bb7255103dbac4d6/home/tui/neovim/keymappings.nix#L8

[pupbrained]

Hello ! Thanks for reporting this bug. When does the error actually appears ? When you run neovim or when completion is supposed to happen ? I was not able to reproduce the error.

The error occurs upon running neovim.

For a few weeks now, the python dependencies of coq-nvim have been included in the nix package. Hence, you shouldn't have to run :COQdeps as the dependencies should already be available.

I assume that this issue has something to do with this update, considering COQ has worked for me up until recently.

Please, make sure that your nixpkgs source is up to date.

I have made sure all of my sources are up to date. I have just now updated my flake again and rebuilt my configuration, and I'm encountering the same issue.

If it does make any difference, I have this same configuration on a different device running NixOS x86_64 and I do not have this issue. I only seem to have it with my MacBook running macOS aarch64 w/ nix-darwin.

[GaetanLepage]

If it does make any difference, I have this same configuration on a different device running NixOS x86_64 and I do not have this issue. I only seem to have it with my MacBook running macOS aarch64 w/ nix-darwin.

Very interesting. What is strange then, is that you don't experience any failure during the building process. Hence, the dependencies are installed correctly I guess. So maybe, it is a problem of the way COQ is looking for its dependencies on arm darwin.

Can you try the following ?

• Run nvim
• :checkhealth provider
• Locate the path of the executable for the Python 3 provider.
• From your terminal, execute this python binary and, in the REPL, try to import std2.

Then we will be able to see if the package has been installed at all.

[pupbrained]

No errors when importing. It seems that python is fine?

[GaetanLepage]

Hmmm, yes. Could you now try from std2.sys import autodie ?

[pupbrained]

Seems to import just fine... odd.

[pupbrained]

Ah, I think I've found the problem.

For some reason, the autodie function is instead named suicide on my machine.

After looking at std2's git repo I can see that the function was renamed a while back.

[GaetanLepage]

Oh nice catch. However, why isn't coq_nvim using the same version of std2 on both machines ? You suggest that you have an outdated version of std2 on your mac right ?

[pupbrained]

Oh nice catch. However, why isn't coq_nvim using the same version of std2 on both machines ? You suggest that you have an outdated version of std2 on your mac right ?

Yes, it was. After deleting .local/share/nvim/coqrt COQ began to work just like before. I'm still not sure why that was out of date, though?

[GaetanLepage]

Yes, it was. After deleting .local/share/nvim/coqrt COQ began to work just like before. I'm still not sure why that was out of date, though?

Indeed it makes sense. What happened is that you had a local copy of the coq python dependencies in your ~/.local/share/nvim which was being used instead of the one bundled in the derivation. Hence you had the bug. By deleting it you made coq use the right one. You should be done with dependency installation now !

I am closing the issue.