Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Native compilation of COQ fails on IA64 and arm #3077

Closed
vicuna opened this issue Aug 18, 2004 · 2 comments
Closed

Native compilation of COQ fails on IA64 and arm #3077

vicuna opened this issue Aug 18, 2004 · 2 comments
Labels
bug

Comments

@vicuna
Copy link

vicuna commented Aug 18, 2004 •
edited

Original bug ID: 3077
Reporter: administrator
Status: closed (set by @xavierleroy on 2011-12-17T11:39:46Z)
Resolution: not fixable
Priority: normal
Severity: minor
Category: ~DO NOT USE (was: OCaml general)
Related to: #3908 #3952
Monitored by: @rixed johans smimram

Bug description

Full_Name: Samuel Mimram
Version: 3.08.0
OS: Linux
Submission from: babasse.csbnet.se (193.11.251.151)

Hello,

[I reposting here a bug that I already have reported on coq-bugs because I was
asked to do so since it is more likely to be a caml bug than a coq bug].

The native code compilation of coq seems to fail on IA64 and arm. You can see
the full log of the Debian buildd here
http://buildd.debian.org/fetch.php?&pkg=coq&ver=8.0pl1-1&arch=ia64&stamp=1092640816&file=log&as=raw
and
http://buildd.debian.org/fetch.php?&pkg=coq&ver=8.0pl1-1&arch=arm&stamp=1092662144&file=log&as=raw
(they seem to be ok but that is because we do fallback on bytecode)

The last relevant lines are:

OCAMLC    contrib/first-order/formula.ml
OCAMLC    contrib/first-order/unify.ml
OCAMLC    contrib/first-order/sequent.ml
OCAMLC    contrib/first-order/rules.ml
OCAMLC    contrib/first-order/instances.ml
OCAMLC    contrib/first-order/ground.ml
OCAMLC4   contrib/first-order/g_ground.ml4
Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead.
OCAMLC -a -o contrib/contrib.cma
COQMKTOP -o bin/coqtop.byte
OCAMLC -o bin/coqc
cd bin; ln -sf coqtop.opt coqtop
bin/coqtop.opt -boot   -translate -strict-implicit -nois -compile
theories7/Init/Notations
make[1]: *** [theories7/Init/Notations.vo] Segmentation fault
make[1]: Leaving directory `/build/buildd/coq-8.0pl1'

The -compile-verbose did not give more information:

bash-2.05a$ bin/coqtop.opt -boot  -compile-verbose -translate -strict-implicit
-nois -compile theories7/Init/Notations
Segmentation fault

(and it's the same using coqtop).

Here are the result given by a gdb on bin/coqtop.opt:

(gdb) r -boot   -translate -strict-implicit -nois -compile
theories7/Init/Notations
(no debugging symbols found)...(no debugging symbols found)...(no debugging
symbols found)...(no debugging symbols found)...
Program received signal SIGSEGV, Segmentation fault.
0x40000000007d9fb0 in svcauthdes_stats ()
(gdb) where
#0  0x40000000007d9fb0 in svcauthdes_stats ()
#1  0x40000000007de590 in svcauthdes_stats ()

The segv happens very soon in the execution of the program as shown by the
strace:

execve("bin/coqtop.opt", ["bin/coqtop.opt", "-boot", "-translate",
"-strict-implicit", "-nois", "-compile", "theories7/Init/Notations"], [/* 16
vars */]) = 0
uname({sys="Linux", node="spe156", ...}) = 0
brk(0)                                  = 0x600000000013c760
open("/etc/ld.so.preload", O_RDONLY)    = -1 ENOENT (No such file or directory)
open("/etc/ld.so.cache", O_RDONLY)      = 3
fstat(3, {st_mode=S_IFREG|0644, st_size=18197, ...}) = 0
mmap(NULL, 18197, PROT_READ, MAP_PRIVATE, 3, 0) = 0x2000000000030000
close(3)                                = 0
open("/lib/libm.so.6.1", O_RDONLY)      = 3
read(3, "\177ELF\2\1\1\0\0\0\0\0\0\0\0\0\3\0002\0\1\0\0\0\300\224"..., 1024) =
1024
fstat(3, {st_mode=S_IFREG|0644, st_size=557528, ...}) = 0
mmap(NULL, 620224, PROT_READ|PROT_EXEC, MAP_PRIVATE, 3, 0) = 0x2000000000044000
mprotect(0x20000000000cc000, 63168, PROT_NONE) = 0
mmap(0x20000000000d4000, 32768, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_FIXED, 3,
0x80000) = 0x20000000000d4000
close(3)                                = 0
open("/lib/libdl.so.2", O_RDONLY)       = 3
read(3, "\177ELF\2\1\1\0\0\0\0\0\0\0\0\0\3\0002\0\1\0\0\0\2404\0"..., 1024) =
1024
fstat(3, {st_mode=S_IFREG|0644, st_size=68808, ...}) = 0
mmap(NULL, 66880, PROT_READ|PROT_EXEC, MAP_PRIVATE, 3, 0) = 0x20000000000dc000
mprotect(0x20000000000e0000, 50496, PROT_NONE) = 0
mmap(0x20000000000ec000, 16384, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_FIXED, 3,
0x10000) = 0x20000000000ec000
close(3)                                = 0
open("/lib/libc.so.6.1", O_RDONLY)      = 3
read(3, "\177ELF\2\1\1\0\0\0\0\0\0\0\0\0\3\0002\0\1\0\0\0ph\3\0"..., 1024) =
1024
fstat(3, {st_mode=S_IFREG|0755, st_size=2427032, ...}) = 0
mmap(NULL, 2508832, PROT_READ|PROT_EXEC, MAP_PRIVATE, 3, 0) =
0x20000000000f0000
mprotect(0x2000000000338000, 116768, PROT_NONE) = 0
mmap(0x2000000000340000, 65536, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_FIXED, 3,
0x240000) = 0x2000000000340000
mmap(0x2000000000350000, 18464, PROT_READ|PROT_WRITE,
MAP_PRIVATE|MAP_FIXED|MAP_ANONYMOUS, -1, 0) = 0x2000000000350000
close(3)                                = 0
mmap(NULL, 32768, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) =
0x2000000000358000
mmap(NULL, 16384, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) =
0x2000000000038000
munmap(0x2000000000030000, 18197)       = 0
brk(0)                                  = 0x600000000013c760
brk(0x600000000013c7a0)                 = 0x600000000013c7a0
brk(0x6000000000140000)                 = 0x6000000000140000
mmap(NULL, 278528, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) =
0x2000000000360000
brk(0x600000000014c000)                 = 0x600000000014c000
mmap(NULL, 495648, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) =
0x20000000003a4000
readlink("/proc/self/exe", "/house/smimram/build/coq-8.0pl1/bin/coqtop.opt",
256) = 46
stat("/house/smimram/build/coq-8.0pl1/bin/coqtop.opt", {st_mode=S_IFREG|0755,
st_size=10989824, ...}) = 0
lseek(0, 0, SEEK_CUR)                   = -1 ESPIPE (Illegal seek)
lseek(1, 0, SEEK_CUR)                   = 3039
brk(0x6000000000150000)                 = 0x6000000000150000
lseek(2, 0, SEEK_CUR)                   = 3147
gettimeofday({1092840396, 872935}, NULL) = 0
getppid()                               = 22484
getpid()                                = 22485
mmap(NULL, 1064960, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) =
0x2000000000420000
times({tms_utime=9, tms_stime=2, tms_cutime=0, tms_cstime=0}) = 2484566395
--- SIGSEGV (Segmentation fault) @ 40000000007d9fb0 (0) ---
+++ killed by SIGSEGV +++

Thanks for your help.

Regards,

Samuel.
@vicuna
Copy link
Author

vicuna commented Jan 31, 2005

Comment author: administrator

Access to IA64 and ARM plaforms is difficult.

@vicuna
Copy link
Author

vicuna commented Dec 17, 2011

Comment author: @xavierleroy

By lack of public interest, the next major release of OCaml will no longer offer an IA64/Itanium native-code generator. I am therefore closing this PR.

The ARM port, however, is still supported and improved. If the ARM problem is still there, feel free to submit a new PR.

@vicuna vicuna closed this as completed Dec 17, 2011
This was referenced Mar 14, 2019
Closed
Closed
@vicuna vicuna added the bug label Mar 19, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@vicuna