Re: [PATCH v2 04/22] verification/dot2k: Make it possible to invoke dot2k without installation

[Gabriele Monaco]

On Fri, 2025-04-11 at 16:04 +0200, Nam Cao wrote:
> On Fri, Apr 11, 2025 at 11:23:25AM +0200, Gabriele Monaco wrote:
> > On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> > > Without installation, dot2k doesn't work:
> > > 
> > > namcao@yellow:~/linux/tools/verification$ python3 ./dot2/dot2k
> > > Traceback (most recent call last):
> > >   File "/home/namcao/linux/tools/verification/./dot2/dot2k", line
> > > 12,
> > > in <module>
> > >     from dot2.dot2k import dot2k
> > > ModuleNotFoundError: No module named 'dot2'
> > > 
> > > Installing dot2k to the system is not always desirable. Sometimes
> > > it
> > > is not
> > > even possible (e.g. no root permission).
> > > 
> > > Restructure the files to make it work without installing.
> > > 
> > > Signed-off-by: Nam Cao <namcao@xxxxxxxxxxxxx>
> > 
> > Mmh, the workflow
> > 
> > pushd tools/verification
> > ...
> > popd
> > 
> > 
> > has always been working in my case, but probably that's because I
> > have
> > PYTHONPATH="." , not sure how much of a good practice that is.
> 
> Ahh, PYTHONPATH is the trick. But that shouldn't be required. The
> scripts
> should work out of the box without any environment setup.
> 
> > Anyway, since you're already moving things around in 9/22
> > ("verification/dot2k: Prepare the frontend for LTL inclusion"),
> > does it
> > make sense to keep the commits separated? Or you could directly
> > move to
> > rvgen here and just add the ltl related changes in the later
> > commit.
> 
> Yes, it makes sense to move them to rvgen here.
> 
> > Also, after your changes on my system, I can run the script from
> > the
> > kernel directory too, which is much better than having to cd to
> > tools/verification .
> > If that's something portable, I'd change the default definition of
> > monitor_templates_dir and allow the user to run the script only
> > from
> > the kernel root.
> > 
> > What do you think?
> 
> I actually prefer running the script from tools/verification. We can
> allow
> user to run from anywhere, with something like:
> 
>  class dot2k(Monitor, Dot2c):
> -    monitor_templates_dir = "rvgen/templates/dot2k"
> +    monitor_templates_dir = os.path.join(os.path.dirname(__file__),
> "../../rvgen/templates/dot2k")

That looks like a good option!

Thanks,
Gabriele