Bug 1735619

Summary: coq can't be installed: nothing provides antlr4-python3-runtime = 1:4.7.2-2.fc31 needed by coq-8.9.1-3.fc31.x86_64
Product: [Fedora] Fedora Reporter: Richard W.M. Jones <rjones>
Component: coqAssignee: Alan Dunn <amdunn>
Status: CLOSED NEXTRELEASE QA Contact: Fedora Extras Quality Assurance <extras-qa>
Severity: unspecified Docs Contact:
Priority: unspecified    
Version: 31CC: amdunn, loganjerry
Target Milestone: ---   
Target Release: ---   
Hardware: Unspecified   
OS: Unspecified   
Whiteboard:
Fixed In Version: Doc Type: If docs needed, set a value
Doc Text:
Story Points: ---
Clone Of: Environment:
Last Closed: 2019-08-30 03:14:17 UTC Type: Bug
Regression: --- Mount Type: ---
Documentation: --- CRM:
Verified Versions: Category: ---
oVirt Team: --- RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: --- Target Upstream Version:
Embargoed:

Description Richard W.M. Jones 2019-08-01 07:28:06 UTC
Description of problem:

There seems to be a missing or renamed dependency which
makes coq uninstallable:

nothing provides antlr4-python3-runtime = 1:4.7.2-2.fc31 needed by coq-8.9.1-3.fc31.x86_64

I couldn't work out what package "antlr4-python3-runtime"
refers to.  Not antlr4 which is a Java program with no
Python.

Version-Release number of selected component (if applicable):

coq-8.9.1-3.fc31.x86_64

How reproducible:

100%

Steps to Reproduce:
1. dnf install coq

Comment 1 Richard W.M. Jones 2019-08-01 07:29:25 UTC
flocq fails to build because of this missing dependency, see:
https://koji.fedoraproject.org/koji/taskinfo?taskID=36718347

Comment 2 Jerry James 2019-08-01 17:31:19 UTC
This is a sad tale of woe and dismay, intimately tied in with the implosion of the Java stack in Fedora.  The original problems are that antlr4 in Rawhide is too old (bug 1596974) and it doesn't ship any language runtimes other than Java (bug 1599015).  Since I could not update coq while those bugs remained unfixed, in desperation I finally added the necessary runtime to the coq package itself.  This is stupid and dangerous, as I noted in the comments to bug 1599015, but the alternative was to leave coq in a broken state over a long time frame.  (Or take over the antlr4 package, of course, but I have neither the expertise nor the bandwidth to do that.)

So now we've got two upstreams in the coq package with two different version and release numbers.  The issue you've stumbled over happened because the main package has this:

Requires:       antlr4-python3-runtime = 1:%{antlr4ver}-%{antlr4rel}

But your commit did not change antlr4rel; it added a .1 to the Release field of the antlr4-python3-runtime subpackage instead.  That won't work.  The antlr4rel number has to be changed instead.  I have fixed this and started a new build.

Don't bother rebuilding the coq stack, by the way.  I'm about to update flocq, gappalib-coq, and frama-c to new versions anyway, so I will do all of those builds, along with the necessary zenon, why3, and why rebuilds.

Comment 3 Richard W.M. Jones 2019-08-01 17:40:09 UTC
No problem, I've added coq + all BR dependencies to the ignore list of my rebuild script.

Comment 4 Ben Cotton 2019-08-13 16:48:25 UTC
This bug appears to have been reported against 'rawhide' during the Fedora 31 development cycle.
Changing version to '31'.

Comment 5 Jerry James 2019-08-30 03:14:17 UTC
Built in Rawhide.