Re: Adding copilot

[Ivan Perez <ivan.perez@keera.co.uk>]

On 2022-05-10 00:39, Scott Talbert wrote:
> On Fri, 6 May 2022, Ivan Perez wrote:
>
> > Thanks again.
> >
> > I've updated the requirement on bimap.
> >
> > There's an additional issue with bimap: the `Data.Bimap` module is no 
> > longer inferred as safe in `0.4.0`, and that throws off 
> > `copilot-theorem`.
> >
> > I've opened an issue on the `bimap` package:
> > https://github.com/joelwilliamson/bimap/issues/14
> >
> > I think there are simple solutions; feel welcome to chime in if you 
> > know a good, clean way to ensure that the code can be inferred as 
> > `Safe` in this case.
> >
> > Please let me know if there's anything else you find in the meantime. 
> > I'll have everything on the copilot side prepared as needed, so that 
> > when other packages address any issues we find, we are ready.
> >
> > Happy to have an interactive session if that can make the conversation 
> > more agile.
>
> Hi Ivan,
>
> I'm not sure that I really understand what 'Safe' means in a Haskell
> context, so I'm not sure I can be of any help on that.

No problem. I'll take care of figuring out how to deal with the 'safe' 
issue.

> The newever bimap and ansi-terminal versions are the only issues I've
> found for copilot so far.  Unfortunately, adding 'what4' (which isn't
> in Debian yet) requires updating a whole bunch of other packages, and
> I haven't gotten a package plan to work yet.  It may take some time to
> sort it out.

Alright. What4's dependencies changed in version 1.3, but 
copilot-theorem still uses 1.2.1. I can update copilot-theorem to use 
what4-1.3 if needed.

Let me know if I can be of any help.

Thanks,

Ivan