Add copilot to list of packages available

[ivanperez-keera]

Feature request

Copilot is a runtime verification framework implemented as an EDSL in Haskell. The development of Copilot has been partly funded by NASA over the years. Copilot is actively maintained, with new releases coming out every 2 months. It is also used by other tools like NASA's Ogma (https://github.com/nasa/ogma), also developed in Haskell, which contributes to its relevance for the community.

I'd like to propose adding Copilot to play-haskell. It would be an easy way for people to get started trying to write Copilot specs, and it would expose users to a project that is used in real-world systems in the aerospace domain.

[ivanperez-keera]

Something worth noting is that Copilot depends on what4, which may be large. I'm sending a PR for your evaluation.

[tomsmeding]

Thanks for the suggestion and PR! I feel that copilot, while a cool project, is quite niche for the playground.

Also, when trying to add it for 9.2.7, I get the following build error:

Failed to build copilot-language-2.1.2.
Build log (
/builderprojs/ghc-9.2.7-cabal/logs/ghc-9.2.7/copilot-language-2.1.2-5ad98f9f9bb662c2cd3e0ff0c18e27ccb93121ee5b22e132e22041c962f4c303.log
):
Configuring library for copilot-language-2.1.2..
Preprocessing library for copilot-language-2.1.2..
Building library for copilot-language-2.1.2..

on the commandline: warning: [-Wdeprecated-flags]
    -auto-all is deprecated: Use -fprof-auto instead

on the commandline: warning: [-Wdeprecated-flags]
    -caf-all is deprecated: Use -fprof-cafs instead
[ 1 of 22] Compiling Copilot.Language.Error ( src/Copilot/Language/Error.hs, dist/build/Copilot/Language/Error.o, dist/build/Copilot/Language/Error.dyn_o )
[ 2 of 22] Compiling Copilot.Language.Prelude ( src/Copilot/Language/Prelude.hs, dist/build/Copilot/Language/Prelude.o, dist/build/Copilot/Language/Prelude.dyn_o )
[ 3 of 22] Compiling Copilot.Language.Stream ( src/Copilot/Language/Stream.hs, dist/build/Copilot/Language/Stream.o, dist/build/Copilot/Language/Stream.dyn_o )

src/Copilot/Language/Stream.hs:18:1: error:
    Could not load module ‘Copilot.Core.Error’
    it is a hidden module in the package ‘copilot-core-3.13’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
   |
18 | import Copilot.Core.Error
   | ^^^^^^^^^^^^^^^^^^^^^^^^^
cabal: Failed to build copilot-language-2.1.2 (which is required by exe:thing
from sandbox-0.1.0.0). See the build log above for details.

Compiling the sandbox for 9.2.5 and 8.10.7 seems to rebuild the world (haven't let that run to completion yet); I have to look more closely in what versions it requires that the previous package set did not satisfy.

Before I continue, is this build error expected (what's the range of supported compilers for copilot?)?

[ivanperez-keera]

I'm not sure why, but you are building an old version of copilot. The latest version is 3.13 (version 3.14 is scheduled to be released today, by the way).

[ivanperez-keera]

Wrt to the compilation error: just yesterday, Frank Dedden created a repo with docker images for the main versions of GHC for our own tests. If there are any issues with the most recent versions, we should be able to find out soon and I'll push a fix.

is quite niche for the playground.

I totally get your point.

This is a bit of a chicken and egg problem :smile: The playground would help us get to more people (including people that wouldn't otherwise think of trying haskell).

Copilot has historically been used in aerospace --so you're right-- but can be used for other domains too. Simon Levy has been using it with drone simulations. Joey Hess has also been doing a lot on this front by creating Arduino bindings.

We've been working on a newer version of our own tutorial. It would be really nice to see what people can do if we can make getting started ridiculously easy (thanks to play-haskell) and make some of those lessons more "interactive".

I'll review what's going on with the versions and ping you nonetheless.

[tomsmeding]

Oh oops -- you're right, I was compiling a ridiculously old version of copilot. Not sure how that happened.

Currently running into some compilation issues wrt the sandbox (network (what on earth pulls in network here) needs /dev/null and the sandbox has no /dev...), when I get through that I'll report back

[tomsmeding]

Build succeeded for 9.2.7, and this example seems to work, so that's good. No build plan found for 8.6.5:

Resolving dependencies...
cabal: Could not resolve dependencies:
[__0] trying: sandbox-0.1.0.0 (user goal)
[__1] trying: text-1.2.3.1/installed-1.2.3.1 (dependency of sandbox)
[__2] trying: copilot-3.13 (dependency of sandbox)
[__3] trying: copilot-theorem-3.13 (dependency of copilot)
[__4] next goal: what4 (dependency of copilot-theorem)
[__4] rejecting: what4-1.4 (conflict: copilot-theorem => what4>=1.3 && <1.4)
[__4] rejecting: what4-1.3 (conflict: text==1.2.3.1/installed-1.2.3.1, what4
=> text>=1.2.4.0 && <1.3)
[__4] skipping: what4-1.2.1, what4-1.2, what4-1.1 (has the same
characteristics that caused the previous version to fail: excludes 'text'
version 1.2.3.1)
[__4] rejecting: what4-1.0 (conflict: copilot-theorem => what4>=1.3 && <1.4)
[__4] fail (backjumping, conflict set: copilot-theorem, text, what4)
After searching the rest of the dependency tree exhaustively, these were the
goals I've had most trouble fulfilling: copilot, sandbox, copilot-theorem,
what4, text
Try running with --minimize-conflict-set to improve the error message.

Seems text is too old for what4 at that ghc version. 8.10.7 does seem to work.

[ivanperez-keera]

I see. I'll ask Galois if they can relax the constraint on text.

EDIT: (Note: I use 8.6.5 all the time -- this was yesterday. It's probably sth about this specific version of text.)

[tomsmeding]

It seems it's me again, I cleaned up the old generated freeze file and now does find a build plan for 8.6.5.

Something else: adding copilot more than doubles the disk space usage for compiled artifacts currently. For ghc 9.2.7, the ~/.cabal/store is 168 MB with the current list of packages, and grows to 375 MB after adding copilot >=3.13. This times 8 GHCs currently available is >1.6 GB extra disk space. On the other hand, the VPS this runs on has 34 GB free disk space remaining.

@ivanperez-keera I imagine that if this gets added to the playground, you'll want to depend on it and have some certainty that copilot will remain available. Is that true? How would you feel if I cannot 100% guarantee that copilot will remain available indefinitely?

[ivanperez-keera]

Something else: adding copilot more than doubles the disk space usage for compiled artifacts currently. For ghc 9.2.7, the ~/.cabal/store is 168 MB with the current list of packages, and grows to 375 MB after adding copilot >=3.13. This times 8 GHCs currently available is >1.6 GB extra disk space.

That was my fear. Most of it comes from what4. Although it has a lot of dependencies, the good "news" is that most are fairly standard. So, hopefully, that would not get noticeably worse over time.

I'm personally spending a fair amount of time cleaning up copilot. This will continue in the future, and our plan is to never stop refining. So, copilot itself should get lighter over time, not heavier.

Is that true? How would you feel if I cannot 100% guarantee that copilot will remain available indefinitely?

Sad :smile: But I would understand. Life is life.

But let me ask the "opposite" question: what would you need to see (e.g., in terms of usage, interest, perhaps even PR, etc.) for you to decide to keep it?

(And btw do you collect any statistics of how often people import modules from each library?)

[tomsmeding]

That was my fear. Most of it comes from what4. Although it has a lot of dependencies, the good "news" is that most are fairly standard. So, hopefully, that would not get noticeably worse over time.

I'm personally spending a fair amount of time cleaning up copilot. This will continue in the future, and our plan is to never stop refining. So, copilot itself should get lighter over time, not heavier.

<3

But let me ask the "opposite" question: what would you need to see (e.g., in terms of usage, interest, perhaps even PR, etc.) for you to decide to keep it?

More hardware. This is currently running on a cheap VPS, not because I really cannot afford more, but because I don't want to spend significant amounts of recurring money on this project. Gershom Bazerman has said to me at some point that Haskell.org might be able to supply hardware to run this stuff, and I've spoken with David Christiansen who is also of the opinion that the project needs more scalable hardware at some point in the future (once we have a better idea of exactly how much we need). In summary, I find it very likely that we can scale up at some point, and then a few gigabytes of disk space will not be an issue anymore.

Hence, disk space is probably just not a very strong argument here. :)

(And btw do you collect any statistics of how often people import modules from each library?)

I don't. It would be interesting to. Do you happen to know how to do that in a robust manner? Or is there nothing better than running the user's code through haskell-src-exts and hoping that doesn't fail too often (when GHC has syntax extensions that haskell-src-exts doesn't yet have), without having to pull in the GHC library for all GHC versions that the playground supports?

In summary we can probably merge this. I have to go now but will merge and push to production either tonight or tomorrow.

[ivanperez-keera]

I've just released Copilot 3.14 with support for GHC up to 9.4.4. GHC 9.6 may work but it wouldn't install for me with ghcup so I did not try it.

[tomsmeding]

Compiling with 9.6 doesn't find a build plan, probably because certain dependencies just haven't upped the bounds yet.

Cabal output

cabal: Could not resolve dependencies:
[__0] trying: sandbox-0.1.0.0 (user goal)
[__1] trying: transformers-0.6.1.0/installed-0.6.1.0 (dependency of sandbox)
[__2] trying: process-1.6.17.0/installed-1.6.17.0 (dependency of sandbox)
[__3] trying: mtl-2.3.1/installed-2.3.1 (dependency of sandbox)
[__4] trying: ghci-9.6.0.20230302/installed-9.6.0.20230302 (dependency of
sandbox)
[__5] trying: copilot-3.14 (dependency of sandbox)
[__6] trying: copilot-theorem-3.14 (dependency of copilot)
[__7] trying: what4-1.4 (dependency of copilot-theorem)
[__8] next goal: scientific (dependency of what4)
[__8] rejecting: scientific-0.3.7.0 (conflict: transformers =>
base==4.18.0.0/installed-4.18.0.0, scientific => base>=4.15 && <4.18)
[__8] trying: scientific-0.3.6.2
[__9] next goal: hashable (dependency of what4)
[__9] rejecting: hashable-1.4.2.0 (conflict: transformers =>
base==4.18.0.0/installed-4.18.0.0, hashable => base>=4.10.1.0 && <4.18)
[__9] rejecting: hashable-1.4.1.0 (conflict: transformers =>
base==4.18.0.0/installed-4.18.0.0, hashable => base>=4.5 && <4.18)
[__9] rejecting: hashable-1.4.0.2 (conflict: transformers =>
base==4.18.0.0/installed-4.18.0.0, hashable => base>=4.5 && <4.17)
[__9] rejecting: hashable-1.4.0.1, hashable-1.4.0.0 (conflict: transformers =>
base==4.18.0.0/installed-4.18.0.0, hashable => base>=4.9 && <4.17)
[__9] rejecting: hashable-1.3.5.0, hashable-1.3.4.1 (conflict: transformers =>
base==4.18.0.0/installed-4.18.0.0, hashable => base>=4.5 && <4.17)
[__9] rejecting: hashable-1.3.4.0 (conflict: transformers =>
base==4.18.0.0/installed-4.18.0.0, hashable => base(>=4.5 && <4.17) && <0)
[__9] rejecting: hashable-1.3.3.0, hashable-1.3.2.0 (conflict: transformers =>
base==4.18.0.0/installed-4.18.0.0, hashable => base>=4.5 && <4.17)
[__9] rejecting: hashable-1.3.1.0 (conflict: transformers =>
base==4.18.0.0/installed-4.18.0.0, hashable => base>=4.5 && <4.16)
[__9] rejecting: hashable-1.3.0.0 (conflict: transformers =>
base==4.18.0.0/installed-4.18.0.0, hashable => base>=4.5 && <4.15)
[__9] rejecting: hashable-1.2.7.0 (conflict: what4 => hashable>=1.3)
[__9] skipping: hashable-1.2.6.1, hashable-1.2.6.0, hashable-1.2.5.0,
hashable-1.2.4.0, hashable-1.2.3.3, hashable-1.2.3.2, hashable-1.2.3.1,
hashable-1.2.3.0, hashable-1.2.2.0, hashable-1.2.1.0, hashable-1.2.0.10,
hashable-1.2.0.9, hashable-1.2.0.8, hashable-1.2.0.7, hashable-1.2.0.6,
hashable-1.2.0.5, hashable-1.2.0.4, hashable-1.2.0.3, hashable-1.2.0.2,
hashable-1.2.0.1, hashable-1.2.0.0, hashable-1.1.2.5, hashable-1.1.2.4,
hashable-1.1.2.3, hashable-1.1.2.2, hashable-1.1.2.1, hashable-1.1.2.0,
hashable-1.1.1.0, hashable-1.1.0.0, hashable-1.0.1.1, hashable-1.0.1.0,
hashable-1.0.0 (has the same characteristics that caused the previous version
to fail: excluded by constraint '>=1.3' from 'what4')
[__9] fail (backjumping, conflict set: hashable, transformers, what4)
After searching the rest of the dependency tree exhaustively, these were the
goals I've had most trouble fulfilling: base, hashable, copilot-theorem,
libBF, copilot-language, copilot-c99, copilot-core, copilot, atom, scientific,
attoparsec, process, mtl, transformers, sandbox, ghci, language-c99-simple,
atto-lisp, smtlib2, what4, copilot-sbv
Try running with --minimize-conflict-set to improve the error message.

Things do seem to work for all other GHCs currently on the playground.

I'd also like to add most of the transitive dependencies of copilot, because why not. @ivanperez-keera Are you okay with me pushing that directly, and closing your PR?

[ivanperez-keera]

Are you okay with me pushing that directly, and closing your PR?

Of course! Thanks!

[tomsmeding]

Copilot should now be available for all GHCs except 9.6.1-rc1 :)

[ivanperez-keera]

That is absolutely amazing! I've started to spread the news :)