Package Request: Spectacle (a Haskell DSL for formal specifications)

[byrongibson]

Project description

Spectacle is an open source, domain-specific language for writing and checking formal specifications in Haskell, by Awake Security. It is designed to replace TLA+ for formally specifying Haskell software, to achieve feature parity with TLA+ while improving on several aspects of TLA+ and TLC.

Metadata

• homepage URL: https://awakesecurity.com/blog/spectacle-a-language-for-writing-and-checking-formal-specifications-in-haskell/
• source URL: https://github.com/awakesecurity/spectacle
• license: Apache 2.0
• platforms: linux, darwin

[sternenseemann]

Can you ask upstream to upload their releases to Hackage? While it's not a requirement, it makes packaging a haskell package a lot less effort for us in general.

[cdepillabout]

cc @riz0id @evanrelf @ixmatus (from https://github.com/awakesecurity/spectacle/graphs/contributors) since I'm pretty sure they are all Nix users.

For a little context: It appears there are users that want to be able to get Spectacle from Nixpkgs. The Haskell infrastructure in Nixpkgs makes it easy (mostly automatic) for us to package/include Haskell packages that are on Hackage. It is possible for us to package Haskell packages that are not on Hackage, but it is more work for us.

[ixmatus]

I agree, uploading to Hackage would make it a lot easier to use from stock nixpkgs. We fully intend to release to Hackage. We will talk about it today. I think there are a few things we wanted to improve before releasing to Hackage, which is the only reason we haven't.

[stale]

I marked this as stale due to inactivity. → More info

[cdepillabout]

Spectacle now appears to be available on Hackage: https://hackage.haskell.org/package/spectacle

[sternenseemann]

Working with GHC 8.10.7 in haskell-updates, issue for 9.0 support here: awakesecurity/spectacle#49