Improve the error message when a file hasn't been type checked#643
Improve the error message when a file hasn't been type checked#643
Conversation
williamdemeo
left a comment
williamdemeo
left a comment
There was a problem hiding this comment.
Looks fine, assuming my understanding of the way this script is meant to work is wrong.
src/checkTypeChecked.sh
Outdated
| agdaiFn="_build/2.7.0/agda/${agdaFn%.*agda}.agdai" | ||
| if [ "$(( $(stat -c "%Y" $agdaiFn) - $(stat -c "%Y" $agdaFn) ))" -lt "0" ]; then | ||
| echo " FAIL: $agdaiFn is not up-to-date" | ||
| echo " FAIL: $agdaiFn does not exist. Please remove the corresponding agda file or import it somewhere." |
There was a problem hiding this comment.
I had the impression that if the script doesn't find an agdai file then it exits and then the corresponding agda file will be type-checked, so the agdai file will be there on the next pass. If that's true, then this error message isn't really what we want. If that's wrong, then I'm fine with the change.
There was a problem hiding this comment.
I need to double check, but I think the first pass of this script is probably pointless and can be removed. If it does something we should add a flag to this script to give the old error message on the first run and the new one on the second run. IIRC the first run of this script only prevents a call to agda if all the interface files are there, but then that call would be very quick anyway (and this would only ever happen locally anyway).
WhatisRT
force-pushed
the
andre/improve-ci-error
branch
from
8cbbd0d to
064413f
Compare
WhatisRT
force-pushed
the
andre/improve-ci-error
branch
from
064413f to
e5df2d1
Compare
2 participants
Description
Just a minor wording improvement so that it becomes clear what to do when the script that checks if files have been checked fails.
Checklist
CHANGELOG.md