Opened 17 years ago
Closed 16 years ago
#119 closed defect (fixed)
Fix compilation problems, missing files
| Reported by: | David Aspinall | Owned by: | courtieu |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-3.7 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: |
Description
Current compilation errors:
!! File error (("Cannot open load file" "phox-fun"))
!! File error (("Cannot open load file" "phox-lang"))
!! File error (("Cannot open load file" "plastic-syntax"))
!! File error (("Cannot open load file" "twelf-font"))
!! Wrong type argument ((symbolp (quote local-vars-list-doc)))
!! Invalid argument (("Character set already defined for this DIMENSION/CHARS/FINAL/DIRECTION combo" #<charset indian-is13194 "IS 13194" "Indian IS 13194" "Generic Indian charset for data exchange with IS 13194" 94 l2r cols=2 g1 final='5' reg=IS13194-Devanagari 0x4489c>))
!! Wrong type argument ((symbolp (quote local-vars-list-doc)))
!! File error (("Cannot open load file" "phox-fun"))
!! File error (("Cannot open load file" "phox-lang"))
!! File error (("Cannot open load file" "plastic-syntax"))
!! File error (("Cannot open load file" "twelf-font"))
!! Wrong type argument ((symbolp (quote local-vars-list-doc)))
Change History (5)
comment:1 Changed 17 years ago by
| Status: | new → assigned |
|---|
comment:2 Changed 16 years ago by
| Owner: | changed from David Aspinall to courtieu |
|---|---|
| Status: | assigned → new |
At the moment the coq code doesn't compile correctly because of top-level forms and mis-ordered dependencies. Since we distribute compiled code and it runs better than interpreted, this should be fixed before release.
comment:3 Changed 16 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | new → closed |
da: I have fixed the compile problems for Coq now, with some rearrangement of the code and fixing a few bugs thrown up. The compilation process is now stricter, and halts with any errors. It's a good way of checking some basic consistency of the code.
comment:4 Changed 16 years ago by
| Resolution: | fixed |
|---|---|
| Status: | closed → reopened |
Unfortunately there are still some nasty compile issues around macro usage in the code, which need to be sorted out for clean compilation.
comment:5 Changed 16 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | reopened → closed |
Compilation now fixed, following some heavy re-organisation of files to make sure that no top-level code which relies on proof-assistant-symbol (i.e., dependent on prover chosen) is evaluated during compile time.
All fixed except x-symbol:
!! Invalid argument (("Character set already defined for this DIMENSION/CHARS/FINAL/DIRECTION combo" #<charset indian-is13194 "IS 13194" "Indian IS 13194" "Generic Indian charset for data exchange with IS 13194" 94 l2r cols=2 g1 final='5' reg=IS13194-Devanagari 0x4489c>))