Build Issue: Could not find Mathlib directory #2
Description
Hi -- I am having trouble building. I am getting multiple errors similar to:
error: ././././PolyrithTutorial/02_Using_Polyrith/03DoubleCover.lean:77:4: Could not find Mathlib directory. Make sure the LEAN_SRC_PATH environment variable is set correctly
It seems these errors occur everywhere . polyrith is being invoked (so there are ~ 20-30 across most of the files in the repo)
I'm a lean novice, but I guess polyrith requires some special configuration. Particularly for using the project from VSCode, I'm not sure how I would set LEAN_SRC_PATH correctly.
Any assistance would be greatly appreciated!
- nehal