Bug 492830 - coqtop fails
coqtop fails
Status: CLOSED NOTABUG
Product: Fedora
Classification: Fedora
Component: coq (Show other bugs)
10
All Linux
low Severity medium
: ---
: ---
Assigned To: Alan Dunn
Fedora Extras Quality Assurance
:
Depends On:
Blocks:
  Show dependency treegraph
 
Reported: 2009-03-30 04:32 EDT by Bjorge Solli
Modified: 2009-03-31 07:45 EDT (History)
1 user (show)

See Also:
Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Story Points: ---
Clone Of:
Environment:
Last Closed: 2009-03-31 07:45:23 EDT
Type: ---
Regression: ---
Mount Type: ---
Documentation: ---
CRM:
Verified Versions:
Category: ---
oVirt Team: ---
RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: ---


Attachments (Terms of Use)

  None (edit)
Description Bjorge Solli 2009-03-30 04:32:22 EDT
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
Comment 1 Alan Dunn 2009-03-30 13:13:33 EDT
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
Comment 2 Bjorge Solli 2009-03-31 07:40:00 EDT
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
Comment 3 Bjorge Solli 2009-03-31 07:45:23 EDT
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.

Note You need to log in before you can comment on or make changes to this bug.