Description of problem: Version-Release number of selected component (if applicable): 8.1pl3-4.fc9 How reproducible: Very Steps to Reproduce: 1. as root, `yum install coq coq-doc` 2. Attempt to view how any theorem was defined. 3. Actual results: Source files are missing for the Coq standard library, and a coqtags TAGS file is not available. Expected results: Source files are included for the Coq standard library, and a coqtags TAGS file is available. Additional info: Development using an interactive theorem prover requires access to the source of the theorem libraries. It is rare for users of an interactive theorem prover to write all of their logic from base axioms. Therefore, these users are almost always engaged in a process of extending the existing theorem library. Such extension is more akin to extending the system, instead of simply linking against it. To assist almost all developers, the theorem library is needed as source (*.v) files along with a TAGS file generated from coqtags. Use of the coq-doc documentation is cumbersome for development. The user is expected to search large index files manually to find a definition in a pretty-printed html file. Since source files are not included here, new users can not easily replay these theorems to watch the prover in action. Since such files are vital to successful proof development, they should be placed in the main package. However, if that does not meet with packaging guidelines, a coq-devel package would be acceptable.
I agree that the Coq .v files would be good to have in there. In fact, I originally wanted to do this, but I was unsure when packaging this whether this would be allowed, so I consulted other distributions - it seems this is not how things are done, say, in Debian. However, given that I think this makes the package more usable and that you, as a user, actually do want this, I'm going to make this change (and I'll look at the TAGS issue) today. Sorry for taking so long. (In reply to comment #0) > Description of problem: > > > Version-Release number of selected component (if applicable): > 8.1pl3-4.fc9 > > How reproducible: > Very > > Steps to Reproduce: > 1. as root, `yum install coq coq-doc` > 2. Attempt to view how any theorem was defined. > 3. > > Actual results: > Source files are missing for the Coq standard library, and a coqtags TAGS file > is not available. > > Expected results: > Source files are included for the Coq standard library, and a coqtags TAGS file > is available. > > Additional info: > Development using an interactive theorem prover requires access to the source > of the theorem libraries. It is rare for users of an interactive theorem prover > to write all of their logic from base axioms. Therefore, these users are > almost always engaged in a process of extending the existing theorem library. > Such extension is more akin to extending the system, instead of simply linking > against it. To assist almost all developers, the theorem library is needed as > source (*.v) files along with a TAGS file generated from coqtags. > > Use of the coq-doc documentation is cumbersome for development. The user is > expected to search large index files manually to find a definition in a > pretty-printed html file. Since source files are not included here, new users > can not easily replay these theorems to watch the prover in action. > > Since such files are vital to successful proof development, they should be > placed in the main package. However, if that does not meet with packaging > guidelines, a coq-devel package would be acceptable.
coq-8.1pl3-5.fc9 has been submitted as an update for Fedora 9. http://admin.fedoraproject.org/updates/coq-8.1pl3-5.fc9
Sources issue fixed. coqtags is for interfacing with ProofGeneral, no?... I don't think that's even packaged for Fedora, but perhaps I can assist with that too. I'll leave this bug open until that's done. (In reply to comment #0) > Description of problem: > > > Version-Release number of selected component (if applicable): > 8.1pl3-4.fc9 > > How reproducible: > Very > > Steps to Reproduce: > 1. as root, `yum install coq coq-doc` > 2. Attempt to view how any theorem was defined. > 3. > > Actual results: > Source files are missing for the Coq standard library, and a coqtags TAGS file > is not available. > > Expected results: > Source files are included for the Coq standard library, and a coqtags TAGS file > is available. > > Additional info: > Development using an interactive theorem prover requires access to the source > of the theorem libraries. It is rare for users of an interactive theorem prover > to write all of their logic from base axioms. Therefore, these users are > almost always engaged in a process of extending the existing theorem library. > Such extension is more akin to extending the system, instead of simply linking > against it. To assist almost all developers, the theorem library is needed as > source (*.v) files along with a TAGS file generated from coqtags. > > Use of the coq-doc documentation is cumbersome for development. The user is > expected to search large index files manually to find a definition in a > pretty-printed html file. Since source files are not included here, new users > can not easily replay these theorems to watch the prover in action. > > Since such files are vital to successful proof development, they should be > placed in the main package. However, if that does not meet with packaging > guidelines, a coq-devel package would be acceptable.
coq-8.1pl3-5.fc9 has been pushed to the Fedora 9 stable repository. If problems still persist, please make note of it in this bug report.
coq-8.1pl3-5.fc8 has been submitted as an update for Fedora 8. http://admin.fedoraproject.org/updates/coq-8.1pl3-5.fc8
coq-8.1pl3-5.fc8 has been pushed to the Fedora 8 stable repository. If problems still persist, please make note of it in this bug report.
This message is a reminder that Fedora 9 is nearing its end of life. Approximately 30 (thirty) days from now Fedora will stop maintaining and issuing updates for Fedora 9. It is Fedora's policy to close all bug reports from releases that are no longer maintained. At that time this bug will be closed as WONTFIX if it remains open with a Fedora 'version' of '9'. Package Maintainer: If you wish for this bug to remain open because you plan to fix it in a currently maintained version, simply change the 'version' to a later Fedora version prior to Fedora 9's end of life. Bug Reporter: Thank you for reporting this issue and we are sorry that we may not be able to fix it before Fedora 9 is end of life. If you would still like to see this bug fixed and are able to reproduce it against a later version of Fedora please change the 'version' of this bug to the applicable version. If you are unable to change the version, please add a comment here and someone will do it for you. Although we aim to fix as many bugs as possible during every release's lifetime, sometimes those efforts are overtaken by events. Often a more recent Fedora release includes newer upstream software that fixes bugs or makes them obsolete. The process we are following is described here: http://fedoraproject.org/wiki/BugZappers/HouseKeeping
Fedora 9 changed to end-of-life (EOL) status on 2009-07-10. Fedora 9 is no longer maintained, which means that it will not receive any further security or bug fix updates. As a result we are closing this bug. If you can reproduce this bug against a currently maintained version of Fedora please feel free to reopen this bug against that version. Thank you for reporting this bug and we are sorry it could not be fixed.