Check Line Length error

[maxsnew]

This is what I get when I ./check-line-lengths.sh locally.

./check-line-lengths.sh: line 5: shopt: globstar: invalid shell option name
Traceback (most recent call last):
  File "<string>", line 3, in <module>
ModuleNotFoundError: No module named 'wcwidth'
Traceback (most recent call last):
  File "<string>", line 3, in <module>
ModuleNotFoundError: No module named 'wcwidth'
Traceback (most recent call last):
  File "<string>", line 3, in <module>
ModuleNotFoundError: No module named 'wcwidth'
Traceback (most recent call last):
  File "<string>", line 3, in <module>
ModuleNotFoundError: No module named 'wcwidth'

Seems to be two issues:

1. one is that Mac OS ships with an old version of bash that doesn't support shopt -s globstar nullglob.
2. the python module errors I don't understand because I already did pip install wcwidth.

[stschaef]

I just upgraded from bash 3 to bash 5 and it fixed the first point. I think this fix is suitable, but if you don't want to upgrade bash then I can take a look at the script

The second point can be fixed via virtual environment. I can try to automate that in the script

[hejohns]

@stschaef We could replace the shopt globstar with find? For 1.

[stschaef]

Just pushed the fix for the venv (accidentally directly to main, cause I thought I was pushing onto my fork 🙃)

[hejohns]

edit: unclear comment. I already have wcwidth, but I still get

hejohns@agda:~/cubical-categorical-logic$ make
find . -name "*.agda" ! -path './Everything.agda' | sed -e 's#/#.#g' -e 's/^\.*//' -e 's/.agda$//' -e 's/^/import /' | LC_ALL=C sort > Everything.agda
fix-whitespace --check
agda Everything.agda
Checking Everything (/home/hejohns/cubical-categorical-logic/Everything.agda).
 Checking Cubical.Categories.Profunctor.AdjointComprehension (/home/hejohns/cubical-categorical-logic/Cubical/Categories/Profunctor/AdjointComprehension.agda).
bash check-line-lengths.sh
Virtual environment does not exist. Creating one now...
The virtual environment was not created successfully because ensurepip is not
available.  On Debian/Ubuntu systems, you need to install the python3-venv
package using the following command.

    apt install python3.11-venv

You may need to use sudo with that command.  After installing the python3-venv
package, recreate your virtual environment.

Failing command: /home/hejohns/cubical-categorical-logic/env/bin/python3

Failed to create virtual environment.
make: *** [Makefile:32: check-line-lengths] Error 1

[hejohns]

also

diff --git a/Makefile b/Makefile
index 3174ed2..66dfa6e 100644                                    
--- a/Makefile                                                                          
+++ b/Makefile
@@ -3,7 +3,7 @@ FIX_WHITESPACE = fix-whitespace                                         

 # Finds all .agda files in the current directory and subdirectories                    
 FIND_AGDA_FILES = find . -name "*.agda"        
-AGDA_FILES = $(shell $(FIND_AGDA_FILES))                                              
+export AGDA_FILES = $(shell $(FIND_AGDA_FILES))                    

 # The targets are the .agdai files corresponding to the .agda files
 AGDAI_FILES = $(AGDA_FILES:.agda=.agdai)
diff --git a/check-line-lengths.sh b/check-line-lengths.sh  
index 30604e5..8427439 100755                                          
--- a/check-line-lengths.sh 
+++ b/check-line-lengths.sh                        
@@ -2,8 +2,7 @@
 # originally written by Steven Schaefer <stschaef>

 error=0                  
-shopt -s globstar nullglob       
-for file in **/*.agda; do
+for file in ${AGDA_FILES}; do                                   
   python3 -c '                         
 import sys                                           
 from wcwidth import wcswidth

[stschaef]

edit: unclear comment. I already have wcwidth, but I still get

hejohns@agda:~/cubical-categorical-logic$ make
find . -name "*.agda" ! -path './Everything.agda' | sed -e 's#/#.#g' -e 's/^\.*//' -e 's/.agda$//' -e 's/^/import /' | LC_ALL=C sort > Everything.agda
fix-whitespace --check
agda Everything.agda
Checking Everything (/home/hejohns/cubical-categorical-logic/Everything.agda).
 Checking Cubical.Categories.Profunctor.AdjointComprehension (/home/hejohns/cubical-categorical-logic/Cubical/Categories/Profunctor/AdjointComprehension.agda).
bash check-line-lengths.sh
Virtual environment does not exist. Creating one now...
The virtual environment was not created successfully because ensurepip is not
available.  On Debian/Ubuntu systems, you need to install the python3-venv
package using the following command.

    apt install python3.11-venv

You may need to use sudo with that command.  After installing the python3-venv
package, recreate your virtual environment.

Failing command: /home/hejohns/cubical-categorical-logic/env/bin/python3

Failed to create virtual environment.
make: *** [Makefile:32: check-line-lengths] Error 1

any luck after installing the package for virtual environments?

[stschaef]

also

diff --git a/Makefile b/Makefile
index 3174ed2..66dfa6e 100644                                    
--- a/Makefile                                                                          
+++ b/Makefile
@@ -3,7 +3,7 @@ FIX_WHITESPACE = fix-whitespace                                         

 # Finds all .agda files in the current directory and subdirectories                    
 FIND_AGDA_FILES = find . -name "*.agda"        
-AGDA_FILES = $(shell $(FIND_AGDA_FILES))                                              
+export AGDA_FILES = $(shell $(FIND_AGDA_FILES))                    

 # The targets are the .agdai files corresponding to the .agda files
 AGDAI_FILES = $(AGDA_FILES:.agda=.agdai)
diff --git a/check-line-lengths.sh b/check-line-lengths.sh  
index 30604e5..8427439 100755                                          
--- a/check-line-lengths.sh 
+++ b/check-line-lengths.sh                        
@@ -2,8 +2,7 @@
 # originally written by Steven Schaefer <stschaef>

 error=0                  
-shopt -s globstar nullglob       
-for file in **/*.agda; do
+for file in ${AGDA_FILES}; do                                   
   python3 -c '                         
 import sys                                           
 from wcwidth import wcswidth

Oh geez, I accidentally pushed way too much

[hejohns]

Sorry my original comment was that this makes you use venvs, even when you already have wcwidth. But that's fine actually. Although I don't know what the actual problem Max had was, so it's not clear to me venvs solve it.

After installing the package there's some issue where env/bin/activate doesn't exist that I'm looking at.

[stschaef]

also

diff --git a/Makefile b/Makefile
index 3174ed2..66dfa6e 100644                                    
--- a/Makefile                                                                          
+++ b/Makefile
@@ -3,7 +3,7 @@ FIX_WHITESPACE = fix-whitespace                                         

 # Finds all .agda files in the current directory and subdirectories                    
 FIND_AGDA_FILES = find . -name "*.agda"        
-AGDA_FILES = $(shell $(FIND_AGDA_FILES))                                              
+export AGDA_FILES = $(shell $(FIND_AGDA_FILES))                    

 # The targets are the .agdai files corresponding to the .agda files
 AGDAI_FILES = $(AGDA_FILES:.agda=.agdai)
diff --git a/check-line-lengths.sh b/check-line-lengths.sh  
index 30604e5..8427439 100755                                          
--- a/check-line-lengths.sh 
+++ b/check-line-lengths.sh                        
@@ -2,8 +2,7 @@
 # originally written by Steven Schaefer <stschaef>

 error=0                  
-shopt -s globstar nullglob       
-for file in **/*.agda; do
+for file in ${AGDA_FILES}; do                                   
   python3 -c '                         
 import sys                                           
 from wcwidth import wcswidth

Oh geez, I accidentally pushed way too much

I'm going to revert these rn btw

[stschaef]

Sorry my original comment was that this makes you use venvs, even when you already have wcwidth. But that's fine actually. Although I don't know what the actual problem Max had was, so it's not clear to me venvs solve it.

After installing the package there's some issue where env/bin/activate doesn't exist that I'm looking at.

there are situations where you may have wcwidth in a particular python env, say your global one, but this script may not be accessing it

for instance, bc its managed by brew I cannot pip3 install wcwidth, and thus I can't globally install wcwidth to run this script

[hejohns]

Oh okay. There's no serious issue with the script afaik. It doesn't like when env already exists for other reasons, but that's fine.

[stschaef]

Okay sounds good.

Sorry for me being a git dweeb occasionally shines. I've reverted the things I've overpushed, and then I'll PULL REQUEST in the script change

[hejohns]

It looks like you've only reverted one commit ("adjoint comp", daf56f4d9b21bdc0699cee885cde4857c9b9d97c). Just in case you had meant to do something else.

[hejohns]

Oh I see you did revert everything in one commit.

[stschaef]

99

geez sorry for how hectic this was

[hejohns]

You're good. I kept commenting before I should've...

[maxsnew]

I rebased and force pushed to fix the history so make sure to pull