search

openai / lean-gym

Apache License 2.0
167 stars 30 forks source link

Make scripts fail fast #29

Open fzyzcjy opened 1 year ago

fzyzcjy commented 1 year ago

When using it (incorrectly), I got something like 

mv: rename ./_target/deps/mathlib/src/all.lean to ./_target/deps/minif2f/lean/src/all.lean: No such file or directory
./scripts/setup.sh: line 15: ./_target/deps/minif2f/lean/src/all.lean: No such file or directory
./scripts/setup.sh: line 16: ./_target/deps/minif2f/lean/src/all.lean: No such file or directory

However, the script continues running and thus it is easy for users not to realize this problem. Thus, to follow the best practices of shell scripting, I add the flags to make it fail fast.