Skip to content

Commit

Permalink
[ re #626 ] turn off NoEquivWhenSplitting warning for make check
Browse files Browse the repository at this point in the history
  • Loading branch information
@Saizan
Saizan authored Nov 19, 2021
1 parent f6ca6e6 commit 93d7f41
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion GNUmakefile
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
AGDA_EXEC?=agda -W error
AGDA_EXEC?=agda -W error -W noNoEquivWhenSplitting
FIX_WHITESPACE?=fix-whitespace
RTS_OPTIONS=+RTS -H3G -RTS
AGDA=$(AGDA_EXEC) $(RTS_OPTIONS)
Expand Down

3 comments on commit 93d7f41

@mortberg
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This causes trouble on 2.6.2:

agda -W error -W noNoEquivWhenSplitting +RTS -H3G -RTS Cubical/README.agda
Error: Unknown warning flag: NoEquivWhenSplitting. See --help=warning.

Isn't it better for the library to work on the main release rather than the development version? Alternatively the makefile could be a bit smarter and check which version of Agda is installed

@Saizan
Copy link
Contributor Author

@Saizan Saizan commented on 93d7f41 Nov 20, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, when I saw the tests passing on the PR I assumed the flag was going to be fine on 2.6.2, but actually the workflow sets its own flags.

Maybe make should run without -W error while make check would be stricter with -W error.

So that random users coming in with agda/master won't complain that make errors out for them.

@mortberg
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds good! Can you make a PR?

Please sign in to comment.