It was tagged so recently (and without binaries) that I think we can delete the tag and tag a new release.

The release and tag have both been deleted

CI builds. Can I get an approval, so I can get this merged?

I think this is fine for now, especially since the old release has now been deleted, but just for future reference - we don’t know what kind of automation people might have with tags and releases and repo mirrors and so on, so in the future I would prefer to err on the side of not modifying existing tags. In this case I would have created a new v0.14.4 tag instead, and a small note in the changelog that v0.14.3 isn’t a real release.

Does using --haddock affect the size of the resulting binary? I’m now wondering if the binary we get will include docs somehow where it didn’t previously, causing the binary to be larger. I can’t see why else it would end up in a separate directory. If so I think the correct fix may be to avoid --haddock entirely, at least for release builds.

we don’t know what kind of automation people might have with tags and releases and repo mirrors and so on, so in the future I would prefer to err on the side of not modifying existing tags. In this case I would have created a new v0.14.4 tag instead, and a small note in the changelog that v0.14.3 isn’t a real release.

Makes sense. Mind if I add that to the RELEASE_GUIDE.md in case this should occur again?

Does using --haddock affect the size of the resulting binary?

I'm looking into that right now.

Adding this to RELEASE_GUIDE.md sounds like a great idea 👍

# v0.14.2
ls -ls purs.bin 
48408 -rwxr-xr-x 1 jordan jordan 49561488 Jun  5 12:18 purs.bin

# binary built from this PR
$ ls -ls purs 
48500 -rwxr-xr-x 1 jordan jordan 49650640 Jul  6 17:55 purs

The difference is 89,152

I think we need to be comparing the old CI script with the new one when run against the same code. What do you get if you revert only the changes in ci/build.sh but leave everything else alone?

If the difference turns out to less than 100KB though then I think that’s safe to ignore.

$ ls -ls purs 
48496 -rwxr-xr-x 1 jordan jordan 49650640 Jul  6 18:39 purs

Seems to be the same binary.

Thanks for checking!