Skip to content

coqlint.sh is not found during make -j(CPU cores) command

Steps to reproduce

  1. Clone repository.
  2. Create a flake.nix that installs relevant packages.
  3. Create an opam switch for this repo.
  4. Run this command
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

5. make build-dep 6. make -j10 (I have 10 cpu cores)

Expected Behavior

For the command make -j10 to run with no errors

Current Behavior

Error message

 COQLINT
 sh: line 3: ./coq-lint.sh: cannot execute: required file not found
 make[2]: *** [Makefile.coq.local:7: real-all] Error 1
 make[1]: *** [Makefile.coq:416: all] Error 2
 make[1]: Leaving directory '/home/humam/Projects/lamba-rust-main'
 make: *** [Makefile:3: all] Error 2

What I tried

I attempted to comment style out of Makefile.coq.local, which delayed the error.

I also attempted to comment out the whole Makefile.coq.local, but that returned this error
make[2]: *** No rule to make target 'style', needed by 'real-all'.  Stop.
make[1]: *** [Makefile.coq:416: all] Error 2
make[1]: Leaving directory '/home/humam/Projects/lamba-rust-main'
make: *** [Makefile:3: all] Error 2

I also tried to input a full path into style, which gave this error.

make[1]: Entering directory '/home/humam/Projects/lamba-rust-main'
make[2]: *** No rule to make target '/home/humam/Projects/lambda-rust-main/coq-lint.sh', needed by 'style'.  Stop.
make[1]: *** [Makefile.coq:416: all] Error 2
make[1]: Leaving directory '/home/humam/Projects/lamba-rust-main'
make: *** [Makefile:3: all] Error 2
Edited by HumamAlhusaini
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information