How to specify a path for linting Z3 in Python with pylint

[benbrastmckie]

I'm using pylint which works great unless I want to import from z3 as follows:

from z3 import *

Pylint seems unable to access the z3 libraries and so adds lots of error messages like Undefined variable 'Bools' etc. The libraries are there, and so the code runs fine. I'm just trying to avoid all the errors.

I don't get these error messages if I specify everything I'm importing as follows:

from z3 import Bools, Solver, unsat, Not, Or, And, BitVec, simplify, BitVecVal, BitVecs, solve

But I want to be able to use from z3 import * since this is standard practice.

I am wondering if there is a way to tell none-ls or pylint where to find z3 and if that will avoid the errors. Very much appreciate any pointers! It would be a shame to have to turn off linting when working with z3.

[mochaaP]

This won't work because pylint (and many tools) is designed that way, which does not support star imports. You could do this, though:

from z3 import *
from typing import TYPE_CHECKING

if TYPE_CHECKING:
	from z3 import Bools, Solver, unsat, Not, Or, And, BitVec, simplify, BitVecVal, BitVecs, solve

[benbrastmckie]

That's great to know. I'll specify the libraries if that is best practice for use with a linter. However, in doing so, it still seems like pylint can't find z3, writing Unable to import 'z3' after 'from z3 import (' on the first line below:

from z3 import (
    BoolSort,
    BitVecSort,
    Function,
    simplify,
    Solver,
    BitVec,
    Not,
    Exists,
    And,
    Implies,
    ForAll,
    sat,
)

Thanks for your suggestions!

[mochaaP]

Hmm, that's weird. Are you in a venv?

[benbrastmckie]

I'm using NixOS... might that explain it? I have pylint and z3 in my path.