| Message ID | caa6a7668f958c68fc7b8a40256e3edf3f11ae99.1744355018.git.namcao@linutronix.de (mailing list archive) |
|---|---|
| State | Superseded |
| Headers | show |
| Series | RV: Linear temporal logic monitors for RT application | expand |
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@linutronix.de> 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. 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. 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? Thanks, Gabriele > --- > tools/verification/dot2/Makefile | 6 +++--- > tools/verification/dot2/{ => dot2}/automata.py | 0 > tools/verification/dot2/{ => dot2}/dot2c.py | 0 > tools/verification/dot2/{ => dot2}/dot2k.py | 0 > 4 files changed, 3 insertions(+), 3 deletions(-) > rename tools/verification/dot2/{ => dot2}/automata.py (100%) > rename tools/verification/dot2/{ => dot2}/dot2c.py (100%) > rename tools/verification/dot2/{ => dot2}/dot2k.py (100%) > > diff --git a/tools/verification/dot2/Makefile > b/tools/verification/dot2/Makefile > index 021beb07a521..7a2ec30014b0 100644 > --- a/tools/verification/dot2/Makefile > +++ b/tools/verification/dot2/Makefile > @@ -16,10 +16,10 @@ clean: > > .PHONY: install > install: > - $(INSTALL) automata.py -D -m 644 > $(DESTDIR)$(PYLIB)/dot2/automata.py > - $(INSTALL) dot2c.py -D -m 644 > $(DESTDIR)$(PYLIB)/dot2/dot2c.py > + $(INSTALL) dot2/automata.py -D -m 644 > $(DESTDIR)$(PYLIB)/dot2/automata.py > + $(INSTALL) dot2/dot2c.py -D -m 644 > $(DESTDIR)$(PYLIB)/dot2/dot2c.py > $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ > - $(INSTALL) dot2k.py -D -m 644 > $(DESTDIR)$(PYLIB)/dot2/dot2k.py > + $(INSTALL) dot2/dot2k.py -D -m 644 > $(DESTDIR)$(PYLIB)/dot2/dot2k.py > $(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/ > > mkdir -p ${miscdir}/ > diff --git a/tools/verification/dot2/automata.py > b/tools/verification/dot2/dot2/automata.py > similarity index 100% > rename from tools/verification/dot2/automata.py > rename to tools/verification/dot2/dot2/automata.py > diff --git a/tools/verification/dot2/dot2c.py > b/tools/verification/dot2/dot2/dot2c.py > similarity index 100% > rename from tools/verification/dot2/dot2c.py > rename to tools/verification/dot2/dot2/dot2c.py > diff --git a/tools/verification/dot2/dot2k.py > b/tools/verification/dot2/dot2/dot2k.py > similarity index 100% > rename from tools/verification/dot2/dot2k.py > rename to tools/verification/dot2/dot2/dot2k.py
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@linutronix.de> > > 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") Best regards, Nam
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@linutronix.de> > > > > 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
diff --git a/tools/verification/dot2/Makefile b/tools/verification/dot2/Makefile index 021beb07a521..7a2ec30014b0 100644 --- a/tools/verification/dot2/Makefile +++ b/tools/verification/dot2/Makefile @@ -16,10 +16,10 @@ clean: .PHONY: install install: - $(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py - $(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py + $(INSTALL) dot2/automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py + $(INSTALL) dot2/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ - $(INSTALL) dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py + $(INSTALL) dot2/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py $(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/ mkdir -p ${miscdir}/ diff --git a/tools/verification/dot2/automata.py b/tools/verification/dot2/dot2/automata.py similarity index 100% rename from tools/verification/dot2/automata.py rename to tools/verification/dot2/dot2/automata.py diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/dot2/dot2/dot2c.py similarity index 100% rename from tools/verification/dot2/dot2c.py rename to tools/verification/dot2/dot2/dot2c.py diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/dot2/dot2/dot2k.py similarity index 100% rename from tools/verification/dot2/dot2k.py rename to tools/verification/dot2/dot2/dot2k.py
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@linutronix.de> --- tools/verification/dot2/Makefile | 6 +++--- tools/verification/dot2/{ => dot2}/automata.py | 0 tools/verification/dot2/{ => dot2}/dot2c.py | 0 tools/verification/dot2/{ => dot2}/dot2k.py | 0 4 files changed, 3 insertions(+), 3 deletions(-) rename tools/verification/dot2/{ => dot2}/automata.py (100%) rename tools/verification/dot2/{ => dot2}/dot2c.py (100%) rename tools/verification/dot2/{ => dot2}/dot2k.py (100%)