A new release of SBV (v3.16) is now on Hackage: sbv: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
This version improves support for the semi-automated theorem-proving interface, and adds several interesting examples from the theorem-proving folklore:
Happy hacking!
-Levent.
6 Likes
Out of interest, why is every previous version “deprecated” on hackage?
My reasoning to deprecate older versions once a new version is out is simple: Each release inevitably contains some bug-fixes. While these are rarely soundness issues (though that does happen as well of course), I don’t want to take that risk. So, I deprecate old versions to guide cabal to prefer the latest.
I’m probably misusing/misunderstanding what “deprecated” is supposed to mean in the Hackage context; but this has been my main motivation. I think for a package that tries to provide guarantees about your code using (semi-)automated theorem-proving, that is justifiable.
1 Like
That’s very understandable, although I fear it doesn’t do too much; as I understand it, cabal will still solve for this older versions if later versions don’t match the constraints, meaning that deprecation does little except make the text red.
Agreed. I think there’s also a notion of “preferred versions” but I never understood how to utilize that properly.
Preferred versions are those that are not deprecated, if I understand correctly.
If cabal does not find a preferred version that matches the constraints, it will take a deprecated version.
As the only preferred version is the latest which has a bound base >= 4.19, any attempt to use SBV with GHC 9.6 or lower will inevitably pick one of the deprecated versions.
Categorially deprecating all versions but the latest effectively achieves nothing. It provides no information to the constraint solver (nor the human user) which of the older versions are more and which are less preferable.
So I think deprecation should be used sparingly. Basically if you have a bug-fix release, the version replaced by this bug-fix release should be deprecated.
5 Likes
Agreed!
As a minor note, Hackage has both deprecated and preferred versions. For example the HaskellNet package has version 0.5.2 deprecated and all versions <0.5.2 non-preferred. The Hackage documentation says:
Preferred and deprecated versions can be used to influence Cabal’s decisions about which versions of PKG to install. If a range of versions is preferred, it means that the installer won’t install a non-preferred package version unless it is explicitly specified or if it’s the only choice the installer has. Deprecating a version adds a range which excludes just that version. All of this information is collected in the preferred-versions file that’s included in the index tarball.
If all the available versions of a package are non-preferred or deprecated, cabal-install will treat this the same as if none of them are. This feature doesn’t affect whether or not to install a package, only for selecting versions after a given package has decided to be installed. Entire-package deprecation is also available, but it’s separate from preferred versions.
Thanks @andreasabel @taylorfausak
Based on your advice, I removed all deprecations from the package; leaving it entirely to cabal/stack etc., pick the right version. I trust these installers will pick the “latest” possible, which fits the bill.
2 Likes