@Enrico Tassi : I added a script to create a smoke test kit on the master branch - it is just one script, not connected to CI yet. The script creates a folder with test files and both a shell script and a batch file to run them. Both scripts assume that the proper
coqc is in path. I wonder how this is best used. Should this be a separately downloadable artifact or should I e.g. integrate it into the Windows installer, so that the smoke test kit is installed? The latter would be a minot complication because one would want to smoke test only installed components, but this is solvable (e.g. check if the file exists in the run script).
The smoke test kit is mostly intended for our purposes (CI and manual smoke tests) and not so much for users - I would think that users only use it if advised by an expert to do some sanity checks.
Last updated: Jan 30 2023 at 10:03 UTC