Aloha!
According to Github, this project is partially written in the formal theorem prover language Coq.
https://en.wikipedia.org/wiki/Coq
The files in question are:
- shift_reg/piso.v
- shift_reg/sipo.v
They are clearly not Coq-files, but nice and normal Verilog files. The problem is that Github has a parser called Linguist
https://github.com/github/linguist
There has been a number of issues opened for Linguist related to misinterpreting Verilog as Coq. But so far it has not been fixed. A solution to this is to add a .gitattribute file to the repo. The file can simply contain one line:
*.v linguist-language=Verilog
There is a copy in my aes core repo you can copy:
https://github.com/secworks/aes/blob/master/.gitattributes
Aloha!
According to Github, this project is partially written in the formal theorem prover language Coq.
https://en.wikipedia.org/wiki/Coq
The files in question are:
They are clearly not Coq-files, but nice and normal Verilog files. The problem is that Github has a parser called Linguist
https://github.com/github/linguist
There has been a number of issues opened for Linguist related to misinterpreting Verilog as Coq. But so far it has not been fixed. A solution to this is to add a .gitattribute file to the repo. The file can simply contain one line:
*.v linguist-language=Verilog
There is a copy in my aes core repo you can copy:
https://github.com/secworks/aes/blob/master/.gitattributes