Re: Adding copilot

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

On 2022-10-14 00:40, Scott Talbert wrote:
> On Fri, 14 Oct 2022, Ivan Perez wrote:
> > On 2022-10-12 14:00, Scott Talbert wrote:
> > > Now, I am down to just a failure on armhf where the build is timing
> > > out. That one file ([57 of 79] Compiling What4.Expr.Builder (
> > > src/What4/Expr/Builder.hs, dist-ghc/build/What4/Expr/Builder.o,
> > > dist-ghc/build/What4/Expr/Builder.dyn_o )) takes a REALLY long time 
> > > to
> > > compile!
> >
> > I asked about this. Without access to that architecture, they can't 
> > figure out why that file takes so long to compile on armhf but not 
> > e.g., armel.
>
> It does take a long time to compile on armel as well - but not sure
> why it seems slightly faster on armel.  In any event, we tried
> building what4 on armhf and it actually succeeded this time.  So,
> we're past that issue now. copilot-theorem and copilot-language built,
> and -libraries is building now.  :)

Yay!

> [...]
>
> That particular file takes a long time to compile even on amd64, so it
> seems likely whatever improvements made to amd64 performance would be
> applicable to other architectures too.

Since we are now past this issue, I'll just propose to the what4 team 
that the file be split in future releases to make things easier.

> I do have access to all of the
> Debian architectures so if you want me to try something on an arm box,
> let me know.

Thanks!

Ivan