Intent to retire why

In a few days, I intend to update coq to version 8.9.1 in Rawhide, and
also update all of the packages that depend on it. The why package
has been abandoned by upstream. Its latest version does not work with
the latest versions of its dependent packages (why3 and frama-c), and
upstream has no intention of fixing it. I intend to retire it when I
do the updates. If somebody wants it, let me know, but be aware that
you will effectively have to become upstream.


Re: Intent to retire why

By Richard W.M. Jones at 06/03/2019 - 11:39

On Fri, May 31, 2019 at 10:10:11AM -0600, Jerry James wrote:
why3 is a replacement for it, is that right?


<a href="" title=""></a>
<a href="" title=""></a>

Still waiting for 4.08 to be released to complete this ...


Re: Intent to retire why

By Jerry James at 06/03/2019 - 14:24

Sort of. Wh3 was originally intended to be a complete replacement, but
functionality has been migrated slowly, requiring one to use both why and
why3 for some years now to get everything. For example, why has a frama-c
plugin. The why3 version exists, but upstream says it is experimental and
has advised me not to even build it for Fedora. The C and Java front ends
for why (<a href="" title=""></a>) have not been replicated in why3 yet.
The situation is unfortunate, but upstream has limited resources.

Over the weekend, I took a look at how hard it would be to keep why working
with the current versions of frama-c and why3. I came up with a patch that
at least gets it to build. I'm going to experiment with it over the next
couple of days and see if the functionality actually works at all. If it
does, I will keep the why package around a little longer, to give any users
time to finish migrating to why3. However, such users should note that
another release of Frama-C is expected in a couple of weeks. If that
release breaks the why package again, I may or may not be able to repair it
again. If not, I will retire the why package at that time.

Noted. I will probably get all these packages built on Wednesday or
Thursday of this week. If that turns out to be a bad time for you, please
let me know and I will postpone the builds. Regards,

Re: Intent to retire why

By Jerry James at 06/06/2019 - 23:12

I got about half of the builds done. Unfortunately, the alt-ergo build
failed on 32-bit ARM with errors that I don't understand:

<a href="" title=""></a>

I ran the build twice just in case it was alpha particles at work, but
sadly got the same result, namely lots of errors messages like this:

/tmp/camlasm8765df.s: Assembler messages:
/tmp/camlasm8765df.s:34184: Error: value of 0000000000035170 too large for
field of 2 bytes at 000000000000ee3e
/tmp/camlasm8765df.s:34186: Error: value of 000000000003356e too large for
field of 2 bytes at 000000000000ee42
/tmp/camlasm8765df.s:34188: Error: value of 000000000003356e too large for
field of 2 bytes at 000000000000ee46

That looks like a 32-bit issue, but the i386 build was successful, so I'm
not sure what is going on here. This is with ocaml 4.07, of course, so
there is some hope that 4.08 will fix the issue. If this really is due to
a code error in alt-ergo, though, it will have to be addressed. Any hints
much appreciated.

Re: Intent to retire why

By Jerry James at 06/08/2019 - 22:13

Some hunting around turned up this:

<a href="" title=""></a>

Sure enough, reinvoking ocamlopt with -fno-thumb resulted in a successful
build of the offending file. I'll try to work that into the spec file
somehow and get the alt-ergo build going again. It doesn't appear to me
that this issue has been resolved upstream yet, though.

Incidentally, thinks today is 10
March 2019.