#1071427 RFS: rumur/2024.05.07-1 -- model checker for the Murphi language

#1071427#5
Date:
2024-05-19 04:58:11 UTC
From:
To:
Package: sponsorship-requests
Severity: normal

Dear mentors,

I am looking for a sponsor for my package "rumur":

  * Package name     : rumur
    Version          : 2024.05.07-1
    Upstream contact : Matthew Fernandez <matthew.fernandez@gmail.com>
  * URL              : https://github.com/Smattr/rumur
  * License          : Unlicense
  * Vcs              : https://github.com/Smattr/rumur/tree/packaging/debian
    Section          : devel

The source builds the following binary packages:

   rumur - model checker for the Murphi language

To access further information about this package, please visit the
following URL:

https://mentors.debian.net/package/rumur/

Alternatively, you can download the package with 'dget' using this command:

   dget -x
https://mentors.debian.net/debian/pool/main/r/rumur/rumur_2024.05.07-1.dsc

Changes since the last upload:

  rumur (2024.05.07-1) unstable; urgency=medium
  .
    * New upstream release.
    * Fix inaccurate libatomic checks in autopkgtests. Closes: #1018205.
    * Fix Vcs-Browser URL. Closes: #1018202.
    * Update debian-compat Build-Depends from 12 to 13.

Regards,

#1071427#10
Date:
2024-06-14 09:47:43 UTC
From:
To:
Hi Matthew,

'rumur' is an extensive package with a lot going on at build time. Some of the
build time tests are skipped due to missing 'xmllint'. Adding 'libxml2-utils' as
a 'Build-Depends' allows the tests to be performed. There maybe reasoning why
this 'Build-Depends' was not added, but only you can let us know that.

Other tests are skipped for a variety of reasons. Maybe you could have an audit
of these and make changes where appropriate?

Please remove the 'moreinfo' tag if/when you upload a new/fixed version.

Regards

Phil

#1071427#17
Date:
2024-06-14 23:39:44 UTC
From:
To:
Control: tags -1 - moreinfo

Thanks for the review, Phil. I did it this way under the assumption that
time on the buildd machines was expensive, but I think the prevailing
wisdom is actually that letting mistakes slip through to end users is a
worse cost. I’ve done as you suggested and enabled more of the skipped
tests. The main block still skipped are the Uclid tests which depend on
a niche academic tool that is not packaged in Debian.

While we’re discussing this, Rumur can do some smarter things if an SMT
solver like Z3 is installed. Should I add z3 to Suggests? I’m unsure
about this as Z3 is merely _one_ SMT solver Rumur can use, not _the_ SMT
solver it must use.

#1071427#24
Date:
2024-06-15 18:11:29 UTC
From:
To:
Letting mistakes slip through as you say would be worse. Software is getting
more complex in a variety of fields/organisations etc. that use Debian. If build
times increase because of this the infrastructure team should see this and
move/act accordingly to meet new or higher needs.

If 'Uclid' is so niche where you believe it is not worthwhile to request its
packaging ans support it, that is your decision knowing more about it and your
package. That may change in the future, but who knows what the future may bring.

Not being required, adding 'z3' as a 'Suggests' would seem appropriate.

In 'debian/control'. Could you update to the latest 'Standards-Version' which is
4.7.0[1].

In 'debian/copyright'. I would update the line below.

Copyright: 2019 Matthew Fernandez <matthew.fernandez@gmail.com>

to

Copyright: 2019-2024 Matthew Fernandez <matthew.fernandez@gmail.com>

Other than these little things, all is good and if you wish to make these
changes, we can then ask a DD to sponsor.

[1] Link below.

https://www.debian.org/doc/debian-policy/upgrading-checklist.html#version-4-7-0

Regards

Phil

#1071427#29
Date:
2024-06-19 11:33:00 UTC
From:
To:
Many thanks for the guidance, Phil. I think I’ve applied all that and
made another upload now. Let me know what you think.

#1071427#34
Date:
2024-06-19 21:06:42 UTC
From:
To:
Hi Matthew,

Thanks for making another update of the package. Your effort and contribution to
Debian is very much welcomed.

Review...

1. Build: OK

2. Lintian: OK - See Additional: A

I: rumur: file-references-package-build-path [usr/include/rumur/location.hh]
N:
N:   The listed file or maintainer script appears to reference the build path
N:   used to build the package as specified in the Build-Path field of the
N:   .buildinfo file.
N:
N:   This is likely to cause the package to be unreproducible, but it may also
N:   indicate that the package will not work correctly outside of the
N:   maintainer's own system.
N:
N:   Please note that this tag will not appear unless the .buildinfo file
N:   contains a Build-Path field. That field is optional. You may have to set
N:   DEB_BUILD_OPTIONS=buildinfo=+path or use
N:   --buildinfo-option=--always-include-path with dpkg-buildpackage when
N:   building.
N:
N:   Please refer to https://reproducible-builds.org/,
N:   https://wiki.debian.org/ReproducibleBuilds/BuildinfoFiles, and the
N:   dpkg-genbuildinfo(1) manual page for details.
N:
N:   Visibility: info
N:   Show-Always: no
N:   Check: files/contents
N:
N:
I: rumur: file-references-package-build-path [usr/include/rumur/parser.yy.hh]

3. Licenses check: OK

4. Build Twice (sudo pbuilder build --twice <package>.dsc): OK

5. Install (No previous installs): OK

6. Upgrade (Over previous installs if any): OK

Additional...

A. The lintian buildinfo information can be investigated at the maintainers
discretion and any action be taken if required.

Summary...

I believe this package is now ready for sponsorship/upload. Could a Debian
Developer (DD) with available free time, please review this package and upload
if you feel it is ready and appropriate for the distribution.

Regards

Phil

#1071427#39
Date:
2024-06-19 22:33:45 UTC
From:
To:
Thanks, Phil.

The reproducible-builds problem is something I’ve investigated several
times over the years. As far as I can tell, I’m blocked by Flex and/or
Bison issues. In particular https://github.com/westes/flex/issues/268.
I’ve tried engaging with the Flex maintainer to get this fixed, to no
avail so far.

Do I need to re-CC mentors to get a DD’s eyes on this? Or do they see
all RFS bug updates?

#1071427#44
Date:
2024-06-20 04:33:22 UTC
From:
To:
Hi Matthew,

I see the your issue(s) with flex etc. Perceiver with upstream and you hopefully
you will be able to convince them that it is an issue of note that needs to be
fixed.

I personally see all RFS's. I would now leave it for up to two weeks and see if
a DD reviews/sponsors the package, if not a little nudge will be in order. :-)

Regards

Phil

#1071427#49
Date:
2024-07-14 06:57:40 UTC
From:
To:
Hello,

Sponsored, thanks for your work on this!

I noticed the same thing as Phil, concerning the embedded build path.
But you seem to have investigated it...

Best,

#1071427#56
Date:
2024-07-14 07:23:42 UTC
From:
To:
close 1071427
thanks

Package got sponsored