Bug 492830
| Summary: | coqtop fails | ||
|---|---|---|---|
| Product: | [Fedora] Fedora | Reporter: | Bjorge Solli <bjorge> |
| Component: | coq | Assignee: | Alan Dunn <amdunn> |
| Status: | CLOSED NOTABUG | QA Contact: | Fedora Extras Quality Assurance <extras-qa> |
| Severity: | medium | Docs Contact: | |
| Priority: | low | ||
| Version: | 10 | CC: | amdunn |
| Target Milestone: | --- | ||
| Target Release: | --- | ||
| Hardware: | All | ||
| OS: | Linux | ||
| Whiteboard: | |||
| Fixed In Version: | Doc Type: | Bug Fix | |
| Doc Text: | Story Points: | --- | |
| Clone Of: | Environment: | ||
| Last Closed: | 2009-03-31 11:45:23 UTC | Type: | --- |
| Regression: | --- | Mount Type: | --- |
| Documentation: | --- | CRM: | |
| Verified Versions: | Category: | --- | |
| oVirt Team: | --- | RHEL 7.3 requirements from Atomic Host: | |
| Cloudforms Team: | --- | Target Upstream Version: | |
| Embargoed: | |||
|
Description
Bjorge Solli
2009-03-30 08:32:22 UTC
Hmm... it works on my machine (Fedora 10, i386), and package builds incorporate a test that uses coqtop. Do you have any more specific information that might help? (Eg: platform - perhaps not i386?, any non-standard directory structure organization that it's potentially possible I failed to account for?, any special non-standard OCaml configuration?) (In reply to comment #0) > Description of problem: > coqtop fails > > Version-Release number of selected component (if applicable): > coq-8.1pl4-3.fc10.i386 > coqide-8.1pl4-1.i386 > > Actual results: > # coqtop > Welcome to Coq 8.1pl4 (Oct. 2008) > Warning: Cannot open /usr/lib/coq/states > Warning: Cannot open /usr/lib/coq/theories > Warning: Cannot open /usr/lib/coq/contrib > Error during initialization : > User error: Can't find file initial.coq on loadpath I personally have never used coqtop before, so I have not done anything to alter the behaviour of the package. My users report that this used to work and now it doesn't. coq has probably been updated during that timeframe. The only thing that comes to mind that could result in unwanted results is that we use cifs as the filesystem on home dirs. Other than this I see that if I unset COQLIB it works. COQLIB is set to /usr/lib/coq in a profile.d-script. Maybe it should not be set to this? I also set COQBIN=/usr/bin/ # uname -r 2.6.27.19-170.2.35.fc10.i686 Bjørge I now see that this profile.d-script is left after our old home-compiled coq-install. After removing it everything works fine. Sorry for the trouble. |