Output linter version during execution

[SvenUmbricht]

This PR adds version output to each run of the witness linter. To get more precise information about the used version, the current git revision is also appended when possible.

Closes #53.

[MartinSpiessl]

This does only work when using a git repository with witness lint. But ideally we also have the verison available for packaged versions of the linter.

Currently there is a variable for storing the version inside https://github.com/sosy-lab/sv-witnesses/blob/main/lint/witnesslint/linter.py

Ideally we set this version to something like "dev". When packaging the linter we can then set this via git describe --dirty.

The verison output of the linter could e.g. first try to determine whether this is a source checkout and use git describe --dirty, and if this is not the case, default to output the version that is stored in that version variable inside linter.py.

Does this make sense?

[PhilippWendler]

Coupling the linter to git as proposed in this PR is somewhat dangerous, for example if in the future we migrate away from git or git changes it command-line parameters etc. So at the very least the code needs to be robust against all kinds of errors when determining the version (git not installed, git returning an error, etc.). I don't think catching FileNotFoundError is enough for this.

What Martin suggests is feasible, we do something like this in CPAchecker, although there we do not need to do it at runtime, but only at build time. (However, if done the code should look first at the hard-coded version and only attempt to run git if this looks like a development version.)

But I want to suggest that for a small project like this, determining the version based on git is not necessary. Just declare a version in the source code, suffixed with -dev for all intermediate commits and without this suffix for releases.
Yes, one has to bump the version manually (but when releasing a new version this is negligible effort compared with writing a changelog, uploading everything etc.) and one looses the exact commit identifier when running a development version, but this is often acceptable (and I would say that this is the case here after #39). We follow this strategy in BenchExec and it works fine.

[SvenUmbricht]

Removed the dependency on git. Personally I also prefer not having this here, but it also means we discard the second part of #53. @MartinSpiessl Is that acceptable for you?

[MartinSpiessl]

Well, the main issue I really think should be addressed is that it should always be clear in SV-COMP which version of the linter was run. Manually bumping the version before creating a zip for the archives repository of the SV-COMP is error-prone, because one might forget to do this and then we have two different versions of the linter which give the same version string.

In the worst case this could lead to a lot of work caused because people try to debug a problem without realizing that there were two different linter versions.

This should be addressed, but can be done in the packaging script/method (that does not yet exist but really should).
So the linter itself does not necessarily need to determine the version via git, I agree with that feature being removed.

Also having commits that just do "bump version to x.y.z" just feels odd to me, there should be a more elegant way to achieve this. I just stumbled upon Python Semantic Release(PSR) via https://py-pkgs.org/07-releasing-versioning.html#automatic-version-bumping , this looks interesting, but is probably overkill for such a small project as the linter.

(and I would say that this is the case here after #39)

Hmmm, I am curious, how would having the package make this easier? As I see it one would also have to bump the version there, so while this would be an improvement for users who want to install the package e.g. via pip, this would not really affect the general considerations of how the version is determined.

Regarding this MR, I think it is good like this and we can merge it. Then worry about how to package the linter for SV-COMP independently from this.

[PhilippWendler]

In the worst case this could lead to a lot of work caused because people try to debug a problem without realizing that there were > two different linter versions.

This is why it is critical to have a clear indication whether a version is a proper release version or a non-unique identifier of a range of commits. Suffixing -dev is a proper way to do this. And this is enough in practice, because it avoids all misunderstandings. If there really comes up the question whether the linter was used in commit 2398ac or 08ef645 when the printed version was 1.0-dev, one can just run it again with a known version. But if releases are made often enough, then this question won't even come up in practice. (Experience from years of BenchExec development.)

Also having commits that just do "bump version to x.y.z" just feels odd to me, there should be a more elegant way to achieve this. I just stumbled upon Python Semantic Release(PSR) via py-pkgs.org/07-releasing-versioning.html#automatic-version-bumping , this looks interesting, but is probably overkill for such a small project as the linter.

I think you are overcomplicating this and your link also just creates such commits. There is nothing bad with this, and it is also negligible effort because it can be automated with a few lines of script.

(and I would say that this is the case here after #39)

Hmmm, I am curious, how would having the package make this easier?

I didn't say this becomes easier.
But if you have the package, then you need to make releases that are uploaded to PyPi, and when making such releases (which should include changelogs, for example), bumping the version is negligible compared with the rest of the effort.

[SvenUmbricht]

Merging this since the current version seems to be acceptable for everyone. Further discussion can take place in #39, once that PR is ready.

[PhilippWendler]

The version-number change in this PR is not good: 1.2-dev is a smaller version number than 1.2by common versioning standards. So this violates version monotonicity. It would be good to bump it to 1.3-dev immediately.

[SvenUmbricht]

Done in 42a9175.