Stream: Coq Platform devs & users

Topic: Smoke test kit files


view this post on Zulip 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!

view this post on Zulip Enrico Tassi (Sep 26 2021 at 16:06):

Sorry, it was not intended to generate breakage.

What you propose makes sense to me.

view this post on Zulip 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: Jan 29 2023 at 19:02 UTC