Michael Soegtrop (Sep 26 2021 at 16:00): Michael Soegtrop (Sep 26 2021 at 16:00):@Enrico Tassi: since you rename the example files I use in the smoke test kit in most versions of most of your projects - and sometimes also required -Q options - and since this cause a bit of work (usually additional CI runs + some research of a where the file went / how to compile them), do you think I should request for all Coq Platform projects a file called "smoke_test.v" which runs without any -Q options? Is the name appropriate?
Of course all package maintainers are welcome to comment!
Enrico Tassi (Sep 26 2021 at 16:06):Sorry, it was not intended to generate breakage.
What you propose makes sense to me.
Michael Soegtrop (Sep 26 2021 at 17:33):No problem - it is a valid improvement to make the names of example files clearer. I anyway think it would be better to have dedicated smoke test files, since the purpose of an example and a smoke test file is different.
Last updated: Jun 03 2023 at 03:01 UTC